1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---

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

Lemma S4_1 l r: l <* [] {{E}}> [0;1] *> r -->* l <* [0;1] <* [] {{E}}> r.

Definition S1 := shift_rule_L _ _ _ _ _ S1_1.

Definition S2 := shift_rule_L _ _ _ _ _ S2_1.

Definition S3 := shift_rule_R _ _ _ _ _ S3_1.

Definition S4 := shift_rule_R _ _ _ _ _ S4_1.

Definition S6 := shift_rule_L _ _ _ _ _ S6_1.

Lemma T3 l r: l {{E}}> [0;0;1] *> r -->* l <* [0;1;1] {{E}}> r.

Lemma T13 l r: l {{E}}> [1;0;1] *> r -->* l <* [0;1;1] {{E}}> r.

Lemma rot01 n (Y : side) : [0;1]^^n *> (0 >> Y) = 0 >> ([1;0]^^n *> Y).

Lemma rot10 n (Y : side) : [1;0]^^n *> (1 >> Y) = 1 >> ([0;1]^^n *> Y).

Lemma Lb u v l r:
l {{E}}> [1;0]^^(S v) *> [0;1]^^(S u) *> r -->*
l <* [1;1] <* [1;0]^^v <* [0;1]^^(S u) {{E}}> r.

Inductive dg := d0 (u v : nat) | d1 (u v : nat).

Definition dr (d : dg) (r : side) : side :=
match d with
| d0 u v => [1;0]^^v *> [0;0] *> [0;1]^^u *> r
| d1 u v => [1;0]^^v *> [0;1]^^u *> r
end.

Fixpoint app_ds (r : side) (ds : list dg) : side :=
match ds with
| [] => r
| d :: t => dr d (app_ds r t)
end.

Definition R0 : side := [1;0;0;1] *> 0inf.

Definition map1 (os : list (nat*nat)) := map (fun '(u,v) => d1 (S u) (S v)) os.

Definition map0 (os : list (nat*nat)) := map (fun '(u,v) => d0 (S u) v) os.

Fixpoint rw (os : list (nat*nat)) (l : side) : side :=
match os with
| [] => l
| (u,v) :: t => rw t (l <* [1;1] <* [1;0]^^v <* [0;1]^^(S u))
end.

Lemma app_ds_app r xs ys : app_ds r (xs ++ ys) = app_ds (app_ds r ys) xs.

Lemma LbS os: forall l r, l {{E}}> app_ds r (map1 os) -->* rw os l {{E}}> r.

Fixpoint ro_out (os : list (nat*nat)) (r : side) : side :=
match os with
| [] => r
| (u,v) :: t => [0;1]^^v *> [1;0]^^(S u) *> [0;0] *> ro_out t r
end.

Fixpoint Oz (t : list (nat*nat)) (u : nat) : list dg :=
match t with
| [] => [d0 0 u]
| (a, b) :: t' => d0 b u :: Oz t' (S a)
end.

Definition Oout (os : list (nat*nat)) (A : nat) : list dg :=
match os with
| [] => []
| (u, v) :: t => d1 (S v) A :: Oz t (S u)
end.

Lemma Ozeq t: forall u r, [1;0]^^u *> [0;0] *> ro_out t r = app_ds r (Oz t u).

Lemma M_spec os u v rest a b:
K (map1 os ++ d0 u (S v) :: rest) a b -->+
K (map0 os ++ d1 (S u) v :: rest) (S a) (S (S b)).

Lemma Mdrop_spec os u2 v2 u rest a b:
K (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) a b -->+
K (map0 os ++ d0 (S u2 + S u) v2 :: rest) (S a) (S (S b)).

Lemma O_spec os a b: os <> [] ->
K (map1 os) (S a) b -->+ K (Oout os (S a)) (S (S (S b))) 1.

Definition bof d := match d with d0 _ _ => 0 | d1 _ _ => 1 end.

Definition vof d := match d with d0 _ v => v | d1 _ v => v end.

Fixpoint Rof (ds : list dg) : nat :=
match ds with
| [] => 0
| d0 _ _ :: t => 2 * Rof t + 1
| d1 _ _ :: t => 2 * Rof t
end.

Definition Rd d r := match d with d0 _ _ => 2*r+1 | d1 _ _ => 2*r end.

Definition ub d r := match d with d0 u _ => u + r + 1 | d1 u _ => u + r end.

Fixpoint AllD (P : dg -> nat -> nat -> Prop) (ds : list dg) : Prop :=
match ds with
| [] => True
| d :: t => AllD P t /\ P d (Rof t) (length t)
end.

Definition canon d := match d with d0 _ v => v >= 1 | d1 u v => u >= 1 /\ v >= 1 end.

Definition PA d r p :=
canon d /\ vof d >= Rd d r + 1 /\ ub d r mod 2 = 1 /\ (p = 0 -> ub d r = 1).

Definition PB k d r p :=
canon d /\ (vof d + bof d) mod 2 = 1 /\ ub d r >= 2^(p+k) /\ (k = 0 -> p = 0 -> d = d0 0 1).

Definition LSBok ds := match ds with [] => False | d :: _ => vof d >= Rof ds + 1 end.

Definition INV (s : list dg * nat * nat) : Prop :=
let '(ds, a, b) := s in
ds <> [] /\ a >= 1 /\ b mod 2 = 1 /\ (a + Rof ds) mod 2 = 0 /\
a + Rof ds + 2 >= 2^(S (length ds)) /\ b + 3 + 2 * Rof ds >= 2^(S (length ds)) /\ LSBok ds /\
( (AllD PA ds /\ a + Rof ds + 1 >= 2^(S (length ds)))
\/ AllD (PB 0) ds
… +1 lines

Definition Kc (s : list dg * nat * nat) : Q * tape := let '(ds, a, b) := s in K ds a b.

Lemma pow2S n : 2^(S n) = 2 * 2^n.

Lemma pow2pos n : 2^n >= 1.

Lemma Rof_bound ds : Rof ds + 1 <= 2^(length ds).

Lemma Rof_map1 os X : Rof (map1 os ++ X) = 2^(length os) * Rof X.

Lemma Rof_map1' os : Rof (map1 os) = 0.

Lemma len_map1 os : length (map1 os) = length os.

Lemma len_map0 os : length (map0 os) = length os.

Lemma AllD_app P xs ys : AllD P (xs ++ ys) -> AllD P ys.

Lemma AllD_last P xs d : AllD P (xs ++ [d]) -> P d 0 0.

Lemma AllD_canon (P : dg -> nat -> nat -> Prop) ds :
(forall d r p, P d r p -> canon d) -> AllD P ds -> Forall canon ds.

Lemma decomp ds : Forall canon ds ->
(exists os, ds = map1 os) \/ (exists os u v rest, ds = map1 os ++ d0 u (S v) :: rest).

Lemma F1 (P : dg -> nat -> nat -> Prop) os u v rest:
(forall u v r p, P (d0 u (S (S v))) r p -> P (d1 (S u) (S v)) r p) ->
(forall u v r p, P (d1 (S u) (S v)) (S r) p -> P (d0 (S u) v) r p) ->
AllD P (map1 os ++ d0 u (S (S v)) :: rest) ->
AllD P (map0 os ++ d1 (S u) (S v) :: rest) /\
Rof (map1 os ++ d0 u (S (S v)) :: rest) = S (Rof (map0 os ++ d1 (S u) (S v) :: rest)) /\
… +1 lines

Lemma PA_touch0 u v r p : PA (d0 u (S (S v))) r p -> PA (d1 (S u) (S v)) r p.

Lemma PA_touch1 u v r p : PA (d1 (S u) (S v)) (S r) p -> PA (d0 (S u) v) r p.

Lemma PB_touch0 k u v r p : PB k (d0 u (S (S v))) r p -> PB k (d1 (S u) (S v)) r p.

Lemma PB_touch1 k u v r p : PB k (d1 (S u) (S v)) (S r) p -> PB k (d0 (S u) v) r p.

Definition Rel r ro rn := rn + 1 <= ro /\ ro <= 2 * (rn + 1) /\ (r = 0 -> ro = rn + 1).

Lemma PB_chain k k' r u v ro rn p :
(k' = k \/ (k = 0 /\ k' = 1 /\ r = 0)) -> Rel r ro rn -> p >= 1 ->
PB k (d1 (S u) (S v)) ro (S p) -> PB k' (d0 (S u) v) rn p.

Lemma PB_abs k k' r p u2 v2 u :
((k' = k /\ (k = 0 -> p >= 1)) \/ (k = 0 /\ k' = 1 /\ p = 0 /\ r = 0)) ->
PB k (d0 u 1) r p -> PB k (d1 (S u2) (S v2)) (2*r+1) (S p) -> PB k' (d0 (S u2 + S u) v2) r p.

Lemma F2chain k k' r os X X' :
(k' = k \/ (k = 0 /\ k' = 1 /\ r = 0)) -> X' <> [] ->
AllD (PB k) (map1 os ++ X) -> AllD (PB k') X' -> Rel r (Rof X) (Rof X') -> length X = S (length X') ->
AllD (PB k') (map0 os ++ X') /\ Rel r (Rof (map1 os ++ X)) (Rof (map0 os ++ X')) /\
length (map1 os ++ X) = S (length (map0 os ++ X')).

Lemma F2 k k' os u2 v2 u rest:
((k' = k /\ (k = 0 -> rest <> [])) \/ (k = 0 /\ k' = 1 /\ rest = [])) ->
AllD (PB k) (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) ->
AllD (PB k') (map0 os ++ d0 (S u2 + S u) v2 :: rest) /\
Rel (Rof rest) (Rof (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest))
    (Rof (map0 os ++ d0 (S u2 + S u) v2 :: rest)) /\
… +1 lines

Lemma Oz_len t u : length (Oz t u) = S (length t).

Lemma Oz_R t u : Rof (Oz t u) + 1 = 2^(S (length t)).

Lemma Oz_AB t : forall u, AllD PA (map1 t) -> u mod 2 = 1 -> (t = [] -> u = 1) -> AllD (PB 0) (Oz t u).

Lemma Oz_CA t : forall u, AllD (PB 1) (map1 t) -> u >= 2^(S (length t)) -> AllD PA (Oz t u).

Lemma Rof_M os u v rest :
Rof (map1 os ++ d0 u (S v) :: rest) = S (Rof (map0 os ++ d1 (S u) v :: rest)).

Lemma len_M os u v w x rest :
length (map0 os ++ d1 w x :: rest) = length (map1 os ++ d0 u v :: rest).

Lemma LSB_M os u v rest :
LSBok (map1 os ++ d0 u (S (S v)) :: rest) -> LSBok (map0 os ++ d1 (S u) (S v) :: rest).

Lemma Rof_head1 os X : os <> [] -> Rof (map1 os ++ X) mod 2 = 0.

Lemma Rof_head0 os x y rest : Rof (map0 os ++ d0 x y :: rest) mod 2 = 1.

Lemma LSB_drop os u2 v2 u rest r :
LSBok (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) ->
Rel r (Rof (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest)) (Rof (map0 os ++ d0 (S u2 + S u) v2 :: rest)) ->
LSBok (map0 os ++ d0 (S u2 + S u) v2 :: rest).

Lemma app_cons_ne {A} (xs : list A) y ys : xs ++ y :: ys <> [].

Lemma macro_step s : INV s -> exists s', Kc s -->+ Kc s' /\ INV s'.