type: definition
verification: machine_ready
dependencies: ["D1-2-formal.md"]
verification_points:
- no_consecutive_ones
- valid_string_set
- recursive_generation
- fibonacci_counting
No11Constraint(Encode : Encoding) : Prop ≡
∀s : Element . s ∈ S →
¬Contains11(Encode(s))
Contains11(str : BinaryString) : Prop ≡
∃i : ℕ . i < |str| - 1 ∧
str[i] = 1 ∧ str[i+1] = 1
Valid_no11 : Set[BinaryString] ≡
{str : BinaryString | ¬Contains11(str)}
Pattern_11 : Set[BinaryString] ≡
{w ∈ {0,1}* | ∃u,v ∈ {0,1}* . w = u ++ "11" ++ v}
Valid_no11 = L((0|10)*(1|ε))
ValidString ::= ε
| 0 · ValidString
| 10 · ValidString
| 1
FSA_no11 := {
States: {q₀, q₁, q_reject},
Start: q₀,
Accept: {q₀, q₁},
Transitions: {
δ(q₀, 0) = q₀,
δ(q₀, 1) = q₁,
δ(q₁, 0) = q₀,
δ(q₁, 1) = q_reject,
δ(q_reject, _) = q_reject
}
}
PrefixClosed(Valid_no11) :=
∀s ∈ Valid_no11 . ∀p prefix_of s . p ∈ Valid_no11
ExtensionRules(s ∈ Valid_no11) := {
s ++ "0" ∈ Valid_no11,
s ++ "1" ∈ Valid_no11 ⟺ ¬EndsWith1(s)
}
Count_no11(n : ℕ) : ℕ := F_{n+2}
where F_k = Fibonacci(k)
Capacity_no11 := lim_{n→∞} (log₂ Count_no11(n))/n = log₂ φ
where φ = (1 + √5)/2
def verify_no_consecutive_ones(binary_string):
return "11" not in binary_string
def verify_valid_string_set(strings):
return all(verify_no_consecutive_ones(s) for s in strings)
def verify_recursive_generation(string):
return matches_grammar(string, valid_no11_grammar)
def verify_fibonacci_counting(n):
return count_valid_strings(n) == fibonacci(n+2)