Marginis #
/- We formally verify the method known as recursive backtracking for a monotone predicate P and another predicate Q at the leaves. -/
A vector of length L monus k, thought of as a possible suffix for a word of length L in which the first k bits are unspecified For example, a Gap 10 10 has length 10 - 10.
[This is a rewrite to replace by induction
by match with
.]
The number of strings satisfying P ∧ Q
, where
P
is a monotone predicate and Q
is a predicate at the leaves.
Equations
- One or more equations did not get rendered due to their size.
- num_by_backtracking P Q w_2 = if P ↑w_2 ∧ Q ↑w_2 then 1 else 0
Instances For
Simplifying a list defined by a vacuous ite
.
Simplifying a gap defined by a vacuous ite
.
Simplifying a gap defined by a vacuous ite
involving num_by_backtracking
.
Writing num_by_backtracking
as a sum of values of itself.
Fintype.card extensionality.
Two vectors are equal if they have the same length and one is a suffix of the other.
For vectors t,y,x
, if y = t ++ x
and y
is longer than x
then t
is nonempty.
If x
and y
have w
as a prefix and are of the same length as w
, then x=y
.
If some sets are disjoint, then the cardinality of their union is the sum of their cardinalities.
Verifies recursive backtracking for b
-ary trees with monotone predicates P
,
with a non-monotone Q
at the leaves.
Gap has decidable equality.
Equations
- instDecidableEqGapSuccOfNatNat = Subtype.instDecidableEq
The lists with a given suffix satisfying conditions P (recursively) and Q.
Equations
- One or more equations did not get rendered due to their size.
- satisfy_and_have_suffix P Q w_2 = if P ↑w_2 ∧ Q ↑w_2 then {w_2} else ∅
Instances For
those_with_suffix
as a union of its own values.
If w
satisfies a predicate then the set of its extensions of the same length
that do the same is {w}
.
satisfy_and_have_suffix
is as advertised.