1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---

Definition tm := Eval compute in (TM_from_str "1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---").

Lemma ev_eq {c1 c2 c2'} : c1 -->* c2 -> c2 = c2' -> c1 -->* c2'.

Lemma prog_eq {c1 c2 c2'} : c1 -->+ c2 -> c2 = c2' -> c1 -->+ c2'.

Definition sd (d : bool) : list Sym := if d then [0;0;0;1] else [0;0;1;0].

Fixpoint RP (P : list (nat*nat*bool)) (r : side) : side :=
match P with
| [] => r
| (p,q,d) :: P' => [1;0]^^p *> [0;1]^^q *> sd d *> RP P' r
end.

Inductive Tl := TN | TA (t : nat) | TB (k : nat).

Definition RT (T : Tl) : side :=
match T with
| TN => 0inf
| TA t => [1;0]^^t *> [1] *> 0inf
| TB k => [1;0;1;1;0;1] *> [0;1]^^k *> 0inf
end.

Definition pre (h : nat) : side := 0inf <* <[1;0]^^(4+h) <* <[1;1;1].

Definition reg (p q : nat) (l : side) : side :=
l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(pred q) <* <[1;1].

Fixpoint LP (Z : list (nat*nat*bool)) (l : side) : side :=
match Z with
| [] => l
| (p,q,d) :: Z' => LP Z' (reg p q l)
end.

Fixpoint OvR (Z : list (nat*nat*bool)) (r : side) : side :=
match Z with
| [] => r
| (p,q,d) :: Z' => [0;1]^^p *> [0;0;0;1] *> [1;0]^^q *> OvR Z' r
end.

Definition touch (x : nat*nat*bool) : nat*nat*bool :=
let '(p,q,d) := x in (S p, pred q, negb d).

Definition okR (x : nat*nat*bool) : Prop := let '(p,q,d) := x in d = false /\ 1 <= q.

Definition okL (x : nat*nat*bool) : Prop := let '(p,q,d) := x in d = false /\ 2 <= q.

Definition okO (x : nat*nat*bool) : Prop := let '(p,q,d) := x in 1 <= p /\ 1 <= q.

Lemma RP_app Z W r : RP (Z ++ W) r = RP Z (RP W r).

Lemma LP_app Z W l : LP (Z ++ W) l = LP W (LP Z l).

Lemma okL_R Z : Forall okL Z -> Forall okR Z.

Lemma Dec h Z p q R T : Forall okL Z ->
K h (Z ++ (p, S (S q), true) :: R) T -->+ K (4+h) (map touch Z ++ (S p, S q, false) :: R) T.

Lemma DecMerge h Z p p' q' d' R T : Forall okL Z ->
K h (Z ++ (p, 1%nat, true) :: (p', q', d') :: R) T -->+ K (4+h) (map touch Z ++ (p+p'+3, q', d') :: R) T.

Lemma DecMergeTail h Z p t : Forall okL Z ->
K h (Z ++ [(p, 1%nat, true)]) (TA t) -->+ K (4+h) (map touch Z) (TA (p+t+3)).

Lemma DecMergeEmpty h Z p : Forall okL Z ->
K h (Z ++ [(p, 1%nat, true)]) TN -->+ K (4+h) (map touch Z) (TA (p+2)).

Lemma Forall_snoc {A} (P : A -> Prop) Z x : Forall P Z -> P x -> Forall P (Z ++ [x]).

Lemma EndR h Z p q : Forall okL Z ->
K h (Z ++ [(p, S (S q), false)]) TN -->+ K (4+h) (map touch Z ++ [(S p, S q, false)]) (TA 1).

Lemma EndLast h Z p : Forall okL Z ->
K h (Z ++ [(p, 1%nat, false)]) TN -->+ K (4+h) (map touch Z) (TA (p+4)).

Lemma X2 h Z p q k : Forall okL Z ->
K h (Z ++ [(p, S (S q), false)]) (TB (S k)) -->+
K (4+h) (map touch Z ++ [(S p, S q, false); (3%nat, S k, true)]) TN.

Fixpoint ovp (q : nat) (Z : list (nat*nat*bool)) (t : nat) : list (nat*nat*bool) :=
match Z with
| [] => [(q, S t, true)]
| (p',q',_) :: Z' => (q, p', true) :: ovp q' Z' t
end.

Lemma ovp_eq Z : forall q t, RP (ovp q Z t) 0inf = [1;0]^^q *> OvR Z ([0;1]^^(S t) *> [0;0;0;1] *> 0inf).

Lemma Ov h p1 q1 Z t : 1 <= q1 -> Forall okR Z -> Forall okO Z ->
K h ((S (S p1), q1, false) :: Z) (TA t) -->+ K 2 ((h+5, S p1, false) :: ovp q1 Z t) TN.

Fixpoint ovpX (q : nat) (Z : list (nat*nat*bool)) (pa : nat) : list (nat*nat*bool) :=
match Z with
| [] => [(q, pa, false)]
| (p',q',_) :: Z' => (q, p', true) :: ovpX q' Z' pa
end.

Lemma ovpX_eq Z : forall q pa r, RP (ovpX q Z pa) r = [1;0]^^q *> OvR Z ([0;1]^^pa *> [0;0;1;0] *> r).

Lemma tailB_eq n : [0;0;1;0;1;0;1] *> [1;0]^^(S n) *> [1] *> 0inf = [0;0;1;0] *> RT (TB n).

Lemma X1 h p1 q1 Z pa pb : 1 <= q1 -> Forall okR Z -> Forall okO Z ->
K h ((S (S p1), q1, false) :: Z ++ [(S pa, 1%nat, false); (pb, 1%nat, false)]) TN -->+
K 2 ((h+5, S p1, false) :: ovpX q1 Z (S pa)) (TB (pb+3)).

Lemma init : c0 -->* K 2 base TN.

Definition bv (d : bool) : nat := if d then 1 else 0.

Fixpoint dv (P : list tri) : nat :=
match P with
| [] => 0
| (_,_,d) :: P' => bv d + 2 * dv P'
end.

Definition dig (x : tri) : bool := let '(_,_,d) := x in d.

Definition dig0 (x : tri) : Prop := dig x = false.

Lemma dv_lt P : dv P < 2 ^ length P.

Lemma dv_zeros Z R : Forall dig0 Z -> dv (Z ++ R) = 2 ^ length Z * dv R.

Lemma dv_tz Z R : Forall dig0 Z -> dv (map touch Z ++ R) + 1 = 2 ^ length Z + 2 ^ length Z * dv R.

Fixpoint AllI (Pr : nat -> tri -> list tri -> Prop) (i : nat) (P : list tri) : Prop :=
match P with
| [] => True
| x :: Y => Pr i x Y /\ AllI Pr (S i) Y
end.

Lemma AllI_app Pr Z : forall i R, AllI Pr i (Z ++ R) -> AllI Pr (i + length Z) R.

Lemma AllI_mono (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i,
(forall j x Y, i <= j -> Pr j x Y -> Pr' j x Y) -> AllI Pr i P -> AllI Pr' i P.

Lemma AllI_shift (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i,
(forall j x Y, i <= j -> Pr (S j) x Y -> Pr' j x Y) -> AllI Pr (S i) P -> AllI Pr' i P.

Lemma AllI_touchZ (Pr Pr' : nat -> tri -> list tri -> Prop) R R' : forall Z i,
Forall dig0 Z ->
(forall j p q Zr, Forall dig0 Zr -> j + S (length Zr) = i + length Z ->
   Pr j (p,q,false) (Zr ++ R) -> Pr' j (S p, pred q, true) (map touch Zr ++ R')) ->
AllI Pr i (Z ++ R) -> AllI Pr' (i + length Z) R' -> AllI Pr' i (map touch Z ++ R').

Inductive phase := E1 | E2 | E1t | E2t | T0 | L1 | L2 | LX.

Definition PN (ph : phase) (c4 : bool) (p q n tv : nat) : Prop :=
match ph with
| E1 => match n with
        | 0 => q >= tv + 2 ^ n + 1 /\ p + tv + 2 ^ n >= 3
        | S _ => q >= tv + 3 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv + 2 ^ n >= 3 * 2 ^ n
        end
… +35 lines

Definition PI (ph : phase) (h i p q n tv : nat) : Prop :=
match i with
| 1 => h mod 2 = 0 /\
       match ph with
       | E1 | E1t => 2 <= n /\ p + tv + 2 ^ n + 3 >= 11 * 2 ^ n /\ h + 4 * (tv + 2 ^ n) + 6 >= 12 * 2 ^ n
       | E2 | E2t => 2 <= n /\ p + tv + 3 >= 11 * 2 ^ n /\ h + 4 * tv + 6 >= 12 * 2 ^ n
… +14 lines

Definition PC (ph : phase) (c4 : bool) (h i p q n tv : nat) : Prop :=
1 <= p /\ 1 <= q /\ PN ph c4 p q n tv /\ PI ph h i p q n tv.

Definition Lift (Pr : nat -> nat -> nat -> nat -> nat -> Prop) (i : nat) (x : tri) (Y : list tri) : Prop :=
let '(p,q,d) := x in Pr i p q (length Y) (dv (x :: Y)).

Definition PCx (ph : phase) (c4 : bool) (h : nat) := Lift (PC ph c4 h).

Lemma pow_pos n : 1 <= 2 ^ n.

Lemma ob_touch ph c4 h i p q n tv : 1 <= tv -> 2 <= q ->
PC ph c4 h i p q n tv -> PC ph c4 (4 + h) i (S p) (pred q) n (tv - 1).

Lemma pow_S n : 2 ^ S n = 2 * 2 ^ n.

Lemma ob_merge ph c4 h i p q n u U :
(ph = L1 \/ ph = L2 \/ ph = LX) ->
1 <= n -> 2 <= u -> u mod 2 = 0 -> U mod 2 = 0 -> U + u <= 2 * 2 ^ n ->
(ph = L1 -> U + u <= 2 ^ n) -> (ph = LX -> 2 <= n) -> (ph = L1 -> c4 = true -> 2 <= n) ->
(i = 1 -> 2 <= n) -> (ph = LX -> i = 1 -> 3 <= n) -> 2 <= q ->
PC ph c4 h i p q (S n) (u + 2 * U) -> PC ph c4 (4 + h) i (S p) (pred q) n (u - 1 + U).

Lemma ob_mt c4 h i p q n : 2 <= q -> (i = 1 -> 1 <= n) ->
PC L2 c4 h i p q (S n) (2 * 2 ^ n) -> PC L2 false (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).

Lemma ob_fuse ph c4 h h' k p p' q' n tv : (ph = L1 \/ ph = L2 \/ ph = LX) -> 3 <= k ->
PC ph c4 h (S k) p' q' n tv -> PC ph c4 h' k (p + p' + 3) q' n tv.

Lemma ob_far ph c4 h h' i j p q n tv : 3 <= i -> 3 <= j ->
PC ph c4 h i p q n tv -> PC ph c4 h' j p q n tv.

Definition endtr (ph ph' : phase) : Prop := (ph = E1 /\ ph' = E2) \/ (ph = E1t /\ ph' = E2t).

Lemma ob_end ph ph' h i p q n : endtr ph ph' -> 1 <= n -> 2 <= q ->
PC ph false h i p q n 0 -> PC ph' false (4 + h) i (S p) (pred q) n (2 ^ n - 1).

Lemma ob_end_top ph ph' h i p q : endtr ph ph' -> 3 <= i ->
PC ph false h i p (S (S q)) 0 0 -> PC ph' false (4 + h) i (S p) (S q) 0 0.

Lemma ob_endlast c4 h i p q n : 2 <= q ->
PC L1 c4 h i p q (S n) 0 -> PC L2 c4 (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).

Lemma ob_x2 h i p q n : 1 <= n -> 2 <= q ->
PC T0 false h i p q n 0 -> PC E1t false (4 + h) i (S p) (pred q) (S n) (3 * 2 ^ n - 1).

Lemma ob_x2_top h i p q : 3 <= i ->
PC T0 false h i p (S (S q)) 0 0 -> PC E1t false (4 + h) i (S p) (S q) 1 2.

Lemma ob_x2_new h i k : 3 <= i -> 3 <= k -> PC E1t false h i 3 k 0 1.

Definition ovtr (ph ph' : phase) (c4' : bool) (Xp : nat -> Prop) : Prop :=
(ph = E2 /\ ph' = L1 /\ c4' = false /\ Xp = (fun x => x <> 4)) \/
(ph = E2 /\ ph' = LX /\ c4' = false /\ Xp = (fun x => x = 4)) \/
(ph = E2t /\ ph' = L1 /\ c4' = true /\ Xp = (fun _ => True)) \/
(ph = L2 /\ ph' = E1 /\ c4' = false /\ Xp = (fun _ => True)).

Lemma ob_ov_head ph ph' c4' Xp h p1 q1 n : ovtr ph ph' c4' Xp ->
PC ph false h 1 (S (S p1)) q1 n 0 -> PC ph' c4' 2 1 (h + 5) (S p1) (S n) (2 * (2 * 2 ^ n) - 2).

Lemma ob_ov_step ph ph' c4' Xp h i pp q p' q' m : ovtr ph ph' c4' Xp -> 1 <= i ->
PC ph false h i pp q (S m) 0 -> PC ph false h (S i) p' q' m 0 -> (m = 0 -> Xp p') ->
PC ph' c4' 2 (S i) q p' (S m) (2 * (2 * 2 ^ m) - 1).

Lemma ob_ov_base ph ph' c4' Xp h i pp q t : ovtr ph ph' c4' Xp -> 1 <= i ->
(ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
PC ph false h i pp q 0 0 -> PC ph' c4' 2 (S i) q (S t) 0 1.

Lemma ob_x1_head h p1 q1 n :
PC LX false h 1 (S (S p1)) q1 (S (S n)) 0 -> PC T0 false 2 1 (h + 5) (S p1) (S n) (2 * 2 ^ n - 2).

Lemma ob_x1_step h i pp q p' q' m : 1 <= i ->
PC LX false h i pp q (S (S (S m))) 0 -> PC LX false h (S i) p' q' (S (S m)) 0 ->
PC T0 false 2 (S i) q p' (S m) (2 * 2 ^ m - 1).

Lemma ob_x1_base h i pp q pa : 1 <= i ->
PC LX false h i pp q 2 0 -> PC LX false h (S i) (S pa) 1 1 0 -> PC T0 false 2 (S i) q (S pa) 0 0.

Lemma dv_zero Z : Forall dig0 Z -> dv Z = 0.

Lemma dv_tz' Z R : Forall dig0 Z -> dv (map touch Z ++ R) = 2 ^ length Z - 1 + 2 ^ length Z * dv R.

Lemma ovp_len q Z t : length (ovp q Z t) = S (length Z).

Lemma ovp_dv q Z t : dv (ovp q Z t) + 1 = 2 ^ S (length Z).

Lemma ovpX_len q Z pa : length (ovpX q Z pa) = S (length Z).

Lemma ovpX_dv q Z pa : dv (ovpX q Z pa) + 1 = 2 ^ length Z.

Fixpoint lastOK (Xp : nat -> Prop) (Z : list tri) : Prop :=
match Z with
| [] => True
| [(p,_,_)] => Xp p
| _ :: Z' => lastOK Xp Z'
end.

Lemma lastOK_cons Xp p q d Z : lastOK Xp ((p,q,d) :: Z) -> (Z = [] -> Xp p) /\ lastOK Xp Z.

Lemma lastOK_dec Z : lastOK (fun x => x = 4) Z \/ lastOK (fun x => x <> 4) Z.

Lemma AllI_ovp ph ph' c4' Xp h t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
forall Z i pp q, 1 <= i -> Forall dig0 Z -> lastOK Xp Z -> PC ph false h i pp q (length Z) 0 ->
AllI (PCx ph false h) (S i) Z -> AllI (PCx ph' c4' 2) (S i) (ovp q Z t).

Lemma AllI_ovpX h pa pb : forall Z i pp q, 1 <= i -> Forall dig0 Z ->
PC LX false h i pp q (S (S (length Z))) 0 ->
AllI (PCx LX false h) (S i) (Z ++ [(S pa, 1, false); (pb, 1, false)]) ->
AllI (PCx T0 false 2) (S i) (ovpX q Z (S pa)).

Lemma passq ph c4 h i p q n tv : PC ph c4 h i p q n tv -> 2 <= tv -> tv mod 2 = 0 -> 2 <= q.

Lemma Z_okL ph c4 h : forall Z i x R, Forall dig0 Z -> dig x = true ->
AllI (PCx ph c4 h) i (Z ++ x :: R) -> Forall okL Z.

Lemma borrow1 ph c4 h k p n tv : 1 <= k -> tv mod 2 = 1 -> PC ph c4 h k p 1 n tv ->
(ph = L1 \/ ph = L2 \/ ph = LX) /\ 3 <= k /\
(ph = L1 -> 1 <= n /\ tv + 1 <= 2 ^ n /\ (c4 = true -> 2 <= n)) /\ (ph = LX -> 2 <= n).

Lemma even2 x : (2 * x) mod 2 = 0.

Lemma pc_len (Pr : nat -> tri -> list tri -> Prop) i P : AllI Pr i P -> True.

Lemma inv_Dec ph c4 h Z p q R : Forall dig0 Z ->
AllI (PCx ph c4 h) 1 (Z ++ (p, S (S q), true) :: R) ->
AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (S p, S q, false) :: R).

Lemma snoc_nn (Z : list tri) y : Z ++ [y] <> [].

Definition minlen (ph : phase) : nat := match ph with LX => 3 | L2 => 1 | _ => 2 end.

Lemma head_len ph c4 h x Y : PCx ph c4 h 1 x Y -> minlen ph <= length Y.

Lemma AllI_len ph c4 h P : P <> [] -> AllI (PCx ph c4 h) 1 P -> S (minlen ph) <= length P.

Lemma q2_V0 ph c4 h i p q n : PC ph c4 h i p q n 0 -> 1 <= n -> (ph = LX -> 2 <= n) -> 2 <= q.

Lemma p1_V0 ph c4 h p q n : PC ph c4 h 1 p q n 0 -> (ph = E2 \/ ph = E2t \/ ph = L2 \/ ph = LX) -> 2 <= p.

Lemma L2_c4_V0 h i p q : PC L2 true h i p q 0 0 -> False.

Lemma AllI_okRO ph c4 h : forall Z i, Forall dig0 Z -> AllI (PCx ph c4 h) i Z -> Forall okR Z /\ Forall okO Z.

Lemma inv_Merge ph c4 h Z p p' q' d' R0 : Forall dig0 Z ->
AllI (PCx ph c4 h) 1 (Z ++ (p, 1, true) :: (p', q', d') :: R0) ->
AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (p + p' + 3, q', d') :: R0).

Lemma inv_MT c4 h Z p : Forall dig0 Z -> AllI (PCx L2 c4 h) 1 (Z ++ [(p, 1, true)]) ->
AllI (PCx L2 false (4 + h)) 1 (map touch Z) /\ 2 <= length Z.

Lemma inv_End ph ph' h Z p q : endtr ph ph' -> Forall dig0 Z ->
AllI (PCx ph false h) 1 (Z ++ [(p, S (S q), false)]) ->
AllI (PCx ph' false (4 + h)) 1 (map touch Z ++ [(S p, S q, false)]).

Lemma inv_X2 h Z p q k : Forall dig0 Z -> 3 <= k ->
AllI (PCx T0 false h) 1 (Z ++ [(p, S (S q), false)]) ->
AllI (PCx E1t false (4 + h)) 1 (map touch Z ++ [(S p, S q, false); (3, k, true)]).

Lemma inv_EndLast c4 h Z p : Forall dig0 Z -> AllI (PCx L1 c4 h) 1 (Z ++ [(p, 1, false)]) ->
AllI (PCx L2 c4 (4 + h)) 1 (map touch Z) /\ 2 <= length Z.

Lemma inv_Ov ph ph' c4' Xp h p1 q1 Z t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
Forall dig0 Z -> lastOK Xp Z ->
AllI (PCx ph false h) 1 ((S (S p1), q1, false) :: Z) ->
AllI (PCx ph' c4' 2) 1 ((h + 5, S p1, false) :: ovp q1 Z t).

Lemma inv_X1 h p1 q1 Z pa pb : Forall dig0 Z ->
AllI (PCx LX false h) 1 ((S (S p1), q1, false) :: Z ++ [(S pa, 1, false); (pb, 1, false)]) ->
AllI (PCx T0 false 2) 1 ((h + 5, S p1, false) :: ovpX q1 Z (S pa)).

Record st := mkst { sh : nat; sP : list (nat*nat*bool); sT : Tl; sph : phase; sc4 : bool }.

Definition Cf (s : st) : Q * tape := K (sh s) (sP s) (sT s).

Definition TC (ph : phase) (c4 : bool) (T : Tl) : Prop :=
match ph with
| E1 | E1t | LX => T = TN /\ c4 = false
| L1 => T = TN
| E2 | E2t => T = TA 1 /\ c4 = false
| T0 => (exists k, T = TB k /\ 3 <= k) /\ c4 = false
… +2 lines

Definition J (s : st) : Prop :=
sP s <> [] /\ TC (sph s) (sc4 s) (sT s) /\ AllI (PCx (sph s) (sc4 s) (sh s)) 1 (sP s).

Lemma split1 (P : list tri) :
(exists Z x R, P = Z ++ x :: R /\ Forall dig0 Z /\ dig x = true) \/ Forall dig0 P.

Lemma Z_okL_V0 ph c4 h y : ph <> LX -> forall Z i, Forall dig0 (Z ++ [y]) ->
AllI (PCx ph c4 h) i (Z ++ [y]) -> Forall okL Z.

Lemma lastOK_True Z : lastOK (fun _ => True) Z.

Lemma Forall_snoc_inv (Pr : tri -> Prop) Z y : Forall Pr (Z ++ [y]) -> Forall Pr Z /\ Pr y.

Lemma last_pc ph c4 h Z p q d : Forall dig0 (Z ++ [(p,q,d)]) -> AllI (PCx ph c4 h) 1 (Z ++ [(p,q,d)]) ->
d = false /\ PC ph c4 h (1 + length Z) p q 0 0.

Lemma first_pc ph c4 h p q d Z : Forall dig0 ((p,q,d) :: Z) -> AllI (PCx ph c4 h) 1 ((p,q,d) :: Z) ->
d = false /\ PC ph c4 h 1 p q (length Z) 0 /\ Forall dig0 Z /\ AllI (PCx ph c4 h) 2 Z.

Lemma Jstep : forall s, J s -> exists s', Cf s -->+ Cf s' /\ J s'.

Lemma J_base : J (mkst 2 base TN E1 false).

Lemma nonhalt : ~ halts tm c0.