Imports
/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module
public import Geb.Prototypes.Computability.CobhamFoldProto.ExprThe recognizer as the fold's degenerate instance
The fold of Geb/Prototypes/Computability/CobhamFoldProto/Expr.lean at the
terminal algebra — the carrier Unit, whose encoding is empty, so p = 0 —
meets the recognizer of Geb/Mathlib/Computability/Cobham/RankedTree.lean at
each layer: the state layout, the dispatch window, the readout window, the bits
a step drops and prepends, and the accepted language.
The two are not one expression. boundMulRaw_ne_boundRaw separates the two
bound children at multiplicity one, at every growth, so the raw trees differ;
and the rejecting words differ, foldOutSem_unit_eq_ite giving [false]
where
Cobham.isRankedSem_eq_ite gives the empty bitstring. What holds is that each
component coincides and the languages agree.
Main definitions
Geb.CobhamFold.encUnit, Geb.CobhamFold.decUnit — the empty encoding of the
terminal carrier and its inverse.
Geb.CobhamFold.algUnit — the terminal algebra.
Main statements
Geb.CobhamFold.dispatchWidthF_zero — the dispatch window at p = 0 is
Cobham.dispatchWidth.
Geb.CobhamFold.stackBits_unit — the stack's layout at p = 0 is the
pending count in unary.
Geb.CobhamFold.stateWordF_unit — the state layout at p = 0 is
Cobham.stateWord of the projected state.
Geb.CobhamFold.readoutWidth_zero — the readout window at p = 0 is the
recognizer's verdict window.
Geb.CobhamFold.dropCountF_unit, Geb.CobhamFold.nextPrefixF_unit — the bits
a step drops and prepends at p = 0 are Cobham.dropCount and
Cobham.nextPrefix of the projected state.
Geb.CobhamFold.foldOut_unit — the fold at the terminal algebra is present
exactly on the valid words.
Geb.CobhamFold.foldOutSem_unit_eq_ite — the expression at the terminal
algebra decides RankedAlphabet.Valid, pinning its value on both branches.
Implementation notes
nextPrefixF branches on Geb.CobhamFold.symOf where Cobham.nextPrefix
branches on RankedAlphabet.arOf, and the two agree through
Geb.CobhamFold.arOf_eq_map_symOf rather than by reduction, which is why
dropCountF_unit and nextPrefixF_unit are proved by a case analysis rather
than stated as rfl.
Cobham.isRankedSem_eq_ite gives the recognizer's rejecting value as the empty
bitstring, while foldOutSem_unit_eq_ite gives [false]: outWord spells both
branches at the width p + 1, so that the marker alone separates them. The
languages the two accept are the same.
one_le_one_mul_width takes the multiplier one: the state carries one bit per pending
subterm and the count rises once per R.width input bits, so at p = 0 the
state never exceeds the input by more than the flag and the slot, which is the
additive bound Cobham.scan already admits.
References
[Cobham1965]
Tags
Cobham, ranked alphabet, fold, terminal algebra, recognizer
@[expose] public sectionnamespace Geb.CobhamFoldopen Cobham RankedAlphabetThe empty encoding of the terminal carrier.
def encUnit : Unit → Fin 0 → Bool := fun _ ↦ Fin.elim0The inverse of the empty encoding.
def decUnit : (Fin 0 → Bool) → Unit := fun _ ↦ ()
The empty encoding's retraction, which holds by Unit's eta.
The terminal algebra of a ranked alphabet.
def algUnit (R : RankedAlphabet) :
(i : Fin R.card) → (Fin (R.arity i) → Unit) → Unit := fun _ _ ↦ ()
The multiplier one meets the bound at p = 0.
theorem one_le_one_mul_width (R : RankedAlphabet) : 0 + 1 ≤ 1 * R.width := R:RankedAlphabet⊢ 0 + 1 ≤ 1 * R.width
R:RankedAlphabetthis:0 < R.width⊢ 0 + 1 ≤ 1 * R.width
All goals completed! 🐙
The dispatch window at p = 0 is the recognizer's.
theorem dispatchWidthF_zero (R : RankedAlphabet) :
dispatchWidthF R 0 = dispatchWidth R := R:RankedAlphabet⊢ dispatchWidthF R 0 = dispatchWidth R
R:RankedAlphabet⊢ 1 + R.width + (0 + 1) * (R.maxArity + 1) = R.width + R.maxArity + 2
All goals completed! 🐙
The readout window at p = 0 is the recognizer's verdict window, which
Cobham.acceptTest reads at R.width + 3 bits.
theorem readoutWidth_zero (R : RankedAlphabet) :
readoutWidth R 0 = R.width + 3 := R:RankedAlphabet⊢ readoutWidth R 0 = R.width + 3
R:RankedAlphabet⊢ 1 + R.width + (0 + 1) * 2 = R.width + 3
All goals completed! 🐙
An entry at p = 0 is the single true the unary count spells.
The stack's layout at p = 0 is the pending count in unary.
theorem stackBits_unit : ∀ st : List Unit,
stackBits encUnit st = List.replicate st.length true :=
List.rec rfl fun a t ih ↦ a:Unitt:List Unitih:stackBits encUnit t = List.replicate t.length true⊢ stackBits encUnit (a :: t) = List.replicate (a :: t).length true
All goals completed! 🐙
The state layout at p = 0 is Cobham.stateWord of the projected state.
theorem stateWordF_unit (R : RankedAlphabet) (s : FoldScan Unit) :
stateWordF R encUnit s = stateWord R (toScan s) := R:RankedAlphabets:FoldScan Unit⊢ stateWordF R encUnit s = stateWord R (toScan s)
All goals completed! 🐙
At p = 0 the bits a step drops are the recognizer's.
theorem dropCountF_unit (R : RankedAlphabet) (b : Bool) (s : FoldScan Unit) :
dropCountF R 0 b s = dropCount R b (toScan s) := R:RankedAlphabetb:Bools:FoldScan Unit⊢ dropCountF R 0 b s = dropCount R b (toScan s)
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unitlive:Bool⊢ dropCountF R 0 b { buf := buf, stack := stack, live := live } =
dropCount R b (toScan { buf := buf, stack := stack, live := live })
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unitlive:Bool⊢ (match { buf := buf, stack := stack, live := live }.live with
| false => 1 + R.width
| true =>
if (b :: { buf := buf, stack := stack, live := live }.buf).length = R.width then
match symOf R (decodeBits (b :: { buf := buf, stack := stack, live := live }.buf)) with
| none => 1 + R.width
| some i =>
if R.arity i ≤ { buf := buf, stack := stack, live := live }.stack.length then 1 + R.width + (0 + 1) * R.arity i
else 1 + R.width
else 1 + R.width) =
match
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.live with
| false => 1 + R.width
| true =>
match
decide
((b ::
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.buf).length =
R.width) with
| false => 1 + R.width
| true =>
match
R.arOf
(decodeBits
(b ::
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.buf)) with
| none => 1 + R.width
| some r =>
match
decide
(r ≤
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.depth) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unitlive:Bool⊢ (match live with
| false => 1 + R.width
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match live with
| false => 1 + R.width
| true =>
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match false with
| false => 1 + R.width
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match false with
| false => 1 + R.width
| true =>
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + rR:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match true with
| false => 1 + R.width
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match true with
| false => 1 + R.width
| true =>
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match false with
| false => 1 + R.width
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match false with
| false => 1 + R.width
| true =>
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match true with
| false => 1 + R.width
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match true with
| false => 1 + R.width
| true =>
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + rR:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.width⊢ (match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match true with
| false => 1 + R.width
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
match hsym : symOf R (decodeBits (b :: buf)) with
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthhsym:symOf R (decodeBits (b :: buf)) = none⊢ (match none with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match true with
| false => 1 + R.width
| true =>
match Option.map R.arity none with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (match some i with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match true with
| false => 1 + R.width
| true =>
match Option.map R.arity (some i) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (match some i with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match true with
| false => 1 + R.width
| true =>
match some (R.arity i) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match decide (R.arity i ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + R.arity i
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ stack.length⊢ (if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match decide (R.arity i ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + R.arity iR:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:¬R.arity i ≤ stack.length⊢ (if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match decide (R.arity i ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + R.arity i
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ stack.length⊢ (if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match decide (R.arity i ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + R.arity i All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:¬R.arity i ≤ stack.length⊢ (if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width) =
match decide (R.arity i ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + R.arity i All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => 1 + R.width
| some i => if R.arity i ≤ stack.length then 1 + R.width + (0 + 1) * R.arity i else 1 + R.width
else 1 + R.width) =
match decide ((b :: buf).length = R.width) with
| false => 1 + R.width
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => 1 + R.width
| some r =>
match decide (r ≤ stack.length) with
| false => 1 + R.width
| true => 1 + R.width + r All goals completed! 🐙
At p = 0 the bits a step prepends are the recognizer's: an entry is the
single true the pending count pushes.
theorem nextPrefixF_unit (R : RankedAlphabet) (b : Bool) (s : FoldScan Unit) :
nextPrefixF R encUnit (algUnit R) b s = nextPrefix R b (toScan s) := R:RankedAlphabetb:Bools:FoldScan Unit⊢ nextPrefixF R encUnit (algUnit R) b s = nextPrefix R b (toScan s)
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unitlive:Bool⊢ nextPrefixF R encUnit (algUnit R) b { buf := buf, stack := stack, live := live } =
nextPrefix R b (toScan { buf := buf, stack := stack, live := live })
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unitlive:Bool⊢ (match { buf := buf, stack := stack, live := live }.live with
| false => false :: bufBits R { buf := buf, stack := stack, live := live }.buf
| true =>
if (b :: { buf := buf, stack := stack, live := live }.buf).length = R.width then
match symOf R (decodeBits (b :: { buf := buf, stack := stack, live := live }.buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ { buf := buf, stack := stack, live := live }.stack.length then
true :: bufBits R [] ++
entryBits encUnit (algUnit R i fun d ↦ { buf := buf, stack := stack, live := live }.stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: { buf := buf, stack := stack, live := live }.buf)) =
match
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.live with
| false =>
false ::
bufBits R
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.buf
| true =>
match
decide
((b ::
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.buf).length =
R.width) with
| false =>
true ::
bufBits R
(b ::
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.buf)
| true =>
match
R.arOf
(decodeBits
(b ::
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.buf)) with
| none => false :: bufBits R []
| some r =>
match
decide
(r ≤
{ buf := { buf := buf, stack := stack, live := live }.buf,
depth := { buf := buf, stack := stack, live := live }.stack.length,
live := { buf := buf, stack := stack, live := live }.live }.depth) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unitlive:Bool⊢ (match live with
| false => false :: bufBits R buf
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match live with
| false => false :: bufBits R buf
| true =>
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match false with
| false => false :: bufBits R buf
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match false with
| false => false :: bufBits R buf
| true =>
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match true with
| false => false :: bufBits R buf
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match true with
| false => false :: bufBits R buf
| true =>
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match false with
| false => false :: bufBits R buf
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match false with
| false => false :: bufBits R buf
| true =>
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true] All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (match true with
| false => false :: bufBits R buf
| true =>
if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match true with
| false => false :: bufBits R buf
| true =>
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true] R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match R.arOf (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unit⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true] R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.width⊢ (match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match true with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
match hsym : symOf R (decodeBits (b :: buf)) with
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthhsym:symOf R (decodeBits (b :: buf)) = none⊢ (match none with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match true with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity none with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true] All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (match some i with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match true with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity (some i) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (match some i with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match true with
| false => true :: bufBits R (b :: buf)
| true =>
match some (R.arity i) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some i⊢ (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match decide (R.arity i ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match decide (R.arity i ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:¬R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match decide (R.arity i ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match decide (R.arity i ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true] R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:R.arity i ≤ stack.length⊢ true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d]) =
match true with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true]
All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:(b :: buf).length = R.widthi:Fin R.cardhsym:symOf R (decodeBits (b :: buf)) = some ihle:¬R.arity i ≤ stack.length⊢ (if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []) =
match decide (R.arity i ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true] All goals completed! 🐙
R:RankedAlphabetb:Boolbuf:List Boolstack:List Unithlen:¬(b :: buf).length = R.width⊢ (if (b :: buf).length = R.width then
match symOf R (decodeBits (b :: buf)) with
| none => false :: bufBits R []
| some i =>
if h : R.arity i ≤ stack.length then true :: bufBits R [] ++ entryBits encUnit (algUnit R i fun d ↦ stack[↑d])
else false :: bufBits R []
else true :: bufBits R (b :: buf)) =
match decide ((b :: buf).length = R.width) with
| false => true :: bufBits R (b :: buf)
| true =>
match Option.map R.arity (symOf R (decodeBits (b :: buf))) with
| none => false :: bufBits R []
| some r =>
match decide (r ≤ stack.length) with
| false => false :: bufBits R []
| true => true :: bufBits R [] ++ [true] All goals completed! 🐙The fold at the terminal algebra is present exactly on the valid words: the recognizer is the fold's degenerate instance.
theorem foldOut_unit (R : RankedAlphabet) (w : List Bool) :
foldOut R (algUnit R) w = if R.Valid w then some () else none := R:RankedAlphabetw:List Bool⊢ foldOut R (algUnit R) w = if R.Valid w then some () else none
R:RankedAlphabetw:List Boolhv:R.Valid w⊢ foldOut R (algUnit R) w = if R.Valid w then some () else noneR:RankedAlphabetw:List Boolhv:¬R.Valid w⊢ foldOut R (algUnit R) w = if R.Valid w then some () else none
R:RankedAlphabetw:List Boolhv:R.Valid w⊢ foldOut R (algUnit R) w = if R.Valid w then some () else none R:RankedAlphabetw:List Boolhv:R.Valid w⊢ foldOut R (algUnit R) w = some ()
R:RankedAlphabetw:List Boolhv:R.Valid whcond:((foldScanFinal R (algUnit R) w).live && (foldScanFinal R (algUnit R) w).buf.isEmpty &&
(foldScanFinal R (algUnit R) w).stack.length == 1) =
true⊢ foldOut R (algUnit R) w = some ()
R:RankedAlphabetw:List Boolhv:R.Valid whcond:((foldScanFinal R (algUnit R) w).live && (foldScanFinal R (algUnit R) w).buf.isEmpty &&
(foldScanFinal R (algUnit R) w).stack.length == 1) =
trueh1:(foldScanFinal R (algUnit R) w).stack.length = 1⊢ foldOut R (algUnit R) w = some ()
R:RankedAlphabetw:List Boolhv:R.Valid whcond:((foldScanFinal R (algUnit R) w).live && (foldScanFinal R (algUnit R) w).buf.isEmpty &&
(foldScanFinal R (algUnit R) w).stack.length == 1) =
trueh1:(foldScanFinal R (algUnit R) w).stack.length = 1⊢ (if true = true then (foldScanFinal R (algUnit R) w).stack.head? else none) = some ()
match hst : (foldScanFinal R (algUnit R) w).stack with
R:RankedAlphabetw:List Boolhv:R.Valid whcond:((foldScanFinal R (algUnit R) w).live && (foldScanFinal R (algUnit R) w).buf.isEmpty &&
(foldScanFinal R (algUnit R) w).stack.length == 1) =
trueh1:(foldScanFinal R (algUnit R) w).stack.length = 1hst:(foldScanFinal R (algUnit R) w).stack = []⊢ (if true = true then [].head? else none) = some ()
R:RankedAlphabetw:List Boolhv:R.Valid whcond:((foldScanFinal R (algUnit R) w).live && (foldScanFinal R (algUnit R) w).buf.isEmpty &&
(foldScanFinal R (algUnit R) w).stack.length == 1) =
trueh1:[].length = 1hst:(foldScanFinal R (algUnit R) w).stack = []⊢ (if true = true then [].head? else none) = some ()
exact absurd h1 (R:RankedAlphabetw:List Boolhv:R.Valid whcond:((foldScanFinal R (algUnit R) w).live && (foldScanFinal R (algUnit R) w).buf.isEmpty &&
(foldScanFinal R (algUnit R) w).stack.length == 1) =
trueh1:[].length = 1hst:(foldScanFinal R (algUnit R) w).stack = []⊢ ¬[].length = 1 All goals completed! 🐙)
R:RankedAlphabetw:List Boolhv:R.Valid whcond:((foldScanFinal R (algUnit R) w).live && (foldScanFinal R (algUnit R) w).buf.isEmpty &&
(foldScanFinal R (algUnit R) w).stack.length == 1) =
trueh1:(foldScanFinal R (algUnit R) w).stack.length = 1head✝:Unittail✝:List Unithst:(foldScanFinal R (algUnit R) w).stack = head✝ :: tail✝⊢ (if true = true then (head✝ :: tail✝).head? else none) = some () All goals completed! 🐙
R:RankedAlphabetw:List Boolhv:¬R.Valid w⊢ foldOut R (algUnit R) w = if R.Valid w then some () else none R:RankedAlphabetw:List Boolhv:¬R.Valid w⊢ (if R.validBool w = true then (foldScanFinal R (algUnit R) w).stack.head? else none) = none
All goals completed! 🐙
The expression at the terminal algebra decides RankedAlphabet.Valid, its
value pinned on both branches.
theorem foldOutSem_unit_eq_ite (R : RankedAlphabet) (w : List Bool) :
foldOutSem R 0 encUnit decUnit decUnit_encUnit (algUnit R) 1 (one_le_one_mul_width R)
![w] =
if R.Valid w then [true] else [false] := R:RankedAlphabetw:List Bool⊢ foldOutSem R 0 encUnit decUnit decUnit_encUnit (algUnit R) 1 ⋯ ![w] = if R.Valid w then [true] else [false]
R:RankedAlphabetw:List Bool⊢ outWord encUnit (if R.Valid w then some () else none) = if R.Valid w then [true] else [false]
R:RankedAlphabetw:List Boolhv:R.Valid w⊢ outWord encUnit (if R.Valid w then some () else none) = if R.Valid w then [true] else [false]R:RankedAlphabetw:List Boolhv:¬R.Valid w⊢ outWord encUnit (if R.Valid w then some () else none) = if R.Valid w then [true] else [false]
R:RankedAlphabetw:List Boolhv:R.Valid w⊢ outWord encUnit (if R.Valid w then some () else none) = if R.Valid w then [true] else [false] R:RankedAlphabetw:List Boolhv:R.Valid w⊢ outWord encUnit (some ()) = [true]
All goals completed! 🐙
R:RankedAlphabetw:List Boolhv:¬R.Valid w⊢ outWord encUnit (if R.Valid w then some () else none) = if R.Valid w then [true] else [false] R:RankedAlphabetw:List Boolhv:¬R.Valid w⊢ outWord encUnit none = [false]
All goals completed! 🐙end Geb.CobhamFoldend