1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF

Definition source_tm := Eval compute in (TM_from_str "1LB0RD_1LC0RC_1RA1LC_1LE0RB_1LF---_0LA0LE").

Definition hash : DH0 * DH0 := ((B, []), (F, [])).

Lemma hash_U : segRLs source_tm hashes hashes U U.

Lemma hash_A : segRLs source_tm hashes [] A8 B8.

Lemma hash_B : segRLs source_tm hashes hashes B8 A8.

Lemma hash_CAUU :
segRLs source_tm hashes [] (C8 ++ A8 ++ U ++ U) (D8 ++ C8 ++ A8).

Lemma hash_E : segRLs source_tm hashes [] E8 D8.

Lemma hash_D : segRLs source_tm hashes [] D8 A8.

Inductive BDigit := BA | BB.

Definition digit_word (d : BDigit) : list Sym :=
match d with BA => A8 | BB => B8 end.

Fixpoint digits_word (ds : list BDigit) : list Sym :=
match ds with
| [] => []
| d :: ds' => digit_word d ++ digits_word ds'
end.

Fixpoint digits_value (ds : list BDigit) : nat :=
match ds with
| [] => 0
| BA :: ds' => 2 * digits_value ds'
| BB :: ds' => 1 + 2 * digits_value ds'
end.

Fixpoint bfinish_count (ds : list BDigit) (out : nat) : nat :=
match ds with
| [] => out
| BA :: ds' => 2 * bfinish_count ds' out + 1
| BB :: ds' => 2 * bfinish_count ds' out
end.

Lemma bfinish_repeat_BA_formula w out :
bfinish_count (repeat BA w) out = (out + 1) * 2^w - 1.

Lemma hash_A_cycle : segRLs source_tm (hashes^^2) hashes A8 A8.

Lemma hash_B_cycle : segRLs source_tm (hashes^^2) hashes B8 B8.

Lemma hash_A_finish k :
segRLs source_tm (hashes^^(2*k+1)) (hashes^^k) A8 B8.

Lemma hash_B_finish k :
segRLs source_tm (hashes^^(2*k)) (hashes^^k) B8 B8.

Lemma hash_A_cycles k :
segRLs source_tm (hashes^^(2*k)) (hashes^^k) A8 A8.

Lemma hash_E_even n :
segRLs source_tm (hashes^^(2*n+2)) (hashes^^n) E8 A8.

Lemma hash_E_odd n :
segRLs source_tm (hashes^^(2*n+3)) (hashes^^n) E8 B8.

Lemma bfinish_spec ds out :
segRLs source_tm (hashes^^(bfinish_count ds out)) (hashes^^out)
  (digits_word ds) (B8^^length ds).

Lemma hashes_U n : segRLs source_tm (hashes^^n) (hashes^^n) U U.

Lemma hashes_U_run signals width :
segRLs source_tm (hashes^^signals) (hashes^^signals) (U^^width) (U^^width).

Lemma segRLs_0inf {hs input output} :
segRLs source_tm hs [] input output ->
sideRLs source_tm hs (input *> 0inf) (output *> 0inf).

Definition common_left_wall : side :=
0inf <* <[1;0;1;0;0;1;0;0].

Lemma sobc1_emit_hash r :
common_left_wall {{{((F, []), L)}}} r -[source_tm]->+
common_left_wall {{{((B, []), R)}}} (U *> r).

Lemma sobc1_hash_CABAD k :
segRLs source_tm hashes []
  (C8 ++ A8^^k ++ B8 ++ A8 ++ D8)
  (D8 ++ C8^^k ++ B8 ++ U^^2 ++ A8).

Lemma sobc1_hash_CAB1110 k :
segRLs source_tm hashes []
  (C8 ++ A8^^k ++ B8 ++ [1;1;1;0])
  (D8 ++ C8^^k ++ B8 ++ U).

Lemma sobc1_extra_CC :
segRLs source_tm hashes []
  (C8 ++ C8) (D8 ++ A8).

Definition sobc12_left_wall : side :=
0inf <* <[1;0;1;0;0;1;0;0].

Definition sobc1_first_word : list Sym :=
U^^22 ++ A8^^3 ++ D8 ++ C8 ++ A8 ++ U^^28 ++
A8 ++ A8 ++ B8 ++ A8.

Definition sobc1_first_call : Q * tape :=
sobc12_left_wall {{{((B, []), R)}}} (sobc1_first_word *> 0inf).

Lemma sobc1_first_call_reachable :
c0 -[source_tm]->> 24396 / sobc1_first_call.

Definition centered_step (d : Z) : Z := - ((d + 1) / 2).

Lemma centered_step_twice d :
centered_step (centered_step d) = (d + 1) / 4.

Definition pow4 (k : nat) : Z := Z.of_nat (Nat.pow 4 k).

Definition pow2 (k : nat) : Z := Z.of_nat (Nat.pow 2 k).

Lemma pow4_succ k : pow4 (S k) = 4 * pow4 k.

Lemma pow2_pos k : 0 < pow2 k.

Lemma pow2_succ k : pow2 (S k) = 2 * pow2 k.

Theorem centered_converges_2w w d :
(2 <= w)%nat ->
(- pow2 w < d < pow2 w)%Z ->
Nat.iter (2 * w) centered_step d = 0.

Definition stable_column_step (half v : Z) : Z := half - v / 2.

Lemma stable_column_centered half p d :
(2 * half = 3 * p - 1)%Z ->
(p mod 2 = 1)%Z ->
stable_column_step half (p + d) = p + centered_step d.

Lemma stable_column_iter_centered half p n d :
(2 * half = 3 * p - 1)%Z ->
(p mod 2 = 1)%Z ->
Nat.iter n (stable_column_step half) (p + d) =
  p + Nat.iter n centered_step d.

Theorem stable_column_converges_2w half p w v :
(2 <= w)%nat ->
(2 * half = 3 * p - 1)%Z ->
(p mod 2 = 1)%Z ->
(- pow2 w < v - p < pow2 w)%Z ->
Nat.iter (2 * w) (stable_column_step half) v = p.

Definition odd_column_width (k : nat) : nat := (2 * k + 1)%nat.

Definition odd_column_half (k : nat) : Z := pow4 k.

Fixpoint odd_column_fixed (k : nat) : Z :=
match k with O => 1 | S k' => 4 * odd_column_fixed k' - 1 end.

Lemma odd_column_fixed_pos k : 0 < odd_column_fixed k.

Lemma pow2_even_width k : pow2 (2 * k) = pow4 k.

Lemma pow2_odd_width k :
pow2 (odd_column_width k) = 2 * odd_column_half k.

Lemma odd_column_fixed_equation k :
2 * odd_column_half k = 3 * odd_column_fixed k - 1.

Lemma odd_column_fixed_odd k : odd_column_fixed k mod 2 = 1.

Theorem odd_column_converges k v :
(1 <= k)%nat ->
(- pow2 (odd_column_width k) < v - odd_column_fixed k <
   pow2 (odd_column_width k))%Z ->
Nat.iter (2 * odd_column_width k) (stable_column_step (odd_column_half k))
  v = odd_column_fixed k.

Fixpoint initial_u_pair_calls (primary pairs : nat) : nat :=
match pairs with
| O => O
| S pairs' => 2 * 2^primary + initial_u_pair_calls (S primary) pairs'
end.

Definition sobc1_initial_pre_calls : nat :=
2^3 + (initial_u_pair_calls 4 14 +
(2^18 + (2^18 + (2^19 + (2^19 +
(2^21 + (2^21 + 2^22))))))).

Lemma initial_u_pair_calls_formula primary pairs :
initial_u_pair_calls primary pairs =
  2^(primary+1) * (2^pairs-1).

Definition sobc1_first_half : nat := 2^23 + 2^22 + 2^20 - 2.

Lemma sobc1_initial_total_half :
22 + sobc1_initial_pre_calls + (2^24-1) =
  2*sobc1_first_half+1.

Theorem standard_mixed_to_binary_out_spec e ds out :
length ds = S e ->
segRLs source_tm
  (hashes ^^ ((out + 1) * 2 ^ (S e) - 2 + digits_value ds))
  (hashes ^^ out)
  (E8^^e ++ A8)
… +1 lines

Corollary standard_mixed_to_binary_spec e ds :
length ds = S e ->
segRLs source_tm (hashes ^^ (2 ^ (S e) - 2 + digits_value ds)) []
  (E8^^e ++ A8) (digits_word ds).

Lemma prefix_E_even k n input output carries :
segRLs source_tm (hashes^^n) (hashes^^carries) input output ->
segRLs source_tm (hashes^^(2^k*n+2*(2^k-1))) (hashes^^carries)
  (E8^^k ++ input) (A8^^k ++ output).

Definition exception_pre_left (n : nat) : side :=
([1;0;1;0] ++ V4^^(2*n+2) ++ [1;0;1]) *> 0inf.

Definition exception_call_left (remaining finished : nat) : side :=
(X4^^(2*finished+5) ++ V4^^(2*remaining) ++ [1;0;1]) *> 0inf.

Definition exception_raw_source (n w : nat) : Q * tape :=
common_left_wall {{{((B, []), R)}}}
  ((U^^(2*n+1) ++ B8^^(S w) ++ [1;1]) *> 0inf).

Definition exception_pre (n w : nat) : Q * tape :=
exception_pre_left n {{{((F, []), L)}}}
  ((E8^^w ++ A8) *> 0inf).

Lemma raw_U_to_X :
segRR source_tm (B, []) (B, []) U X4.

Lemma segRR_lpow_same h w v k :
segRR source_tm h h w v -> segRR source_tm h h (w^^k) (v^^k).

Lemma raw_Us_to_Xs k :
segRR source_tm (B, []) (B, []) (U^^k) (X4^^k).

Lemma raw_B_forward :
segRR source_tm (B, []) (B, []) B8 Q8.

Lemma raw_B_return l r :
([1;0;1] *> Q8 *> l) {{{((F, []), L)}}} r -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}} (E8 *> r).

Lemma raw_exception_tail_base l :
l {{{((B, []), R)}}} ((B8 ++ [1;1]) *> 0inf) -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}} (A8 *> 0inf).

Lemma raw_exception_tail w l :
l {{{((B, []), R)}}}
    ((B8^^(S w) ++ [1;1]) *> 0inf) -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}}
    ((E8^^w ++ A8) *> 0inf).

Lemma exception_pre_left_direct n :
([1;0;1] *> X4^^(2*n+1) *> Q8 *> 0inf) = exception_pre_left n.

Lemma exception_raw_to_pre n w :
exception_raw_source n w -[source_tm]->* exception_pre n w.

Definition left_hash : DH0 * DH0 := ((F, []), (B, [])).

Lemma left_hash_XX :
segRLs (flip source_tm) [left_hash] [left_hash]
  (X4^^2) (X4^^2).

Lemma left_relaunch_base :
segRLs (flip source_tm) [left_hash] []
  (X4^^5 ++ V4^^2) (X4^^7).

Lemma left_hash_X_pairs k :
segRLs (flip source_tm) [left_hash] [left_hash]
  (X4^^(2*k)) (X4^^(2*k)).

Lemma left_launch_segment :
segRLs (flip source_tm) [left_hash] []
  ([1;0;1;0] ++ V4^^4) (X4^^5).

Lemma exception_launch k :
sideRLs (flip source_tm) [left_hash]
  (exception_pre_left (S k)) (exception_call_left k 0).

Lemma exception_relaunch_side remaining finished :
sideRLs (flip source_tm) [left_hash]
  (exception_call_left (S remaining) finished)
  (exception_call_left remaining (S finished)).

Lemma exception_relaunches k finished :
sideRLs (flip source_tm) ([left_hash]^^k)
  (exception_call_left k finished)
  (exception_call_left 0 (finished+k)).

Lemma exception_calls k input output :
segRLs source_tm (hashes^^(S k)) [] input output ->
exception_call_left k 0 {{{((B, []), R)}}} (input *> 0inf)
  -[source_tm]->+
exception_call_left 0 k {{{((F, []), L)}}} (output *> 0inf).

Definition exception_done (n : nat) (output : list Sym) : Q * tape :=
common_left_wall {{{((B, []), R)}}}
  ((C8 ++ A8 ++ U^^(2*n) ++ output) *> 0inf).

Lemma exception_exit k output :
exception_call_left 0 k {{{((F, []), L)}}} (output *> 0inf)
  -[source_tm]->+ exception_done (S k) output.

Lemma exception_launch_progress k r :
exception_pre_left (S k) {{{((F, []), L)}}} r -[source_tm]->+
exception_call_left k 0 {{{((B, []), R)}}} r.

Lemma exception_exit_zero output :
exception_pre_left 0 {{{((F, []), L)}}} (output *> 0inf)
  -[source_tm]->+ exception_done 0 output.

Lemma exception_pre_from_seg n input output :
segRLs source_tm (hashes^^n) [] input output ->
exception_pre_left n {{{((F, []), L)}}} (input *> 0inf)
  -[source_tm]->+ exception_done n output.

Theorem sobc1_exception_from_seg n w output :
segRLs source_tm (hashes^^n) []
  (E8^^w ++ A8) output ->
exception_raw_source n w -[source_tm]->* exception_done n output.

Fixpoint even_residue (n : nat) : Z :=
match n with
| O => 3
| S n' => 4 * even_residue n' + 1
end.

Fixpoint odd_residue (n : nat) : Z :=
match n with
| O => 26
| S n' => 4 * odd_residue n' - 2
end.

Definition even_residue_width (n : nat) : nat := (2 * n + 4)%nat.

Definition odd_residue_width (n : nat) : nat := (2 * n + 5)%nat.

Lemma even_residue_bounds n :
3 <= even_residue n <= pow2 (even_residue_width n) - 6.

Lemma even_residue_S_lower n : 13 <= even_residue (S n).

Lemma odd_residue_bounds n :
3 <= odd_residue n <= pow2 (odd_residue_width n) - 6.

Lemma odd_residue_complement n :
odd_residue n =
  2 * (pow2 (even_residue_width n) - even_residue n).

Lemma even_residue_complement n :
even_residue (S n) =
  2 * (pow2 (odd_residue_width n) - odd_residue n) + 1.

Lemma low_step_odd_to_even n :
pow2 (even_residue_width n) - odd_residue n / 2 =
  even_residue n.

Lemma low_step_even_to_odd n :
pow2 (odd_residue_width n) - even_residue (S n) / 2 =
  odd_residue n.

Definition z_birth_value (n : nat) : Z :=
2 * (pow2 (even_residue_width (S n)) - even_residue (S n)) + 1.

Definition z_birth_width (n : nat) : nat := (2 * n + 7)%nat.

Lemma z_birth_complement n :
z_birth_value n =
  2 * (pow2 (even_residue_width (S n)) - even_residue (S n)) + 1.

Lemma z_birth_zero : z_birth_value O = 103.

Lemma z_birth_succ n :
z_birth_value (S n) = 4 * z_birth_value n - 5.

Lemma z_birth_bounds n :
3 <= z_birth_value n <= pow2 (z_birth_width n) - 6.

Lemma z_birth_first_low_step n :
pow2 (even_residue_width (S n)) - z_birth_value n / 2 =
  even_residue (S n).

Definition low_slice (total : Z) (m : nat) (r v : Z) : Prop :=
exists high capacity,
  total = capacity * pow2 m /\
  v = high * pow2 m + r /\
  (0 <= high < capacity)%Z.

Lemma low_slice_safe total m r v :
low_slice total m r v ->
(3 <= r <= pow2 m - 6)%Z ->
(3 <= v <= total - 6)%Z.

Lemma low_slice_step total m r v (right_odd : bool) :
low_slice total (S m) r v ->
(3 <= r < pow2 (S m))%Z ->
low_slice total m (pow2 m - r / 2)
  ((if right_odd then total / 2 else total) - v / 2).

Lemma z_birth_low_slice n :
low_slice (pow2 (z_birth_width n)) (z_birth_width n)
  (z_birth_value n) (z_birth_value n).

Inductive LineagePhase :=
| LBirth (n : nat)
| LEven (n : nat)
| LOdd (n : nat).

Definition lineage_width (p : LineagePhase) : nat :=
match p with
| LBirth n => z_birth_width n
| LEven n => even_residue_width n
| LOdd n => odd_residue_width n
end.

Definition lineage_residue (p : LineagePhase) : Z :=
match p with
| LBirth n => z_birth_value n
| LEven n => even_residue n
| LOdd n => odd_residue n
end.

Inductive lineage_next : LineagePhase -> LineagePhase -> Prop :=
| lineage_birth n : lineage_next (LBirth n) (LEven (S n))
| lineage_even n : lineage_next (LEven (S n)) (LOdd n)
| lineage_odd n : lineage_next (LOdd n) (LEven n).

Definition arbitrary_column_step (total : Z) (right_odd : bool) (v : Z) : Z :=
(if right_odd then total / 2 else total) - v / 2.

Lemma lineage_residue_bounds p :
(3 <= lineage_residue p <= pow2 (lineage_width p) - 6)%Z.

Lemma lineage_next_width p p' :
lineage_next p p' -> lineage_width p = S (lineage_width p').

Lemma lineage_next_low_step p p' :
lineage_next p p' ->
pow2 (lineage_width p') - lineage_residue p / 2 =
  lineage_residue p'.

Lemma lineage_step_preserves_slice total p p' v right_odd :
lineage_next p p' ->
low_slice total (lineage_width p) (lineage_residue p) v ->
low_slice total (lineage_width p') (lineage_residue p')
  (arbitrary_column_step total right_odd v).

Definition lineage_fuel (p : LineagePhase) : nat :=
match p with
| LBirth n => 2 * n + 3
| LEven n => 2 * n
| LOdd n => 2 * n + 1
end.

Fixpoint zinputs (total : Z) (inputs : list bool) (v : Z) : Z :=
match inputs with
| [] => v
| b::inputs' => zinputs total inputs' (arbitrary_column_step total b v)
end.

Theorem lineage_inputs_safe total p v inputs :
(length inputs <= lineage_fuel p)%nat ->
low_slice total (lineage_width p) (lineage_residue p) v ->
(3 <= zinputs total inputs v <= total-6)%Z.

Definition ordinary_left (u : nat) : side := X4^^u *> common_left_wall.

Lemma left_emit_zero :
sideRLs (flip source_tm) [left_hash]
  (ordinary_left 0) (ordinary_left 1).

Lemma left_emit_one :
sideRLs (flip source_tm) [left_hash]
  (ordinary_left 1) (ordinary_left 2).

Lemma nat_ind2 (P : nat -> Prop) :
P 0%nat -> P 1%nat ->
(forall n, P n -> P (S (S n))) ->
forall n, P n.

Lemma left_emit_call u :
sideRLs (flip source_tm) [left_hash]
  (ordinary_left u) (ordinary_left (S u)).

Lemma left_emit_calls k u :
sideRLs (flip source_tm) ([left_hash]^^k)
  (ordinary_left u) (ordinary_left (u+k)).

Lemma ordinary_emit_progress u r :
ordinary_left u {{{((F, []), L)}}} r -[source_tm]->+
ordinary_left (S u) {{{((B, []), R)}}} r.

Lemma ordinary_seg_return k u input output r :
segRLs source_tm (hashes^^(S k)) [] input output ->
ordinary_left u {{{((B, []), R)}}} (input *> r) -[source_tm]->+
ordinary_left (u + k) {{{((F, []), L)}}} (output *> r).

Lemma ordinary_seg_run k u input output r :
segRLs source_tm (hashes^^(S k)) [] input output ->
ordinary_left u {{{((B, []), R)}}} (input *> r) -[source_tm]->+
ordinary_left (u + S k) {{{((B, []), R)}}} (output *> r).

Lemma ordinary_seg_run_pos calls u input output r :
1 <= calls -> segRLs source_tm (hashes^^calls) [] input output ->
ordinary_left u {{{((B, []), R)}}} (input *> r) -[source_tm]->+
ordinary_left (u + calls) {{{((B, []), R)}}} (output *> r).

Lemma raw_X_return l r :
(X4 *> l) {{{((F, []), L)}}} r -[source_tm]->+
l {{{((F, []), L)}}} (U *> r).

Lemma raw_X_returns u l r :
(X4^^u *> l) {{{((F, []), L)}}} r -[source_tm]->*
l {{{((F, []), L)}}} (U^^u *> r).

Lemma ordinary_return_wall u r :
ordinary_left u {{{((F, []), L)}}} r -[source_tm]->*
common_left_wall {{{((F, []), L)}}} (U^^u *> r).

Lemma ordinary_seg_to_wall k u input output r :
segRLs source_tm (hashes^^(S k)) [] input output ->
ordinary_left u {{{((B, []), R)}}} (input *> r) -[source_tm]->+
common_left_wall {{{((B, []), R)}}}
  ((U^^(u + S k) ++ output) *> r).

Fixpoint z_tail_digits (n : nat) : list BDigit :=
match n with
| O => [BA; BA; BB; BB]
| S n' => BA :: BB :: z_tail_digits n'
end.

Definition z_digits (n : nat) : list BDigit :=
BB :: BB :: BB :: z_tail_digits n.

Lemma z_tail_digits_length n : length (z_tail_digits n) = 2 * n + 4.

Lemma z_digits_length n : length (z_digits n) = z_birth_width n.

Lemma z_digits_value_zero : digits_value (z_digits O) = 103.

Lemma z_digits_value_succ n :
digits_value (z_digits (S n)) + 5 = 4 * digits_value (z_digits n).

Theorem z_digits_value n :
Z.of_nat (digits_value (z_digits n)) = z_birth_value n.

Theorem digits_exist width value :
value < 2 ^ width ->
exists ds, length ds = width /\ digits_value ds = value.

Lemma cd_start :
segRLs source_tm (hashes^^2) []
  (C8 ++ A8 ++ U^^2) (A8 ++ C8 ++ A8).

Definition cd_calls (n : nat) : nat := 2 * (2^n - 1).

Definition cd_input (n : nat) : list Sym := C8 ++ A8 ++ U^^(2*n).

Definition cd_output (n : nat) : list Sym := A8^^n ++ C8 ++ A8.

Lemma cd_batch n :
segRLs source_tm (hashes^^cd_calls n) []
  (cd_input n) (cd_output n).

Definition after_cd (n : nat) (tail : list Sym) : Q * tape :=
ordinary_left (cd_calls n) {{{((B, []), R)}}}
  ((cd_output n ++ tail) *> 0inf).

Lemma cd_calls_positive n :
1 <= n -> 1 <= cd_calls n.

Lemma exception_done_cd n tail :
1 <= n ->
exception_done n tail -[source_tm]->+ after_cd n tail.

Lemma all_A_cycles width signals :
segRLs source_tm
  (hashes^^(signals * 2^width))
  (hashes^^signals)
  (A8^^width) (A8^^width).

Lemma primary_lift signals width input output :
segRLs source_tm (hashes^^signals) [] input output ->
segRLs source_tm (hashes^^(signals*2^width)) []
  (A8^^width ++ input) (A8^^width ++ output).

Lemma primary_one_rule p w1 w2 :
segRLs source_tm hashes [] w1 w2 ->
segRLs source_tm (hashes^^(2^p)) []
  (A8^^p ++ w1) (A8^^p ++ w2).

Definition ca_pair_calls (width : nat) : nat := 2 * 2^width.

Lemma ca_pair0 : segRLs source_tm (hashes^^2) [] (C8 ++ C8) (A8^^2).

Lemma ca_pair width rest :
segRLs source_tm (hashes^^ca_pair_calls width) []
  (A8^^width ++ C8 ++ C8 ++ rest)
  (A8^^(width+2) ++ rest).

Fixpoint c_sweep_calls (width pairs : nat) : nat :=
match pairs with
| O => O
| S pairs' => ca_pair_calls width + c_sweep_calls (width+2) pairs'
end.

Lemma c_sweep width pairs rest :
segRLs source_tm
  (hashes^^c_sweep_calls width pairs) []
  (A8^^width ++ C8^^(2*pairs+1) ++ rest)
  (A8^^(width+2*pairs) ++ C8 ++ rest).

Definition ca_finish_calls (width : nat) : nat := 4 * 2^width.

Lemma ca_finish0 :
segRLs source_tm (hashes^^4) []
  (C8 ++ B8 ++ U ++ [1;1;1;1] ++ A8 ++ B8 ++ A8)
  (A8^^3 ++ U^^2 ++ B8 ++ B8).

Lemma ca_finish width rest :
segRLs source_tm
  (hashes^^ca_finish_calls width) []
  (A8^^width ++ C8 ++ B8 ++ U ++ [1;1;1;1] ++
    A8 ++ B8 ++ A8 ++ rest)
  (A8^^(width+3) ++ U^^2 ++ B8 ++ B8 ++ rest).

Definition ca_start_calls (width : nat) : nat := 2 * 2^width.

Lemma ca_start0 k :
segRLs source_tm (hashes^^2) []
  (C8 ++ A8^^k ++ B8 ++ B8 ++ A8 ++ B8 ++ A8)
  (A8 ++ C8^^k ++ B8 ++ U ++ [1;1;1;1] ++ A8 ++ B8 ++ A8).

Lemma ca_start width k rest :
segRLs source_tm
  (hashes^^ca_start_calls width) []
  (A8^^width ++ C8 ++ A8^^k ++ B8 ++ B8 ++
    A8 ++ B8 ++ A8 ++ rest)
  (A8^^(width+1) ++ C8^^k ++ B8 ++ U ++ [1;1;1;1] ++
… +1 lines

Definition ca_calls (primary pairs : nat) : nat :=
ca_start_calls primary +
(c_sweep_calls (primary+1) pairs +
 ca_finish_calls (primary+1+2*pairs)).

Lemma ca_batch primary pairs rest :
segRLs source_tm
  (hashes^^ca_calls primary pairs) []
  (A8^^primary ++ C8 ++ A8^^(2*pairs+1) ++
    B8 ++ B8 ++ A8 ++ B8 ++ A8 ++ rest)
  (A8^^(primary+2*pairs+4) ++ U^^2 ++ B8 ++ B8 ++ rest).

Record BinaryColumn := mkBinaryColumn {
  column_e : nat;
  column_digits : list BDigit;
  column_length : length column_digits = S column_e
}.

Definition mixed_column_word (c : BinaryColumn) : list Sym :=
E8^^column_e c ++ A8.

Definition binary_column_word (c : BinaryColumn) : list Sym :=
digits_word (column_digits c).

Definition column_required (out : nat) (c : BinaryColumn) : nat :=
(out + 1) * 2 ^ S (column_e c) - 2 +
  digits_value (column_digits c).

Fixpoint mixed_columns_required (columns : list BinaryColumn) : nat :=
match columns with
| [] => 0
| c :: columns' => column_required (mixed_columns_required columns') c
end.

Fixpoint spaced_words (words : list (list Sym)) : list Sym :=
match words with
| [] => []
| [word] => word
| word :: words' => word ++ U^^2 ++ spaced_words words'
end.

Definition mixed_columns_word columns :=
spaced_words (map mixed_column_word columns).

Definition binary_columns_word columns :=
spaced_words (map binary_column_word columns).

Lemma mixed_column_spec c out :
segRLs source_tm (hashes ^^ column_required out c) (hashes ^^ out)
  (mixed_column_word c) (binary_column_word c).

Theorem mixed_columns_spec columns :
segRLs source_tm (hashes ^^ mixed_columns_required columns) []
  (mixed_columns_word columns) (binary_columns_word columns).

Definition widths_sum (es : list nat) : nat :=
fold_right (fun e n => S e+n) 0%nat es.

Lemma widths_sum_nil : widths_sum [] = 0%nat.

Lemma widths_sum_cons e es : widths_sum (e::es) = S e + widths_sum es.

Definition columns_widths columns := map S (map column_e columns).

Definition columns_width_sum columns :=
fold_right Nat.add 0%nat (columns_widths columns).

Lemma columns_width_sum_cons c columns :
columns_width_sum (c :: columns) = S (column_e c) + columns_width_sum columns.

Lemma columns_width_sum_singleton c :
columns_width_sum [c] = S (column_e c).

Lemma widths_sum_column_es columns :
widths_sum (map column_e columns) = columns_width_sum columns.

Lemma map_S_injective xs ys : map S xs = map S ys -> xs = ys.

Lemma columns_width_sum_positive columns :
columns <> [] -> 1 <= columns_width_sum columns.

Fixpoint geom4n (n : nat) : nat :=
match n with
| O => O
| S n' => 1 + 4 * geom4n n'
end.

Definition half_parameter (n : nat) : nat := 2*n+6.

Definition round_primary_width (current previous : nat) : nat :=
half_parameter current + half_parameter previous + 6.

Definition round_outer_suffix (previous : nat) : list BDigit :=
[BB; BB; BA; BB; BA; BB] ++ z_tail_digits previous.

Definition round_outer_digits (current previous : nat) : list BDigit :=
repeat BA (half_parameter current + 2) ++
  round_outer_suffix previous.

Definition round_post_unary (current previous : nat) : nat :=
cd_calls (half_parameter current) +
  ca_calls (half_parameter current) (previous+4).

Lemma geom4n_succ n : geom4n (S n) = 1 + 4 * geom4n n.

Lemma c_sweep_calls_formula width pairs :
c_sweep_calls width pairs = 2^(width+1) * geom4n pairs.

Lemma ca_calls_formula primary pairs :
ca_calls primary pairs =
  2^(primary+1) +
  (2^(primary+2) * geom4n pairs + 2^(primary+2*pairs+3)).

Lemma cd_calls_formula n :
1 <= n -> cd_calls n = 2^(n+1)-2.

Lemma round_post_unary_formula current previous :
round_post_unary current previous =
  2^(half_parameter current+2) *
    (1 + geom4n (previous+4) + 2^(2*(previous+4)+1)) - 2.

Lemma digits_value_app ds1 ds2 :
digits_value (ds1 ++ ds2) =
  digits_value ds1 + 2^(length ds1) * digits_value ds2.

Lemma digits_value_repeat_BA n : digits_value (repeat BA n) = 0%nat.

Lemma round_outer_suffix_length previous :
length (round_outer_suffix previous) = 2*previous+10.

Lemma round_outer_digits_length current previous :
length (round_outer_digits current previous) =
  round_primary_width current previous.

Lemma round_outer_suffix_zero : digits_value (round_outer_suffix 0) = 811.

Lemma round_outer_suffix_succ previous :
digits_value (round_outer_suffix (S previous)) + 1 =
  4 * digits_value (round_outer_suffix previous).

Lemma round_outer_suffix_formula previous :
2 * digits_value (round_outer_suffix previous) =
  1 + geom4n (previous+4) +
    2^(2*(previous+4)+1) + 2^(2*(previous+4)+2).

Lemma round_outer_digits_value current previous :
digits_value (round_outer_digits current previous) =
  2^(half_parameter current+1) *
    (1 + geom4n (previous+4) +
      2^(2*(previous+4)+1) + 2^(2*(previous+4)+2)).

Theorem round_unary_decodes_outer current previous :
round_post_unary current previous / 2 + 1 +
    2^(round_primary_width current previous-1) =
  digits_value (round_outer_digits current previous).

Lemma digits_word_repeat_BA n : digits_word (repeat BA n) = A8^^(n).

Lemma digits_word_app ds1 ds2 :
digits_word (ds1 ++ ds2) = digits_word ds1 ++ digits_word ds2.

Lemma round_outer_digits_word current previous :
digits_word (round_outer_digits current previous) =
  A8^^(half_parameter current+2) ++
  B8 ++ B8 ++ A8 ++ B8 ++ A8 ++ B8 ++
  digits_word (z_tail_digits previous).

Lemma z_digits_word_split previous :
digits_word (z_digits previous) =
  B8 ++ B8 ++ B8 ++ digits_word (z_tail_digits previous).

Lemma sobc1_B_blank :
sideRLs source_tm hashes
  (B8 *> 0inf) ((E8 ++ [1;1]) *> 0inf).

Lemma sobc1_Bs_blank w :
sideRLs source_tm hashes
  ((B8^^(S w)) *> 0inf)
  ((A8^^w ++ E8 ++ [1;1]) *> 0inf).

Lemma sobc1_As_E w :
sideRLs source_tm (hashes^^(2^w))
  ((A8^^w ++ E8 ++ [1;1]) *> 0inf)
  ((A8^^w ++ D8 ++ [1;1]) *> 0inf).

Lemma sobc1_As_D w :
sideRLs source_tm (hashes^^(2^w))
  ((A8^^w ++ D8 ++ [1;1]) *> 0inf)
  ((A8^^(S w) ++ [1;1]) *> 0inf).

Lemma sobc1_B_edge w :
sideRLs source_tm (hashes^^((2^(S w))+1))
  ((B8^^(S w)) *> 0inf) ((A8^^(S w) ++ [1;1]) *> 0inf).

Lemma all_B_carry w :
segRLs source_tm hashes hashes (B8^^S w) (A8^^S w).

Lemma binary_column_carry_to_zero c out :
segRLs source_tm
  (hashes^^S (bfinish_count (column_digits c) out))
  (hashes^^S out)
  (binary_column_word c) (A8^^S (column_e c)).

Definition all_A_columns_word columns :=
spaced_words (map (fun c => A8^^S (column_e c)) columns).

Lemma binary_columns_word_cons2 c c' columns :
binary_columns_word (c::c'::columns) =
  binary_column_word c ++ U^^2 ++ binary_columns_word (c'::columns).

Lemma all_A_columns_word_cons2 c c' columns :
all_A_columns_word (c::c'::columns) =
  A8^^S (column_e c) ++ U^^2 ++ all_A_columns_word (c'::columns).

Fixpoint columns_frontier_count (columns : list BinaryColumn) : nat :=
match columns with
| [] => 0
| [c] => bfinish_count (column_digits c) 0 +
    2^S (column_e c) + 1
| c :: columns' =>
… +3 lines

Lemma columns_frontier_count_positive columns :
columns <> [] -> 1 <= columns_frontier_count columns.

Theorem binary_columns_to_frontier columns :
columns <> [] ->
sideRLs source_tm
  (hashes^^columns_frontier_count columns)
  ((binary_columns_word columns) *> 0inf)
  ((all_A_columns_word columns ++ [1;1]) *> 0inf).

Lemma raw_separator_return l r :
([1;0;1] *> X4^^2 *> Q8 *> l) {{{((F, []), L)}}} r
  -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}}
  ((A8 ++ U^^2) *> r).

Lemma raw_Bs_to_Qs k :
segRR source_tm (B, []) (B, []) (B8^^k) (Q8^^k).

Lemma raw_B_returns k l r :
([1;0;1] *> Q8^^k *> l) {{{((F, []), L)}}} r
  -[source_tm]->*
([1;0;1] *> l) {{{((F, []), L)}}} (E8^^k *> r).

Definition full_exception_columns es :=
spaced_words (map (fun e => B8^^S e) es) ++ [1;1].

Definition initialized_mixed_columns es :=
spaced_words (map (fun e => E8^^e ++ A8) es).

Lemma full_exception_columns_cons2 e e' es :
full_exception_columns (e::e'::es) =
  B8^^S e ++ U^^2 ++ full_exception_columns (e'::es).

Lemma initialized_mixed_columns_cons2 e e' es :
initialized_mixed_columns (e::e'::es) =
  (E8^^e ++ A8) ++ U^^2 ++ initialized_mixed_columns (e'::es).

Lemma raw_exception_columns es l :
es <> [] ->
l {{{((B, []), R)}}} (full_exception_columns es *> 0inf)
  -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}}
  (initialized_mixed_columns es *> 0inf).

Definition exception_columns_raw_source (n : nat) (es : list nat) : Q * tape :=
common_left_wall {{{((B, []), R)}}}
  ((U^^(2*n+1) ++ full_exception_columns es) *> 0inf).

Definition exception_columns_pre (n : nat) (es : list nat) : Q * tape :=
exception_pre_left n {{{((F, []), L)}}}
  (initialized_mixed_columns es *> 0inf).

Lemma exception_columns_raw_to_pre n es :
es <> [] ->
exception_columns_raw_source n es -[source_tm]->*
  exception_columns_pre n es.

Theorem sobc1_exception_columns_from_seg n es output :
es <> [] ->
segRLs source_tm (hashes^^n) []
  (initialized_mixed_columns es) output ->
exception_columns_raw_source n es -[source_tm]->*
  exception_done n output.

Lemma initialized_mixed_columns_eq es columns :
columns_widths columns = map S es ->
initialized_mixed_columns es = mixed_columns_word columns.

Lemma digits_value_BBBA_pairs k :
digits_value ([BB; BA]^^k) = geom4n k.

Definition sobc1_second_tail_digits : list BDigit :=
[BB] ++ ([BB; BA]^^9) ++ [BA; BB; BB; BB; BA].

Lemma sobc1_second_tail_length :
length sobc1_second_tail_digits = 24.

Lemma sobc1_second_tail_value :
2 * digits_value sobc1_second_tail_digits =
  1 + geom4n 10 + 7 * 2^21.

Lemma primary_D_absorb primary rest :
segRLs source_tm (hashes^^(2^primary)) []
  (A8^^primary ++ D8 ++ rest)
  (A8^^(S primary) ++ rest).

Lemma initial_u_pairs primary pairs rest :
segRLs source_tm
  (hashes^^initial_u_pair_calls primary pairs) []
  (A8^^primary ++ C8 ++ A8 ++ U^^(2*pairs) ++ rest)
  (A8^^(primary+pairs) ++ C8 ++ A8 ++ rest).

Lemma primary_one_side_rule primary input output :
sideRLs source_tm hashes input output ->
sideRLs source_tm (hashes^^(2^primary))
  ((A8^^primary) *> input) ((A8^^primary) *> output).

Lemma bfinish_count_app ds1 ds2 out :
bfinish_count (ds1 ++ ds2) out =
  bfinish_count ds1 (bfinish_count ds2 out).

Lemma primary_single_B_D low :
segRLs source_tm (hashes^^(2^low)) []
  (A8^^low ++ B8 ++ D8 ++ [1;1])
  (A8^^(low+2) ++ [1;1]).

Lemma sobc1_initial_pre_side :
sideRLs source_tm
  (hashes^^sobc1_initial_pre_calls)
  ((A8^^3 ++ D8 ++ C8 ++ A8 ++ U^^28 ++
    A8 ++ A8 ++ B8 ++ A8) *> 0inf)
  ((A8^^24 ++ [1;1]) *> 0inf).

Lemma zero_primary_finish_seg width rest :
segRLs source_tm (hashes^^(2^width-1)) []
  (A8^^width ++ rest) (B8^^width ++ rest).

Lemma ordinary_all_A_to_exception width u n :
1 <= width -> u+(2^width-1) = 2*n+1 ->
ordinary_left u {{{((B, []), R)}}}
  ((A8^^width ++ [1;1]) *> 0inf) -[source_tm]->+
exception_raw_source n (width-1).

Lemma sobc1_first_call_to_exception :
sobc1_first_call -[source_tm]->*
  exception_raw_source sobc1_first_half 23.

Lemma bfinish_count_value ds out :
bfinish_count ds out + digits_value ds + 1 =
  (out+1) * 2^(length ds).

Lemma digits_value_bound ds :
digits_value ds < 2^(length ds).

Lemma digits_value_BB_BB_lower ds : 3 <= digits_value (BB :: BB :: ds).

Lemma digits_value_BB_odd ds : Nat.odd (digits_value (BB :: ds)) = true.

Lemma digits_value_msb_BA_safe ds :
3 <= length ds ->
digits_value (ds ++ [BA]) <= 2^(length (ds ++ [BA]))-6.

Lemma binary_column_value_bound c :
digits_value (column_digits c) < 2^S (column_e c).

Definition columns_frontier_next (columns : list BinaryColumn) : nat :=
match columns with
| [] => 2
| _ => columns_frontier_count columns
end.

Lemma columns_frontier_head_equation c columns :
columns_frontier_count (c :: columns) +
    digits_value (column_digits c) =
  columns_frontier_next columns * 2^S (column_e c).

Lemma pow2_S_odd_false n : Nat.odd (2^S n) = false.

Lemma columns_frontier_head_parity c columns :
Nat.odd (columns_frontier_count (c :: columns)) =
Nat.odd (digits_value (column_digits c)).

Definition post_ca_side (primary : nat) (columns : list BinaryColumn) : side :=
((A8^^primary ++ U^^2 ++ binary_columns_word columns) *> 0inf).

Definition all_A_frontier_side
  (primary : nat) (columns : list BinaryColumn) : side :=
((A8^^primary ++ U^^2 ++ all_A_columns_word columns ++ [1;1]) *>
  0inf).

Definition post_ca_state
  (unary primary : nat) (columns : list BinaryColumn) : Q * tape :=
ordinary_left unary {{{((B, []), R)}}} (post_ca_side primary columns).

Definition all_A_frontier_state
  (unary primary : nat) (columns : list BinaryColumn) : Q * tape :=
ordinary_left unary {{{((B, []), R)}}}
  (all_A_frontier_side primary columns).

Definition post_to_frontier_calls
  (primary : nat) (columns : list BinaryColumn) : nat :=
columns_frontier_count columns * 2^primary.

Lemma post_ca_to_frontier_side primary columns :
columns <> [] ->
sideRLs source_tm
  (hashes^^post_to_frontier_calls primary columns)
  (post_ca_side primary columns)
  (all_A_frontier_side primary columns).

Theorem post_ca_to_frontier unary primary columns :
columns <> [] ->
post_ca_state unary primary columns -[source_tm]->*
all_A_frontier_state
  (unary + post_to_frontier_calls primary columns) primary columns.

Definition all_A_widths_word es :=
spaced_words (map (fun e => A8^^S e) es).

Lemma all_A_widths_word_cons2 e e' es :
all_A_widths_word (e::e'::es) =
  A8^^S e ++ U^^2 ++ all_A_widths_word (e'::es).

Lemma all_A_width_finish e out :
segRLs source_tm (hashes^^((out+1)*2^(S e)-1)) (hashes^^out)
  (A8^^S e) (B8^^S e).

Lemma all_A_widths_finish es :
es <> [] -> segRLs source_tm (hashes^^(2^(widths_sum es)-1)) []
  (all_A_widths_word es ++ [1;1]) (full_exception_columns es).

Lemma all_A_widths_to_exception es u n r :
es <> [] -> u + (2^(widths_sum es)-1) = 2*n+1 ->
ordinary_left u {{{((B, []), R)}}}
    ((all_A_widths_word es ++ [1;1]) *> r) -[source_tm]->+
common_left_wall {{{((B, []), R)}}}
    ((U^^(2*n+1) ++ full_exception_columns es) *> r).

Definition sobc1_middle_width (n : nat) : nat := n+26.

Definition sobc1_before_second_finish_calls (n : nat) : nat :=
2^n + (2^n + (c_sweep_calls (n+1) 10 +
(2^(n+21) + (2^(n+21) +
((13*2^(n+22)-1) + (2^(n+26)+1)))))).

Definition sobc1_middle_index : nat :=
2^22 + 2^21 + 2^19 - 4.

Lemma sobc1_middle_index_half :
half_parameter sobc1_middle_index = sobc1_first_half.

Definition sobc1_second_digits_at (n : nat) : list BDigit :=
repeat BA (n+2) ++ sobc1_second_tail_digits.

Lemma sobc1_second_digits_at_length n :
length (sobc1_second_digits_at n) = sobc1_middle_width n.

Lemma sobc1_second_digits_at_value n :
digits_value (sobc1_second_digits_at n) =
  2^(n+2) * digits_value sobc1_second_tail_digits.

Definition sobc1_second_digits : list BDigit :=
sobc1_second_digits_at sobc1_first_half.

Definition sobc1_second_half : nat :=
2^sobc1_middle_width sobc1_first_half - 2 +
  digits_value sobc1_second_digits.

Lemma sobc1_second_digits_length :
length sobc1_second_digits = sobc1_middle_width sobc1_first_half.

Lemma sobc1_second_total_general n :
1 <= n ->
cd_calls n + sobc1_before_second_finish_calls n +
    (2^sobc1_middle_width n-1) =
  2*(2^sobc1_middle_width n-2 +
    digits_value (sobc1_second_digits_at n))+1.

Lemma sobc1_second_total_half :
cd_calls sobc1_first_half +
    sobc1_before_second_finish_calls sobc1_first_half +
    (2^sobc1_middle_width sobc1_first_half-1) =
  2*sobc1_second_half+1.

Definition column_value (c : BinaryColumn) : nat :=
digits_value (column_digits c).

Definition column_width (c : BinaryColumn) : nat := S (column_e c).

Definition column_safe (c : BinaryColumn) : Prop :=
3 <= column_value c /\ column_value c <= 2^(column_width c)-6.

Lemma column_safe_lower c : column_safe c -> 3 <= column_value c.

Definition column_next_value (right_odd : bool) (c : BinaryColumn) : nat :=
(if right_odd then 2^(column_e c) else 2^(S (column_e c))) -
  column_value c / 2.

Definition column_step
  (right_odd : bool) (c c' : BinaryColumn) : Prop :=
column_e c' = column_e c /\
column_value c' = column_next_value right_odd c.

Fixpoint columns_step
  (columns columns' : list BinaryColumn) : Prop :=
match columns, columns' with
| [c], [c'] => column_step true c c'
| c :: d :: tail, c' :: rest' =>
    column_step (Nat.odd (column_value d)) c c' /\
… +3 lines

Lemma column_next_value_bound right_odd c :
3 <= column_value c ->
column_next_value right_odd c < 2^(column_width c).

Lemma column_step_exists right_odd c :
3 <= column_value c ->
exists c', column_step right_odd c c'.

Theorem columns_step_exists columns :
columns <> [] ->
Forall column_safe columns ->
exists columns', columns_step columns columns'.

Lemma columns_step_nonempty columns columns' :
columns_step columns columns' -> columns <> [] /\ columns' <> [].

Lemma columns_step_widths columns columns' :
columns_step columns columns' ->
columns_widths columns' = columns_widths columns.

Definition ceil_half (n : nat) : nat := (n+1)/2.

Lemma odd_true_witness n :
Nat.odd n = true -> exists q, n = 2*q+1.

Lemma ceil_half_odd q : ceil_half (2*q+1) = q+1.

Lemma ceil_half_scaled_sub t w v :
1 <= t -> 1 <= w -> v < 2^w ->
ceil_half (t*2^w-v) = t*2^(w-1)-v/2.

Lemma frontier_ceil_half c columns :
ceil_half (columns_frontier_count (c :: columns)) +
    column_value c / 2 =
  columns_frontier_next columns * 2^(column_e c).

Lemma odometer_cons_arith e s tailF tailR v v' :
1 <= s -> 1 <= tailF -> v < 2^(S e) ->
tailR+2 = 2^(s-1)+ceil_half tailF ->
v' = (if Nat.odd tailF then 2^e else 2^(S e))-v/2 ->
(tailR+1)*2^(S e)-2+v'+2 =
  2^(S e+s-1)+ceil_half (tailF*2^(S e)-v).

Lemma columns_step_width_sum columns columns' :
columns_step columns columns' ->
columns_width_sum columns' = columns_width_sum columns.

Theorem columns_step_required columns columns' :
columns_step columns columns' ->
mixed_columns_required columns' + 2 =
  2^(columns_width_sum columns - 1) +
    ceil_half (columns_frontier_count columns).

Lemma round_primary_width_positive current previous :
1 <= round_primary_width current previous.

Definition round_outer_column (current previous : nat) : BinaryColumn.

Lemma round_outer_column_word current previous :
binary_column_word (round_outer_column current previous) =
  A8^^(half_parameter current+2) ++
  B8 ++ B8 ++ A8 ++ B8 ++ A8 ++ B8 ++
  digits_word (z_tail_digits previous).

Lemma round_post_unary_half_formula current previous :
round_post_unary current previous / 2 =
  2^(half_parameter current+1) *
    (1 + geom4n (previous+4) + 2^(2*(previous+4)+1)) - 1.

Definition round_frontier_unary
  (current previous : nat) (columns : list BinaryColumn) : nat :=
round_post_unary current previous +
  columns_frontier_count columns *
    2^(round_primary_width current previous).

Definition round_next_half
  (current previous : nat) (columns : list BinaryColumn) : nat :=
round_frontier_unary current previous columns / 2 +
  2^(round_primary_width current previous +
    columns_width_sum columns - 1) - 1.

Lemma round_frontier_unary_half current previous columns :
round_frontier_unary current previous columns / 2 =
round_post_unary current previous / 2 +
  columns_frontier_count columns *
    2^(round_primary_width current previous-1).

Definition round_next_index current previous columns : nat :=
(round_next_half current previous columns - 6) / 2.

Lemma round_next_half_even_ge6 current previous columns :
columns <> [] ->
exists k, round_next_half current previous columns = 2*k /\ 6 <= 2*k.

Lemma round_next_half_parameter current previous columns :
columns <> [] ->
round_next_half current previous columns =
  half_parameter (round_next_index current previous columns).

Definition columns_head_odd (columns : list BinaryColumn) : Prop :=
match columns with
| [] => False
| c :: _ => Nat.odd (column_value c) = true
end.

Theorem round_output_required current previous columns columns' :
columns <> [] ->
columns_step columns columns' ->
columns_head_odd columns ->
mixed_columns_required
    (round_outer_column current previous :: columns') =
… +1 lines

Definition frontier_es
  (current previous : nat) (columns : list BinaryColumn) : list nat :=
(round_primary_width current previous-1) :: map column_e columns.

Definition round_output_columns current previous columns' :=
round_outer_column current previous :: columns'.

Lemma round_frontier_exception_equation current previous columns :
columns <> [] ->
round_frontier_unary current previous columns+
    (2^(round_primary_width current previous+
      columns_width_sum columns)-1) =
  2*round_next_half current previous columns+1.

Theorem all_A_frontier_to_exception_done
  current previous columns columns' :
columns <> [] ->
columns_step columns columns' ->
columns_head_odd columns ->
all_A_frontier_state
… +6 lines

Definition z_column (previous : nat) : BinaryColumn.

Lemma z_column_word previous :
binary_column_word (z_column previous) = digits_word (z_digits previous).

Lemma z_column_e previous : column_e (z_column previous) =
half_parameter previous.

Lemma binary_columns_word_cons c columns :
columns <> [] ->
binary_columns_word (c :: columns) =
  binary_column_word c ++ U^^2 ++ binary_columns_word columns.

Lemma ca_calls_positive primary pairs : 1 <= ca_calls primary pairs.

Lemma exception_done_ca n pairs rest :
1 <= n ->
exception_done n
  (A8^^(2*pairs) ++ B8++B8++A8++B8++A8++rest) -[source_tm]->+
ordinary_left (cd_calls n + ca_calls n pairs) {{{((B, []), R)}}}
  ((A8^^(n+2*pairs+4) ++ U^^2 ++ B8++B8++rest) *> 0inf).

Theorem exception_done_to_next_post
  current previous columns columns' :
columns <> [] ->
columns_step columns columns' ->
exception_done (round_next_half current previous columns)
    (binary_columns_word
… +8 lines

Theorem sobc1_canonical_round
  current previous columns columns' :
columns <> [] ->
columns_head_odd columns ->
columns_step columns columns' ->
post_ca_state (round_post_unary current previous)
… +8 lines

Definition round_width_dominance
  (current previous : nat) (columns : list BinaryColumn) : Prop :=
2 * columns_width_sum columns + 4 <= half_parameter previous + 1 /\
2 * (half_parameter previous + 1 + columns_width_sum columns) + 4 <=
  half_parameter current + 1.

Lemma pow2_linear_margin n : 2*n+8 <= 2^(n+5).

Lemma output_columns_width_sum previous columns columns' :
columns_step columns columns' ->
columns_width_sum (z_column previous :: columns') =
  half_parameter previous + 1 + columns_width_sum columns.

Lemma round_next_half_growth current previous columns :
columns <> [] ->
2 * (half_parameter current + 1 +
    (half_parameter previous + 1 + columns_width_sum columns)) + 4 <=
  round_next_half current previous columns + 1.

Theorem round_width_dominance_step
  current previous columns columns' :
columns <> [] ->
columns_step columns columns' ->
round_width_dominance current previous columns ->
round_width_dominance
… +2 lines

Lemma z_column_width previous :
column_width (z_column previous) = z_birth_width previous.

Lemma z_column_value previous :
Z.of_nat (column_value (z_column previous)) = z_birth_value previous.

Lemma z_birth_value_odd n : (z_birth_value n mod 2 = 1)%Z.

Lemma Zodd_of_nat n : Z.odd (Z.of_nat n) = Nat.odd n.

Lemma z_column_odd previous :
Nat.odd (column_value (z_column previous)) = true.

Record AbstractColumn := mkAbstractColumn {
  abstract_width : nat;
  abstract_value : Z;
}.

Definition abstract_of_column (c : BinaryColumn) : AbstractColumn :=
mkAbstractColumn (column_width c) (Z.of_nat (column_value c)).

Definition abstract_safe (c : AbstractColumn) : Prop :=
(3 <= abstract_value c <= pow2 (abstract_width c)-6)%Z.

Definition abstract_step (right_odd : bool) (c : AbstractColumn) : AbstractColumn :=
mkAbstractColumn (abstract_width c)
  (arbitrary_column_step (pow2 (abstract_width c)) right_odd (abstract_value c)).

Fixpoint abstract_columns_next (columns : list AbstractColumn) : list AbstractColumn :=
match columns with
| [] => []
| c :: rest =>
    match rest with
    | [] => [abstract_step true c]
… +3 lines

Definition abstract_columns_iter n columns :=
Nat.iter n abstract_columns_next columns.

Definition abstract_head_odd (columns : list AbstractColumn) : Prop :=
match columns with [] => False | c::_ => Z.odd (abstract_value c) = true end.

Definition abstract_columns_safe := Forall abstract_safe.

Definition abstract_suffix_good (settle : nat) (columns : list AbstractColumn) : Prop :=
columns <> [] /\
(forall n, abstract_columns_safe (abstract_columns_iter n columns)) /\
(forall n, settle <= n -> abstract_head_odd (abstract_columns_iter n columns)).

Lemma hd_nonempty {A} (x y : A) xs : xs <> [] -> hd x xs = hd y xs.

Lemma abstract_columns_next_nonempty columns : columns <> [] -> abstract_columns_next columns <> [].

Lemma abstract_columns_iter_nonempty n columns : columns <> [] -> abstract_columns_iter n columns <> [].

Lemma abstract_columns_iter_succ_right n columns : abstract_columns_next (abstract_columns_iter n columns) = abstract_columns_iter (S n) columns.

Lemma abstract_columns_iter_succ_left n columns :
abstract_columns_iter n (abstract_columns_next columns) =
abstract_columns_iter (S n) columns.

Lemma abstract_columns_iter_add m n columns : abstract_columns_iter (m+n) columns = abstract_columns_iter n (abstract_columns_iter m columns).

Lemma abstract_columns_next_cons c columns :
columns <> [] ->
abstract_columns_next (c::columns) =
  abstract_step (Z.odd (abstract_value (hd c columns))) c :: abstract_columns_next columns.

Lemma abstract_columns_iter_cons n c columns :
columns <> [] -> exists c',
  abstract_columns_iter n (c::columns) =
    c'::abstract_columns_iter n columns.

Lemma abstract_columns_iter_head_width n c columns :
columns <> [] -> abstract_width (hd c (abstract_columns_iter n (c::columns))) = abstract_width c.

Lemma column_safe_abstract c : column_safe c <-> abstract_safe (abstract_of_column c).

Lemma columns_safe_abstract columns :
Forall column_safe columns <-> abstract_columns_safe (map abstract_of_column columns).

Lemma abstract_column_step c c' right_odd :
column_safe c -> column_step right_odd c c' ->
abstract_of_column c' = abstract_step right_odd (abstract_of_column c).

Lemma columns_step_abstract columns columns' :
Forall column_safe columns ->
columns_step columns columns' ->
map abstract_of_column columns' = abstract_columns_next (map abstract_of_column columns).

Fixpoint abstract_head_inputs (n : nat) (columns : list AbstractColumn) : list bool :=
match n with
| O => []
| S n' =>
    match columns with
    | [] => []
… +3 lines

Lemma abstract_head_inputs_length n columns :
columns <> [] -> length (abstract_head_inputs n columns) = n.

Definition abstract_birth birth := mkAbstractColumn (z_birth_width birth) (z_birth_value birth).

Lemma abstract_birth_eq birth : abstract_birth birth = abstract_of_column (z_column birth).

Lemma abstract_iter_head_value c columns n :
columns <> [] ->
abstract_value (hd c (abstract_columns_iter n (c::columns))) =
  zinputs (pow2 (abstract_width c)) (abstract_head_inputs n columns) (abstract_value c).

Theorem abstract_birth_early_safe birth columns n :
columns <> [] -> n <= z_birth_width birth-4 ->
abstract_safe (hd (abstract_birth birth) (abstract_columns_iter n (abstract_birth birth::columns))).

Lemma stable_step_safe_Z width value :
4 <= width ->
(3 <= value <= pow2 width-6)%Z ->
(3 <= stable_column_step (pow2 (width-1)) value <= pow2 width-6)%Z.

Lemma zinputs_repeat_true total n value :
zinputs total (repeat true n) value =
  Nat.iter n (arbitrary_column_step total true) value.

Lemma arbitrary_true_iter width n value :
1 <= width ->
Nat.iter n (arbitrary_column_step (pow2 width) true) value =
Nat.iter n (stable_column_step (pow2 (width-1))) value.

Lemma arbitrary_true_iter_safe width n value :
4 <= width ->
(3 <= value <= pow2 width-6)%Z ->
(3 <= Nat.iter n (arbitrary_column_step (pow2 width) true) value <=
  pow2 width-6)%Z.

Theorem z_odd_width_converges_odd k value :
2 <= k ->
(3 <= value <= pow2 (odd_column_width k)-6)%Z ->
Z.odd (Nat.iter (2*odd_column_width k)
  (arbitrary_column_step (pow2 (odd_column_width k)) true) value) = true.

Lemma abstract_suffix_good_inputs settle columns q n :
abstract_suffix_good settle columns -> settle <= q ->
abstract_head_inputs n (abstract_columns_iter q columns) = repeat true n.

Lemma abstract_safe_width c : abstract_safe c -> 4 <= abstract_width c.

Theorem abstract_suffix_good_prepend_birth settle columns birth :
abstract_suffix_good settle columns ->
settle <= z_birth_width birth-4 ->
abstract_suffix_good (settle+2*z_birth_width birth) (abstract_birth birth::columns).

Lemma abstract_singleton_iter n c :
abstract_columns_iter n [c] =
[mkAbstractColumn (abstract_width c)
  (Nat.iter n (arbitrary_column_step (pow2 (abstract_width c)) true) (abstract_value c))].

Theorem abstract_singleton_good k c :
abstract_width c = odd_column_width k -> abstract_safe c ->
abstract_suffix_good (2*abstract_width c) [c].

Lemma abstract_suffix_good_shift settle columns :
abstract_suffix_good settle columns ->
abstract_suffix_good (Nat.pred settle) (abstract_columns_next columns).

Definition columns_schedule (columns : list BinaryColumn) : Prop :=
exists settle,
  abstract_suffix_good settle (map abstract_of_column columns) /\
  settle <= 2 * columns_width_sum columns.

Definition sobc1_round_invariant
  (current previous : nat) (columns : list BinaryColumn) : Prop :=
round_width_dominance current previous columns /\
columns_schedule columns /\
columns_head_odd columns.

Theorem sobc1_round_invariant_progress current previous columns :
sobc1_round_invariant current previous columns ->
exists columns',
  post_ca_state (round_post_unary current previous)
      (round_primary_width current previous) columns
    -[source_tm]->+
… +9 lines

Theorem sobc1_canonical_nonhalt current previous columns :
sobc1_round_invariant current previous columns ->
~ halts source_tm
  (post_ca_state (round_post_unary current previous)
    (round_primary_width current previous) columns).

Definition sobc1_second_base : nat :=
2^(sobc1_first_half+25)-1 +
  2^(sobc1_first_half+1) *
    digits_value sobc1_second_tail_digits.

Definition sobc1_current_index : nat := sobc1_second_base-3.

Lemma double_pred_sum_mul a b c :
1 <= a -> 2*a-2+2*b*c = 2*(a-1+b*c).

Lemma sobc1_second_half_double_at n :
2^sobc1_middle_width n-2 + digits_value (sobc1_second_digits_at n) =
2*(2^(n+25)-1 + 2^(n+1)*digits_value sobc1_second_tail_digits).

Lemma sobc1_second_half_double :
sobc1_second_half = 2*sobc1_second_base.

Lemma second_base_ge3_at n v :
3 <= 2^(n+25)-1 + 2^(n+1)*v.

Lemma sobc1_second_base_ge3 : 3 <= sobc1_second_base.

Lemma half_parameter_pred3 n :
3 <= n -> half_parameter (n-3) = 2*n.

Lemma sobc1_current_index_half :
half_parameter sobc1_current_index = sobc1_second_half.

Lemma sobc1_first_half_large : 46 <= sobc1_first_half+1.

Lemma entry_current_dominance n v :
2*(n+22)+4 <= 2*(2^(n+25)-1+2^(n+1)*v)+1.

Definition sobc1_entry_rest : list BDigit :=
([BB; BA]^^7) ++ [BA; BB; BB; BB; BA].

Definition sobc1_entry_digits : list BDigit :=
[BB; BB] ++ sobc1_entry_rest.

Lemma sobc1_second_digits_split :
sobc1_second_digits =
  repeat BA (sobc1_first_half+2) ++
    [BB; BB; BA; BB; BA] ++ sobc1_entry_rest.

Definition sobc1_entry_column : BinaryColumn :=
mkBinaryColumn 20 sobc1_entry_digits ltac:(
  unfold sobc1_entry_digits, sobc1_entry_rest;
  rewrite !length_app, lpow_length; reflexivity).

Lemma sobc1_entry_column_facts :
column_width sobc1_entry_column = odd_column_width 10 /\
column_safe sobc1_entry_column /\
Nat.odd (column_value sobc1_entry_column) = true.

Theorem sobc1_entry_invariant :
sobc1_round_invariant sobc1_current_index sobc1_middle_index
  [sobc1_entry_column].

Definition sobc1_first_output : list Sym :=
A8^^20 ++ B8 ++ A8 ++ D8 ++ A8.

Lemma sobc1_first_exception_seg :
segRLs source_tm (hashes^^sobc1_first_half) []
  (E8^^23 ++ A8) sobc1_first_output.

Definition sobc1_middle_digits (n : nat) : list BDigit :=
repeat BA (n+22) ++ [BB; BB; BA; BA].

Lemma sobc1_middle_digits_word n :
digits_word (sobc1_middle_digits n) =
  A8^^(n+22) ++ B8 ++ B8 ++ A8 ++ A8.

Lemma sobc1_middle_digits_length n :
length (sobc1_middle_digits n) = sobc1_middle_width n.

Lemma sobc1_middle_finish_count n :
bfinish_count (sobc1_middle_digits n) 0 =
  13 * 2^(n+22) - 1.

Lemma sobc1_middle_to_zero_edge n :
sideRLs source_tm
  (hashes^^
    (13*2^(n+22)-1 + (2^(n+26)+1)))
  ((digits_word (sobc1_middle_digits n)) *> 0inf)
  ((A8^^(n+26) ++ [1;1]%sym) *> 0inf).

Lemma sobc1_initial_blank_bridge :
sideRLs source_tm hashes
  ((C8 ++ B8 ++ U^^2 ++ A8^^2) *> 0inf)
  ((D8 ++ B8 ++ B8 ++ A8 ++ A8) *> 0inf).

Lemma sobc1_after_cd_to_before_second_finish_side n :
sideRLs source_tm
  (hashes^^sobc1_before_second_finish_calls n)
  ((A8^^n ++ C8 ++ A8 ++ sobc1_first_output) *> 0inf)
  ((A8^^sobc1_middle_width n ++ [1;1]%sym) *> 0inf).

Lemma sobc1_after_cd_to_before_second_finish n :
after_cd n sobc1_first_output -[source_tm]->*
ordinary_left (cd_calls n+sobc1_before_second_finish_calls n)
  {{{((B, []), R)}}}
  ((A8^^sobc1_middle_width n++[1;1]) *> 0inf).

Theorem sobc1_first_done_to_second_exception :
exception_done sobc1_first_half sobc1_first_output -[source_tm]->*
  exception_raw_source sobc1_second_half (sobc1_first_half+25).

Lemma sobc1_second_tail_word :
digits_word sobc1_second_digits =
A8^^(2*(sobc1_middle_index+4)) ++
  B8++B8++A8++B8++A8++digits_word sobc1_entry_rest.

Lemma sobc1_entry_primary_width :
sobc1_second_half + 2*(sobc1_middle_index+4)+4 =
  round_primary_width sobc1_current_index sobc1_middle_index.

Theorem sobc1_c0_to_entry_post :
c0 -[source_tm]->*
post_ca_state
  (round_post_unary sobc1_current_index sobc1_middle_index)
  (round_primary_width sobc1_current_index sobc1_middle_index)
  [sobc1_entry_column].

Theorem sobc1_nonhalt : ~ halts source_tm c0.

Definition y_after (k : nat) : list Sym :=
match k with
| 0%nat => A8
| 1%nat => B8
| 2%nat => E8 ++ [1;1]
| 3%nat => D8 ++ [1;1]
… +3 lines

Definition tail_word (k : nat) : list Sym := U^^(2*k+1) ++ B8 ++ [1;1].

Lemma raw_tail_base k l : k <= 5 ->
l {{{((B, []), R)}}} ((B8 ++ U^^(2*k+1) ++ B8 ++ [1;1]) *> 0inf)
  -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}} ((U^^(2*k+3) ++ y_after k) *> 0inf).

Lemma raw_tail_column k e l : k <= 5 ->
l {{{((B, []), R)}}} ((B8^^S e ++ tail_word k) *> 0inf)
  -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}}
  ((E8^^e ++ U^^(2*k+3) ++ y_after k) *> 0inf).

Definition full_tail (es : list nat) (e k : nat) : list Sym :=
spaced_words (map (fun e => B8^^S e) es ++ [B8^^S e]) ++ tail_word k.

Definition mixed_tail (es : list nat) (e k : nat) : list Sym :=
spaced_words (map (fun e => E8^^e ++ A8) es ++ [E8^^e]) ++
  U^^(2*k+3) ++ y_after k.

Lemma spaced_snoc_cons (w : list Sym) ws x :
spaced_words ((w :: ws) ++ [x]) = w ++ U^^2 ++ spaced_words (ws ++ [x]).

Theorem raw_tail_columns es e k l : k <= 5 ->
l {{{((B, []), R)}}} (full_tail es e k *> 0inf)
  -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}} (mixed_tail es e k *> 0inf).

Definition Yw : list Sym :=
[1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;
 1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;1;0;1;0;0;1;0;0].

Lemma cycler_step L :
(rev Yw *> L) {{B}}> 0inf -[source_tm]->+ (rev Yw *> [0;0;1] *> L) {{B}}> 0inf.

Theorem cycler_nonhalt L : ~ halts source_tm ((rev Yw *> L) {{B}}> 0inf).

Lemma overflow_base l :
l {{{((B, []), R)}}} ((B8 ++ tail_word 6) *> 0inf)
  -[source_tm]->+
(rev Yw *> [0;1;0;1] *> l) {{B}}> 0inf.

Lemma overflow_column e l : exists l',
l {{{((B, []), R)}}} ((B8^^S e ++ tail_word 6) *> 0inf)
  -[source_tm]->+ (rev Yw *> l') {{B}}> 0inf.

Theorem overflow_columns es e l : exists l',
l {{{((B, []), R)}}} (full_tail es e 6 *> 0inf)
  -[source_tm]->+ (rev Yw *> l') {{B}}> 0inf.

Theorem exit_nonhalt es e l :
~ halts source_tm (l {{{((B, []), R)}}} (full_tail es e 6 *> 0inf)).

Definition pre_left_far (n : nat) (far : side) : side :=
([1;0;1;0] ++ V4^^(2*n+2)) *> far.

Definition call_left_far (remaining finished : nat) (far : side) : side :=
(X4^^(2*finished+5) ++ V4^^(2*remaining)) *> far.

Lemma pre_rotate_list m :
[1;0;1] ++ X4^^(S m) = [1;0;1;0] ++ V4^^m ++ [0;1;0].

Lemma nested_pre_left c f :
[1;0;1] *> exception_call_left c f =
pre_left_far (S f) ([0;1;0] *> V4^^(2*c) *> [1;0;1] *> 0inf).

Lemma launch_far k far :
sideRLs (flip source_tm) [left_hash] (pre_left_far (S k) far) (call_left_far k 0 far).

Lemma relaunch_far remaining finished far :
sideRLs (flip source_tm) [left_hash]
  (call_left_far (S remaining) finished far)
  (call_left_far remaining (S finished) far).

Lemma relaunches_far k r finished far :
sideRLs (flip source_tm) ([left_hash]^^k)
  (call_left_far (k + r) finished far)
  (call_left_far r (finished + k) far).

Theorem nested_launch h r far inp out :
segRLs source_tm (hashes^^h) [] inp out ->
pre_left_far (S (h + r)) far {{{((F, []), L)}}} (inp *> 0inf)
  -[source_tm]->+
call_left_far r h far {{{((B, []), R)}}} (out *> 0inf).

Lemma E_to_B m : segRLs source_tm (hashes^^(3*(2^m-1))) [] (E8^^m) (B8^^m).

Lemma digits_word_repeat_BB n : digits_word (repeat BB n) = B8^^n.

Lemma digits_value_repeat_BB n : digits_value (repeat BB n) = 2^n - 1.

Fixpoint nested_required (es : list nat) (e : nat) : nat :=
match es with
| [] => 3*(2^(S e)-1)
| e0 :: es' =>
    (nested_required es' e + 1) * 2^(S e0) - 2 + (2^(S e0) - 1)
end.

Lemma nested_counter es e :
segRLs source_tm (hashes^^nested_required es e) []
  (spaced_words (map (fun e => E8^^e ++ A8) es ++ [E8^^S e]))
  (spaced_words (map (fun e => B8^^S e) es ++ [B8^^S e])).

Theorem nested_exit c f es e :
nested_required es e <= f ->
~ halts source_tm (exception_call_left c f {{{((B, []), R)}}}
  (full_tail es (S e) 5 *> 0inf)).

Inductive SDigit := SE | SD | SA | SB.

Definition sdigit_word (d : SDigit) : list Sym :=
match d with SE => E8 | SD => D8 | SA => A8 | SB => B8 end.

Definition sdigit_value (d : SDigit) : Z :=
match d with SE => (-2)%Z | SD => (-1)%Z | SA => 0%Z | SB => 1%Z end.

Fixpoint sdigits_word (ds : list SDigit) : list Sym :=
match ds with [] => [] | d :: ds' => sdigit_word d ++ sdigits_word ds' end.

Fixpoint sdigits_value (ds : list SDigit) : Z :=
match ds with
| [] => 0%Z
| d :: ds' => (sdigit_value d + 2 * sdigits_value ds')%Z
end.

Definition sdigit_of (d : BDigit) : SDigit := match d with BA => SA | BB => SB end.

Definition tail_layout (primary : nat) (zs : list BinaryColumn)
  (last : list SDigit) (k lv : nat) : list Sym :=
A8^^primary ++ U^^2 ++
spaced_words (map binary_column_word zs ++ [sdigits_word last]) ++
U^^(2*k+1) ++ y_after lv.

Definition post_ca_tail (unary primary : nat) (zs : list BinaryColumn)
  (last : list SDigit) (k lv : nat) : Q * tape :=
ordinary_left unary {{{((B, []), R)}}} (tail_layout primary zs last k lv *> 0inf).

Fixpoint zs_value (o : nat) (zs : list BinaryColumn) : Z :=
match zs with
| [] => 0%Z
| c :: zs' => (2^Z.of_nat o * Z.of_nat (column_value c) +
               zs_value (o + column_width c) zs')%Z
end.

Definition tail_W (primary : nat) zs (last : list SDigit) : nat :=
primary + columns_width_sum zs + length last.

Definition tail_V (primary : nat) zs last (lv : nat) : Z :=
(zs_value primary zs +
 2^Z.of_nat (primary + columns_width_sum zs) * sdigits_value last +
 2^Z.of_nat (tail_W primary zs last) * (Z.of_nat lv - 1))%Z.

Definition trigger_hash primary zs last lv : Z :=
(5 * 2^Z.of_nat (tail_W primary zs last) - tail_V primary zs last lv)%Z.

Definition tail_next_half current previous zs last lv : Z :=
((Z.of_nat (round_post_unary current previous) +
  trigger_hash (round_primary_width current previous) zs last lv - 1) / 2)%Z.

Definition tail_next_index current previous zs last lv : nat :=
Z.to_nat ((tail_next_half current previous zs last lv - 6) / 2).

Definition eff_level (last : list SDigit) (lv : nat) : Z :=
((sdigits_value last + 2^Z.of_nat (length last) * (Z.of_nat lv - 1)) /
   2^Z.of_nat (length last))%Z.

Definition tail_triggers (k : nat) (last : list SDigit) (lv : nat) : Prop :=
(Z.of_nat k - 1 + (2 - eff_level last lv) >= 5)%Z.

Definition column_budget (n : nat) (c : BinaryColumn) : Prop :=
exists phase,
  n <= lineage_fuel phase /\
  low_slice (pow2 (column_width c)) (lineage_width phase)
    (lineage_residue phase) (Z.of_nat (column_value c)).

Lemma column_budget_safe n c : column_budget n c -> column_safe c.

Lemma lineage_next_fuel phase :
1 <= lineage_fuel phase ->
exists phase', lineage_next phase phase' /\
  S (lineage_fuel phase') = lineage_fuel phase.

Lemma column_budget_step n c c' b :
column_budget (S n) c -> column_step b c c' -> column_budget n c'.

Lemma z_column_budget previous : column_budget 3 (z_column previous).

Fixpoint tail_columns_step (right_odd : bool)
  (cs cs' : list BinaryColumn) : Prop :=
match cs, cs' with
| [], [] => True
| c::rest, c'::rest' =>
    column_step (match rest with [] => right_odd
… +4 lines

Theorem tail_columns_budget_step n cs b :
Forall (column_budget (S n)) cs ->
exists cs', tail_columns_step b cs cs' /\ Forall (column_budget n) cs'.

Lemma column_budget_weaken n m c : n <= m -> column_budget m c -> column_budget n c.

Theorem tail_columns_round_budget k previous cs b :
1 <= k <= 3 -> Forall (column_budget (4-k)) cs ->
exists cs', tail_columns_step b cs cs' /\
  Forall (column_budget (4-S k)) (z_column previous :: cs').

Definition phase_width k := 30-k.

Definition phase_value k : Z :=
match k with
| 1 => 391468375%Z
| 2 => (-195734187)%Z
| 3 => 97867094%Z
| _ => (-116042411)%Z
… +1 lines

Definition phase_lv k := match k with 1 => 4 | 2 => 1 | 3 => 5 | _ => 3 end.

Definition phase_eff k : Z :=
((phase_value k + 2^Z.of_nat (phase_width k) * (Z.of_nat (phase_lv k)-1)) /
  2^Z.of_nat (phase_width k))%Z.

Lemma phase_effective_levels :
phase_eff 1 = 3%Z /\ phase_eff 2 = (-1)%Z /\
phase_eff 3 = 4%Z /\ phase_eff 4 = 0%Z.

Lemma phase_level_step k :
1 <= k <= 3 -> phase_eff (S k) = (Z.of_nat k + 1 - phase_eff k)%Z.

Lemma phase_value_step k :
1 <= k <= 3 ->
(phase_value (S k) mod 2^Z.of_nat (phase_width (S k)) =
  2^Z.of_nat (phase_width (S k)) -
    (phase_value k mod 2^Z.of_nat (phase_width k))/2)%Z.

Lemma phase_window k :
1 <= k <= 4 ->
(3 <= phase_value k + 2^Z.of_nat (phase_width k)*2)%Z /\
(phase_value k <= 2^Z.of_nat (phase_width k)-6)%Z.

Record finite_round_pre current previous zs last k lv : Prop := {
  fr_stage : 1 <= k <= 4;
  fr_columns : Forall (column_budget (4-k)) zs;
  fr_head_odd : match zs with
                | c::_ => Nat.odd (column_value c) = true
                | [] => Z.odd (sdigits_value last) = true end;
… +8 lines

Lemma finite_pre_safe current previous zs last k lv :
finite_round_pre current previous zs last k lv -> Forall column_safe zs.

Lemma finite_pre_eff current previous zs last k lv :
finite_round_pre current previous zs last k lv -> eff_level last lv = phase_eff k.

Lemma finite_pre_nontrigger current previous zs last k lv :
finite_round_pre current previous zs last k lv -> k <= 3 ->
~ tail_triggers k last lv.

Lemma finite_pre_trigger current previous zs last lv :
finite_round_pre current previous zs last 4 lv -> tail_triggers 4 last lv.

Definition finite_round_obligation : Prop :=
forall current previous zs last k lv,
finite_round_pre current previous zs last k lv -> k <= 3 ->
exists zs' last' lv',
  post_ca_tail (round_post_unary current previous)
    (round_primary_width current previous) zs last k lv
… +7 lines

Definition finite_trigger_obligation : Prop :=
forall current previous zs last lv,
finite_round_pre current previous zs last 4 lv ->
exists c f es e,
  post_ca_tail (round_post_unary current previous)
    (round_primary_width current previous) zs last 4 lv
… +3 lines

Definition early_tail := U^^3 ++ A8 ++ B8^^2 ++ [1;1].

Definition fourth_tail := C8 ++ [1;1] ++ C8 ++ A8^^2 ++ [1;1;1;1].

Lemma opening_D_to_third_done :
(D;; tape0) -[source_tm]->* exception_done 28 early_tail.

Lemma opening_local_hash :
segRLs source_tm hashes []
  (C8 ++ A8 ++ U ++ A8 ++ B8^^2 ++ [1;1])
  (D8 ++ fourth_tail).

Definition opening_after_cd_calls p :=
initial_u_pair_calls p 1 +
  (2^(p+1) + (2^(p+1) + (2^(p+2)-1))).

Lemma opening_after_cd_side p :
sideRLs source_tm (hashes^^opening_after_cd_calls p)
  ((A8^^p ++ C8 ++ A8 ++ early_tail) *> 0inf)
  ((B8^^(p+2) ++ fourth_tail) *> 0inf).

Definition opening_n4 := 3*2^29-2.

Lemma opening_total_count_general p :
cd_calls p + opening_after_cd_calls p = 2*(3*2^(p+1)-2)+1.

Lemma opening_total_count :
cd_calls 28 + opening_after_cd_calls 28 = 2*opening_n4+1.

Theorem opening_D_to_fourth_frontier :
(D;; tape0) -[source_tm]->*
ordinary_left (2*opening_n4+1) {{{((B, []), R)}}}
  ((B8^^30 ++ fourth_tail) *> 0inf).

Fixpoint sfinish_count (ds : list SDigit) (out : nat) : nat :=
match ds with
| [] => out
| d::rest => 2*sfinish_count rest out +
    match d with SE => 3 | SD => 2 | SA => 1 | SB => 0 end
end.

Lemma hash_D_finish n :
segRLs source_tm (hashes^^(2*n+2)) (hashes^^n) D8 B8.

Theorem sfinish_spec ds out :
segRLs source_tm (hashes^^sfinish_count ds out) (hashes^^out)
  (sdigits_word ds) (B8^^length ds).

Theorem sfinish_value ds out :
(Z.of_nat (sfinish_count ds out) + sdigits_value ds + 1 =
  (Z.of_nat out+1)*pow2 (length ds))%Z.

Lemma tail_level_finish lv : lv <= 5 ->
sideRLs source_tm (hashes^^(5-lv))
  (y_after lv *> 0inf) ((B8 ++ [1;1]) *> 0inf).

Definition last_finish_count last lv := sfinish_count last (5-lv).

Lemma last_to_frontier last k lv : lv <= 5 ->
sideRLs source_tm (hashes^^last_finish_count last lv)
  ((sdigits_word last ++ U^^(2*k+1) ++ y_after lv) *> 0inf)
  ((B8^^length last ++ U^^(2*k+1) ++ B8 ++ [1;1]) *> 0inf).

Fixpoint columns_with_tail (zs : list BinaryColumn) (tail : list Sym) : list Sym :=
match zs with [] => tail
| c::rest => binary_column_word c ++ U^^2 ++ columns_with_tail rest tail end.

Fixpoint all_B_with_tail (zs : list BinaryColumn) (tail : list Sym) : list Sym :=
match zs with [] => tail
| c::rest => B8^^column_width c ++ U^^2 ++ all_B_with_tail rest tail end.

Fixpoint columns_finish_count (zs : list BinaryColumn) (out : nat) : nat :=
match zs with [] => out
| c::rest => bfinish_count (column_digits c) (columns_finish_count rest out) end.

Lemma columns_finish_tail zs out input output :
sideRLs source_tm (hashes^^out) (input *> 0inf) (output *> 0inf) ->
sideRLs source_tm (hashes^^columns_finish_count zs out)
  (columns_with_tail zs input *> 0inf) (all_B_with_tail zs output *> 0inf).

Definition tail_finish_count primary zs last lv :=
bfinish_count (repeat BA primary) (columns_finish_count zs (last_finish_count last lv)).

Definition tail_frontier primary zs (last : list SDigit) k :=
B8^^primary ++ U^^2 ++
  all_B_with_tail zs (B8^^length last ++ U^^(2*k+1) ++ B8 ++ [1;1]).

Lemma spaced_cons_nonempty a xs : xs <> [] ->
spaced_words (a::xs) = a ++ U^^2 ++ spaced_words xs.

Lemma tail_layout_chain primary zs last k lv :
tail_layout primary zs last k lv =
A8^^primary ++ U^^2 ++
  columns_with_tail zs (sdigits_word last ++ U^^(2*k+1) ++ y_after lv).

Theorem tail_to_frontier primary zs last k lv : lv <= 5 ->
sideRLs source_tm (hashes^^tail_finish_count primary zs last lv)
  (tail_layout primary zs last k lv *> 0inf)
  (tail_frontier primary zs last k *> 0inf).

Lemma pow2_add_local a b : (pow2 (a+b) = pow2 a * pow2 b)%Z.

Lemma pow2_Zpow n : pow2 n = (2^Z.of_nat n)%Z.

Lemma bfinish_value_Z ds out :
(Z.of_nat (bfinish_count ds out) + Z.of_nat (digits_value ds) + 1 =
  (Z.of_nat out+1)*pow2 (length ds))%Z.

Fixpoint columns_value_Z (zs : list BinaryColumn) : Z :=
match zs with [] => 0%Z
| c::rest => (Z.of_nat (column_value c) +
    pow2 (column_width c)*columns_value_Z rest)%Z end.

Lemma zs_value_shift o zs : (zs_value o zs = pow2 o * columns_value_Z zs)%Z.

Lemma columns_finish_value zs out :
(Z.of_nat (columns_finish_count zs out) + columns_value_Z zs + 1 =
  (Z.of_nat out+1)*pow2 (columns_width_sum zs))%Z.

Theorem trigger_hash_count primary zs last lv : lv <= 5 ->
Z.of_nat (S (tail_finish_count primary zs last lv)) = trigger_hash primary zs last lv.

Definition E_digit (n : N) : SDigit :=
match n with
| N0 => SE | Npos xH => SD
| Npos (xO _) => SA | Npos (xI _) => SB
end.

Definition E_carry (n : N) : N :=
match n with
| N0 | Npos xH => N0
| Npos (xO p) | Npos (xI p) => N.pred (Npos p)
end.

Fixpoint E_decode (width : nat) (n : N) : list SDigit * N :=
match width with
| O => ([], n)
| S w => let '(ds, out) := E_decode w (E_carry n) in
    (E_digit n :: ds, out)
end.

Lemma E_digit_spec n :
segRLs source_tm (hashes^^N.to_nat n) (hashes^^N.to_nat (E_carry n))
  E8 (sdigit_word (E_digit n)).

Theorem E_decode_spec width n :
segRLs source_tm (hashes^^N.to_nat n) (hashes^^N.to_nat (snd (E_decode width n)))
  (E8^^width) (sdigits_word (fst (E_decode width n))).

Lemma E_decode_length width n : length (fst (E_decode width n)) = width.

Lemma E_digit_value n :
(Z.of_N n - 2 = sdigit_value (E_digit n) + 2*Z.of_N (E_carry n))%Z.

Theorem E_decode_value width n :
(sdigits_value (fst (E_decode width n)) +
  pow2 width * Z.of_N (snd (E_decode width n)) =
  Z.of_N n - 2*(pow2 width-1))%Z.

Definition opening_call_base : N := 462424812206%N.

Definition opening_digits : list SDigit := [SA;SA;SA;SA;SB;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SA;SB;SB;SB;SA;SB].

Lemma opening_decode_exact :
E_decode 36 opening_call_base = (opening_digits, 4%N).

Lemma opening_digits_value : sdigits_value opening_digits = 50107951792%Z.

Lemma opening_tail_four :
sideRLs source_tm (hashes^^4) (A8 *> 0inf) ((A8 ++ [1;1]) *> 0inf).

Lemma opening_decode_base :
sideRLs source_tm (hashes^^N.to_nat opening_call_base)
  ((E8^^36 ++ U^^3 ++ A8) *> 0inf)
  ((sdigits_word opening_digits ++ U^^3 ++ A8 ++ [1;1]) *> 0inf).

Definition opening_decode_calls k :=
2^k*N.to_nat opening_call_base + 2*(2^k-1).

Theorem opening_decode k :
sideRLs source_tm (hashes^^opening_decode_calls k)
  ((E8^^(k+36) ++ U^^3 ++ A8) *> 0inf)
  ((A8^^k ++ sdigits_word opening_digits ++ U^^3 ++ A8 ++ [1;1]) *> 0inf).

Lemma opening_call_base_formula :
N.to_nat opening_call_base = (1292*2^30+4)/3 + 2.

Theorem opening_decode_calls_formula k :
opening_decode_calls k = 2^(k+2)-2 + 2^k*((1292*2^30+4)/3).

Definition entry_n5 := opening_decode_calls (opening_n4-2).

Definition entry_current := (entry_n5-6)/2.

Definition entry_previous := (opening_n4-6)/2.

Definition entry_rest := skipn 9 opening_digits.

Definition entry_last := SB::SB::entry_rest.

Definition entry_state := post_ca_tail
(round_post_unary entry_current entry_previous)
(round_primary_width entry_current entry_previous) [] entry_last 1 4.

Lemma opening_n4_even_large :
(exists q, opening_n4=2*q) /\ 64<=opening_n4.

Lemma even_index_half n :
(exists q, n=2*q /\ 6<=2*q) -> half_parameter ((n-6)/2)=n.

Lemma entry_previous_half : half_parameter entry_previous=opening_n4.

Lemma opening_base_even : exists b, N.to_nat opening_call_base=2*b.

Lemma opening_decode_even_ge6 k : 2<=k ->
exists q, opening_decode_calls k=2*q /\ 6<=2*q.

Lemma entry_n5_even_ge6 : exists q, entry_n5=2*q /\ 6<=2*q.

Lemma entry_current_half : half_parameter entry_current=entry_n5.

Lemma opening_entry_growth n : 64<=n ->
2*(n+30)+4 <= opening_decode_calls (n-2)+1.

Lemma entry_last_facts :
length entry_last=29 /\ sdigits_value entry_last=391468375%Z /\
Z.odd (sdigits_value entry_last)=true.

Lemma entry_opening_word :
A8^^(opening_n4-2) ++ sdigits_word opening_digits ++ U^^3 ++ A8 ++ [1;1] =
A8^^(2*(entry_previous+4)) ++ B8++B8++A8++B8++A8++
  (sdigits_word entry_rest ++ U^^3 ++ A8 ++ [1;1]).

Theorem opening_exception_to_entry :
exception_done entry_n5
  (A8^^(opening_n4-2) ++ sdigits_word opening_digits ++ U^^3 ++ A8 ++ [1;1])
-[source_tm]->+ entry_state.

Theorem entry_pre : finite_round_pre
entry_current entry_previous [] entry_last 1 4.

Definition fossil_tail := C8 ++ [1;1] ++ C8 ++ U ++ [1;1] ++ U.

Definition fossil_start m := C8 ++ A8^^m ++ D8 ++ D8 ++ A8 ++ U ++ E8 ++ A8.

Lemma fossil_scan m :
segRLs source_tm hashes [] (fossil_start m)
  (D8 ++ C8^^m ++ D8 ++ D8 ++ fossil_tail).

Lemma fossil_tail_finish :
sideRLs source_tm (hashes^^25)
  (fossil_tail *> 0inf) ((B8^^2 ++ U ++ B8 ++ [1;1]) *> 0inf).

Lemma c_sweep_even width pairs rest :
segRLs source_tm (hashes^^c_sweep_calls width pairs) []
  (A8^^width ++ C8^^(2*pairs) ++ rest)
  (A8^^(width+2*pairs) ++ rest).

Lemma fossil_tail_lift width :
sideRLs source_tm (hashes^^(25*2^width + (2^width-1)))
  ((A8^^width ++ fossil_tail) *> 0inf)
  ((B8^^(width+2) ++ U ++ B8 ++ [1;1]) *> 0inf).

Definition fossil_calls p k :=
2^p + 2^p + c_sweep_calls (p+1) k +
2^(p+1+2*k) + 2^(p+2+2*k) +
(25*2^(p+3+2*k) + (2^(p+3+2*k)-1)).

Theorem fossil_run p k :
sideRLs source_tm (hashes^^fossil_calls p k)
  ((A8^^p ++ fossil_start (2*k)) *> 0inf)
  ((B8^^(p+2*k+5) ++ U ++ B8 ++ [1;1]) *> 0inf).

Lemma geom4n_power k : 3 * geom4n k + 1 = 2^(2*k).

Lemma fossil_count_formula n k :
fossil_calls (S n) k = 2^n * ((1292*2^(2*k)+4)/3) - 1.

Theorem fossil_run_closed n k :
sideRLs source_tm (hashes^^(2^n * ((1292*2^(2*k)+4)/3) - 1))
  ((A8^^(S n) ++ fossil_start (2*k)) *> 0inf)
  ((B8^^(S n+2*k+5) ++ U ++ B8 ++ [1;1]) *> 0inf).

Definition exception_done_side n (output : side) : Q * tape :=
common_left_wall {{{((B, []), R)}}}
  ((C8 ++ A8 ++ U^^(2*n)) *> output).

Lemma exception_exit_side k output :
exception_call_left 0 k {{{((F, []), L)}}} output -[source_tm]->+
exception_done_side (S k) output.

Lemma exception_exit_zero_side output :
exception_pre_left 0 {{{((F, []), L)}}} output -[source_tm]->+
exception_done_side 0 output.

Lemma exception_calls_side k input output :
sideRLs source_tm (hashes^^(S k)) input output ->
exception_call_left k 0 {{{((B, []), R)}}} input -[source_tm]->+
exception_call_left 0 k {{{((F, []), L)}}} output.

Theorem exception_pre_from_side n input output :
sideRLs source_tm (hashes^^n) input output ->
exception_pre_left n {{{((F, []), L)}}} input -[source_tm]->+
exception_done_side n output.

Corollary exception_pre_from_side_word n input output :
sideRLs source_tm (hashes^^n) (input *> 0inf) (output *> 0inf) ->
exception_pre_left n {{{((F, []), L)}}} (input *> 0inf) -[source_tm]->+
exception_done n output.

Lemma ordinary_raw_pre_left n :
[1;0;1] *> ordinary_left (2*n+1) = exception_pre_left n.

Lemma ordinary_raw_pre_left_count tally n :
tally = 2*n+1 -> [1;0;1] *> ordinary_left tally = exception_pre_left n.

Lemma exception_relaunches_partial h r finished :
sideRLs (flip source_tm) ([left_hash]^^h)
  (exception_call_left (h+r) finished)
  (exception_call_left r (finished+h)).

Theorem exception_partial_side h r finished input output :
sideRLs source_tm (hashes^^h) input output ->
exception_call_left (h+r) finished {{{((B, []), R)}}} input -[source_tm]->*
exception_call_left r (finished+h) {{{((B, []), R)}}} output.

Theorem exception_launch_partial_side h r input output :
sideRLs source_tm (hashes^^h) input output ->
exception_pre_left (S (h+r)) {{{((F, []), L)}}} input -[source_tm]->+
exception_call_left r h {{{((B, []), R)}}} output.

Definition fourth_output := A8^^29 ++ D8 ++ D8 ++ A8 ++ U ++ E8 ++ A8.

Definition fourth_raw_output := E8^^30 ++ D8 ++ A8 ++ U ++ E8 ++ A8.

Lemma fourth_raw l :
l {{{((B, []), R)}}} ((B8^^30 ++ fourth_tail) *> 0inf) -[source_tm]->+
([1;0;1] *> l) {{{((F, []), L)}}} (fourth_raw_output *> 0inf).

Lemma n4_binary : opening_n4 = N.to_nat 1610612734%N.

Lemma n4_large : 10 <= opening_n4.

Lemma fourth_decode :
segRLs source_tm (hashes^^opening_n4) [] fourth_raw_output fourth_output.

Theorem fourth_frontier_to_done :
ordinary_left (2*opening_n4+1) {{{((B, []), R)}}}
  ((B8^^30 ++ fourth_tail) *> 0inf) -[source_tm]->+
exception_done opening_n4 fourth_output.

Lemma fourth_cd_to_fossil :
exception_done opening_n4 fourth_output -[source_tm]->+
ordinary_left (cd_calls opening_n4) {{{((B, []), R)}}}
  ((A8^^opening_n4 ++ fossil_start 30) *> 0inf).

Lemma fossil_calls_positive_formula p k : 1 <= p ->
fossil_calls p k = 2^(p-1)*((1292*2^(2*k)+4)/3)-1.

Lemma fifth_total_tally_generic n : 2 <= n ->
cd_calls n + fossil_calls n 15 = 2*opening_decode_calls (n-2)+1.

Lemma fifth_total_tally :
cd_calls opening_n4 + fossil_calls opening_n4 15 =
  2*opening_decode_calls (opening_n4-2)+1.

Definition fifth_output := A8^^(opening_n4-2) ++ sdigits_word opening_digits ++ U^^3 ++ A8 ++ [1;1].

Theorem fossil_to_fifth_frontier :
ordinary_left (cd_calls opening_n4) {{{((B, []), R)}}}
  ((A8^^opening_n4 ++ fossil_start 30) *> 0inf) -[source_tm]->*
ordinary_left (2*opening_decode_calls (opening_n4-2)+1) {{{((B, []), R)}}}
  ((B8^^(opening_n4+35) ++ U ++ B8 ++ [1;1]) *> 0inf).

Lemma fifth_frontier_to_done_generic n : 2 <= n ->
ordinary_left (2*opening_decode_calls (n-2)+1) {{{((B, []), R)}}}
  ((B8^^(n+35) ++ U ++ B8 ++ [1;1]) *> 0inf) -[source_tm]->+
exception_done (opening_decode_calls (n-2)) (A8^^(n-2) ++ sdigits_word opening_digits ++ U^^3 ++ A8 ++ [1;1]).

Theorem fifth_frontier_to_done :
ordinary_left (2*opening_decode_calls (opening_n4-2)+1) {{{((B, []), R)}}}
  ((B8^^(opening_n4+35) ++ U ++ B8 ++ [1;1]) *> 0inf) -[source_tm]->+
exception_done (opening_decode_calls (opening_n4-2)) fifth_output.

Theorem opening_D_to_fifth_done :
(D;; tape0) -[source_tm]->*
exception_done (opening_decode_calls (opening_n4-2)) fifth_output.

Definition decode_budget r := ceil_half r - 2.

Lemma column_decode_budget c c' r :
4 <= r -> column_step (Nat.odd r) c c' ->
column_required (decode_budget r) c' =
  decode_budget (r*2^(column_width c)-column_value c).

Fixpoint right_remaining (cs : list BinaryColumn) (r : nat) : nat :=
match cs with
| [] => r
| c::rest => right_remaining rest r * 2^(column_width c) - column_value c
end.

Fixpoint columns_input_count (cs : list BinaryColumn) (out : nat) : nat :=
match cs with
| [] => out
| c::rest => column_required (columns_input_count rest out) c
end.

Lemma right_remaining_lower cs r : 1 <= r -> r <= right_remaining cs r.

Lemma right_remaining_head_parity c cs r : 1 <= r ->
Nat.odd (right_remaining (c::cs) r) = Nat.odd (column_value c).

Theorem columns_decode_budget cs cs' r :
4 <= r -> tail_columns_step (Nat.odd r) cs cs' ->
columns_input_count cs' (decode_budget r) = decode_budget (right_remaining cs r).

Lemma right_remaining_finish cs last lv :
right_remaining cs (S (last_finish_count last lv)) =
  S (columns_finish_count cs (last_finish_count last lv)).

Fixpoint mixed_with_tail (cs : list BinaryColumn) (tail : list sym) : list sym :=
match cs with
| [] => tail
| c::rest => mixed_column_word c ++ U^^2 ++ mixed_with_tail rest tail
end.

Theorem mixed_with_tail_spec cs out input output :
sideRLs source_tm (hashes^^out) (input *> 0inf) (output *> 0inf) ->
sideRLs source_tm (hashes^^columns_input_count cs out)
  (mixed_with_tail cs input *> 0inf) (columns_with_tail cs output *> 0inf).

Lemma mixed_with_tail_same_width b cs cs' input :
tail_columns_step b cs cs' -> mixed_with_tail cs input = mixed_with_tail cs' input.

Theorem tail_columns_decode cs cs' r input output :
4 <= r -> tail_columns_step (Nat.odd r) cs cs' ->
sideRLs source_tm (hashes^^decode_budget r) (input *> 0inf) (output *> 0inf) ->
sideRLs source_tm (hashes^^decode_budget (right_remaining cs r))
  (mixed_with_tail cs input *> 0inf) (columns_with_tail cs' output *> 0inf).

Lemma post_unary_even current previous :
round_post_unary current previous = 2*(round_post_unary current previous/2).

Theorem primary_decode_tally current previous r :
4 <= r -> Nat.odd r = true ->
round_post_unary current previous + (r*2^(round_primary_width current previous)-1) =
  2*column_required (decode_budget r) (round_outer_column current previous)+1.

Definition decoded_last7 := fst (E_decode 28 341136723%N).

Definition decoded_last8 := fst (E_decode 27 768955732%N).

Definition decoded_last9 := fst (E_decode 26 18175315%N).

Lemma decode_last7 : E_decode 28 341136723%N = (decoded_last7, 0%N).

Lemma decode_last8 : E_decode 27 768955732%N = (decoded_last8, 3%N).

Lemma decode_last9 : E_decode 26 18175315%N = (decoded_last9, 0%N).

Lemma decode_trigger_frontier :
E_decode 25 134217725%N = (repeat SB 25, 1%N).

Theorem decoded_last_checkpoints :
length decoded_last7 = 28 /\ sdigits_value decoded_last7 = (-195734187)%Z /\
length decoded_last8 = 27 /\ sdigits_value decoded_last8 = 97867094%Z /\
length decoded_last9 = 26 /\ sdigits_value decoded_last9 = (-116042411)%Z.

Lemma E_decode_tail_run width calls ds out k lv :
E_decode width calls = (ds, out) ->
sideRLs source_tm (hashes^^N.to_nat out)
  (y_after k *> 0inf) (y_after lv *> 0inf) ->
sideRLs source_tm (hashes^^N.to_nat calls)
  ((E8^^width ++ U^^(2*k+3) ++ y_after k) *> 0inf)
… +1 lines

Theorem last_case6_return :
sideRLs source_tm (hashes^^N.to_nat 341136723%N)
  ((E8^^28 ++ U^^5 ++ y_after 1) *> 0inf)
  ((sdigits_word decoded_last7 ++ U^^5 ++ y_after 1) *> 0inf).

Theorem last_case7_return :
sideRLs source_tm (hashes^^N.to_nat 768955732%N)
  ((E8^^27 ++ U^^7 ++ y_after 2) *> 0inf)
  ((sdigits_word decoded_last8 ++ U^^7 ++ y_after 5) *> 0inf).

Theorem last_case8_return :
sideRLs source_tm (hashes^^N.to_nat 18175315%N)
  ((E8^^26 ++ U^^9 ++ y_after 3) *> 0inf)
  ((sdigits_word decoded_last9 ++ U^^9 ++ y_after 3) *> 0inf).

Theorem last_case9_frontier :
sideRLs source_tm (hashes^^N.to_nat 134217725%N)
  ((E8^^25 ++ U^^11 ++ y_after 4) *> 0inf)
  ((B8^^25 ++ U^^11 ++ y_after 5) *> 0inf).

Definition phase_R (k : nat) : N :=
match k with
| 1%nat => 682273449%N | 2%nat => 1537911467%N
| 3%nat => 36350634%N | _ => 317369003%N
end.

Lemma phase_R_value k : 1 <= k <= 4 ->
((6-Z.of_nat (phase_lv k))*pow2 (phase_width k)-phase_value k =
  Z.of_N (phase_R k))%Z.

Theorem finite_last_R current previous zs last k lv :
finite_round_pre current previous zs last k lv ->
S (last_finish_count last lv) = N.to_nat (phase_R k).

Lemma phase_R_large k : (4 <= N.to_nat (phase_R k))%nat.

Definition next_last k :=
match k with 1%nat => decoded_last7 | 2%nat => decoded_last8 | _ => decoded_last9 end.

Lemma phase_decode_budget k : 1 <= k <= 3 ->
decode_budget (N.to_nat (phase_R k)) =
  N.to_nat (match k with 1%nat => 341136723%N | 2%nat => 768955732%N | _ => 18175315%N end).

Theorem finite_last_decode k : 1 <= k <= 3 ->
sideRLs source_tm (hashes^^decode_budget (N.to_nat (phase_R k)))
  ((E8^^(phase_width k-1) ++ U^^(2*k+3) ++ y_after k) *> 0inf)
  ((sdigits_word (next_last k) ++ U^^(2*k+3) ++ y_after (phase_lv (S k))) *> 0inf).

Theorem next_last_checkpoints k : 1 <= k <= 3 ->
length (next_last k) = phase_width (S k) /\
sdigits_value (next_last k) = phase_value (S k).

Lemma N_to_nat_odd n : Nat.odd (N.to_nat n) = N.odd n.

Lemma phase_R_parity k :
Nat.odd (N.to_nat (phase_R k)) = Z.odd (phase_value k).

Lemma finite_suffix_odd current previous zs last k lv :
finite_round_pre current previous zs last k lv ->
Nat.odd (right_remaining zs (N.to_nat (phase_R k))) = true.

Theorem finite_columns_decode current previous zs last k lv :
finite_round_pre current previous zs last k lv -> k<=3 ->
exists zs',
  tail_columns_step (Nat.odd (N.to_nat (phase_R k))) zs zs' /\
  Forall (column_budget (4-S k)) (z_column previous :: zs') /\
  sideRLs source_tm (hashes^^decode_budget (right_remaining zs (N.to_nat (phase_R k))))
… +3 lines

Definition tail_frontier_state unary primary zs last k : Q * tape :=
ordinary_left unary {{{((B, []), R)}}} (tail_frontier primary zs last k *> 0inf).

Theorem post_tail_to_frontier unary primary zs last k lv : lv <= 5 ->
post_ca_tail unary primary zs last k lv -[source_tm]->*
tail_frontier_state (unary + tail_finish_count primary zs last lv)
  primary zs last k.

Lemma all_B_tail_full zs last k :
all_B_with_tail zs (B8^^S last ++ tail_word k) =
full_tail (map column_e zs) last k.

Lemma tail_frontier_full primary zs last k e : length last = S e ->
tail_frontier (S primary) zs last k = full_tail (primary :: map column_e zs) e k.

Theorem post_tail_raw unary primary zs last k lv e :
lv <= 5 -> k <= 5 -> length last = S e ->
post_ca_tail unary (S primary) zs last k lv -[source_tm]->+
([1;0;1] *> ordinary_left
  (unary + tail_finish_count (S primary) zs last lv)) {{{((F, []), L)}}}
  (mixed_tail (primary :: map column_e zs) e k *> 0inf).

Lemma mixed_tail_chain cs e k :
mixed_tail (map column_e cs) e k =
mixed_with_tail cs (E8^^e ++ U^^(2*k+3) ++ y_after k).