1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---

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

Definition sneg (s : Sym) : Sym := match s with S0 => S1 | S1 => S0 end.

Definition seqb (a b : Sym) : bool :=
match a, b with S0, S0 | S1, S1 => true | _, _ => false end.

Record lf := LF { lc : N; lv : list N }.

Fixpoint dot (vs nu : list N) : N :=
match vs, nu with
| v :: vs', x :: nu' => (v * x + dot vs' nu')%N
| _, _ => 0%N
end.

Definition ev (nu : list N) (a : lf) : nat := N.to_nat (lc a + dot (lv a) nu).

Fixpoint zadd (a b : list N) : list N :=
match a, b with
| x :: a', y :: b' => (x + y)%N :: zadd a' b'
| [], _ => b
| _, [] => a
end.

Definition lf_add (a b : lf) : lf := LF (lc a + lc b) (zadd (lv a) (lv b)).

Definition lf_S (a : lf) : lf := LF (N.succ (lc a)) (lv a).

Definition lf_one : lf := LF 1 [].

Definition allz (vs : list N) : bool := forallb (fun v => N.eqb v 0) vs.

Definition all4 (vs : list N) : bool := forallb (fun v => N.eqb (N.modulo v 4) 0) vs.

Definition is_zero (a : lf) : bool := andb (N.eqb (lc a) 0) (allz (lv a)).

Definition is_one (a : lf) : bool := andb (N.eqb (lc a) 1) (allz (lv a)).

Definition posb (a : lf) : bool := negb (N.eqb (lc a) 0).

Inductive tl_ := T0 | TV (k : nat).

Definition run : Type := (Sym * lf)%type.

Definition sd : Type := (list run * tl_)%type.

Fixpoint alt (b : Sym) (n : nat) : list Sym :=
match n with O => [] | S n' => b :: alt (sneg b) n' end.

Definition ev_tl (sg : nat -> side) (t : tl_) : side :=
match t with T0 => const S0 | TV k => sg k end.

Fixpoint ev_runs (nu : list N) (rs : list run) (s : side) : side :=
match rs with
| [] => s
| (b, n) :: rs' => alt b (ev nu n) *> ev_runs nu rs' s
end.

Definition ev_sd nu sg (s : sd) : side := ev_runs nu (fst s) (ev_tl sg (snd s)).

Fixpoint pop_runs (rs : list run) (t : tl_) : option (Sym * sd) :=
match rs with
| (b, n) :: rs' =>
    if is_zero n then pop_runs rs' t
    else if posb n then
      Some (b, ((if is_one n then rs' else (sneg b, LF (N.pred (lc n)) (lv n)) :: rs'), t))
… +3 lines

Definition pop (s : sd) : option (Sym * sd) := pop_runs (fst s) (snd s).

Definition push (w : Sym) (s : sd) : sd :=
match s with
| ((b0, n0) :: rs, t) =>
    if seqb w b0 then ((w, lf_one) :: (b0, n0) :: rs, t)
    else ((w, lf_S n0) :: rs, t)
| ([], t) => ([(w, lf_one)], t)
… +1 lines

Definition afterb (c : Sym) (n : lf) : Sym := if N.eqb (N.modulo (lc n) 2) 0 then c else sneg c.

Definition push_run (c : Sym) (n : lf) (s : sd) : sd :=
match s with
| ((b0, n0) :: rs, t) =>
    if seqb (afterb c n) b0 then ((c, lf_add n n0) :: rs, t)
    else ((c, n) :: (b0, n0) :: rs, t)
| ([], t) => ([(c, n)], t)
… +1 lines

Definition cR_st (i : nat) : Q :=
match i mod 4 with 0 => B | 1 => C | 2 => A | _ => B end.

Definition cR_bt (i : nat) : Sym :=
match i mod 4 with 0 => S0 | 1 => S1 | 2 => S0 | _ => S1 end.

Definition cR_idx (q : Q) (b : Sym) : option nat :=
match q, b with
| B, S0 => Some 0 | C, S1 => Some 1 | A, S0 => Some 2 | B, S1 => Some 3
| _, _ => None
end.

Definition cL_st (i : nat) : Q :=
match i mod 4 with 0 => D | 1 => D | 2 => E | _ => C end.

Definition cL_bt (i : nat) : Sym :=
match i mod 4 with 0 => S1 | 1 => S0 | 2 => S1 | _ => S0 end.

Definition cL_idx (q : Q) (b : Sym) : option nat :=
match q, b with
| D, S1 => Some 0 | D, S0 => Some 1 | E, S1 => Some 2 | C, S0 => Some 3
| _, _ => None
end.

Definition lastb (c : Sym) (n : lf) : Sym := if N.eqb (N.modulo (lc n) 2) 0 then sneg c else c.

Inductive cfg := Rc (q : Q) (l r : sd) | Lc (q : Q) (l r : sd).

Definition ev_cfg nu sg (c : cfg) : Q * tape :=
match c with
| Rc q l r => (ev_sd nu sg l) {{q}}> (ev_sd nu sg r)
| Lc q l r => (ev_sd nu sg l) <{{q}} (ev_sd nu sg r)
end.

Definition tag (o : option cfg) : option (cfg * bool) :=
match o with Some c => Some (c, true) | None => None end.

Definition sstep (c : cfg) : option (cfg * bool) :=
match c with
| Rc q l ((b, n) :: rs, t) =>
    if is_zero n then Some (Rc q l (rs, t), false) else
    match cR_idx q b with
    | Some i =>
… +16 lines

Fixpoint runp (p : positive) (c : cfg) : option (cfg * bool) :=
match p with
| xH => sstep c
| xO p' =>
    match runp p' c with
    | Some (c1, b1) => match runp p' c1 with Some (c2, b2) => Some (c2, orb b1 b2) | None => None end
… +12 lines

Lemma sneg_neq a b : seqb a b = false -> b = sneg a.

Lemma seqb_eq a b : seqb a b = true -> a = b.

Lemma sneg_sneg a : sneg (sneg a) = a.

Lemma dot_zadd a b nu : dot (zadd a b) nu = (dot a nu + dot b nu)%N.

Lemma ev_add nu a b : ev nu (lf_add a b) = ev nu a + ev nu b.

Lemma ev_S nu a : ev nu (lf_S a) = S (ev nu a).

Lemma allz_dot vs nu : allz vs = true -> dot vs nu = 0%N.

Lemma all4_dot vs nu : all4 vs = true -> exists k, dot vs nu = (4 * k)%N.

Lemma ev_zero nu a : is_zero a = true -> ev nu a = 0.

Lemma ev_one nu a : is_one a = true -> ev nu a = 1.

Lemma ev_pos nu a : posb a = true -> ev nu a = S (ev nu (LF (N.pred (lc a)) (lv a))).

Lemma ev_mod4 nu a : all4 (lv a) = true -> exists k, ev nu a = N.to_nat (lc a) + 4 * k.

Lemma ev_runs_app nu rs1 rs2 s : ev_runs nu (rs1 ++ rs2) s = ev_runs nu rs1 (ev_runs nu rs2 s).

Lemma pop_runs_spec nu sg rs t b s' :
pop_runs rs t = Some (b, s') -> ev_runs nu rs (ev_tl sg t) = b >> ev_sd nu sg s'.

Lemma pop_spec nu sg s b s' : pop s = Some (b, s') -> ev_sd nu sg s = b >> ev_sd nu sg s'.

Lemma push_spec nu sg w s : ev_sd nu sg (push w s) = w >> ev_sd nu sg s.

Definition afterb_nat (c : Sym) (n : nat) : Sym := if Nat.eqb (n mod 2) 0 then c else sneg c.

Lemma afterb_nat_S c m : afterb_nat c (S m) = afterb_nat (sneg c) m.

Lemma alt_add c m k : alt c (m + k) = alt c m ++ alt (afterb_nat c m) k.

Lemma afterb_ev nu c n : all4 (lv n) = true -> afterb c n = afterb_nat c (ev nu n).

Lemma push_run_spec nu sg c n s :
all4 (lv n) = true -> ev_sd nu sg (push_run c n s) = alt c (ev nu n) *> ev_sd nu sg s.

Definition lastb_nat (c : Sym) (m : nat) : Sym := if Nat.eqb (m mod 2) 0 then sneg c else c.

Lemma lastb_ev nu c n : all4 (lv n) = true -> lastb c n = lastb_nat c (ev nu n).

Lemma rev_alt b m (l : side) :
alt (sneg (lastb_nat b (S m))) (S m) *> l = alt (sneg (lastb_nat (sneg b) m)) m *> (sneg b >> l).

Lemma cR_cases i : (i mod 4 = 0 /\ S i mod 4 = 1) \/ (i mod 4 = 1 /\ S i mod 4 = 2) \/
(i mod 4 = 2 /\ S i mod 4 = 3) \/ (i mod 4 = 3 /\ S i mod 4 = 0).

Lemma cR_bt_S i : cR_bt (S i) = sneg (cR_bt i).

Lemma cL_bt_S i : cL_bt (S i) = sneg (cL_bt i).

Lemma accR_step i l X :
(l {{cR_st i}}> (cR_bt i >> X)) --> ((sneg (cR_bt i) >> l) {{cR_st (S i)}}> X).

Lemma accL_step i r X :
((cL_bt i >> X) <{{cL_st i}} r) --> (X <{{cL_st (S i)}} (sneg (cL_bt i) >> r)).

Lemma accR m : forall i l r,
(l {{cR_st i}}> (alt (cR_bt i) m *> r)) -->*
((alt (sneg (lastb_nat (cR_bt i) m)) m *> l) {{cR_st (i + m)}}> r).

Lemma accR_S m i l r :
(l {{cR_st i}}> (alt (cR_bt i) (S m) *> r)) -->+
((alt (sneg (lastb_nat (cR_bt i) (S m))) (S m) *> l) {{cR_st (i + S m)}}> r).

Lemma accL m : forall i l r,
((alt (cL_bt i) m *> l) <{{cL_st i}} r) -->*
(l <{{cL_st (i + m)}} (alt (sneg (lastb_nat (cL_bt i) m)) m *> r)).

Lemma accL_S m i l r :
((alt (cL_bt i) (S m) *> l) <{{cL_st i}} r) -->+
(l <{{cL_st (i + S m)}} (alt (sneg (lastb_nat (cL_bt i) (S m))) (S m) *> r)).

Definition Rel (b : bool) (c c' : Q * tape) : Prop := if b then c -->+ c' else c -->* c'.

Lemma Rel_trans b1 b2 c c' c'' : Rel b1 c c' -> Rel b2 c' c'' -> Rel (orb b1 b2) c c''.

Lemma tag_spec nu sg c o c' b : o = single c -> tag o = Some (c', b) -> Rel b (ev_cfg nu sg c) (ev_cfg nu sg c').

Lemma cR_idx_spec q b i : cR_idx q b = Some i -> q = cR_st i /\ b = cR_bt i.

Lemma cL_idx_spec q b i : cL_idx q b = Some i -> q = cL_st i /\ b = cL_bt i.

Lemma cR_st_mod i k : cR_st (i + N.to_nat (N.modulo k 4)) = cR_st (i + N.to_nat k).

Lemma cL_st_mod i k : cL_st (i + N.to_nat (N.modulo k 4)) = cL_st (i + N.to_nat k).

Lemma cR_st_add4 i a k : cR_st (i + (a + 4 * k)) = cR_st (i + a).

Lemma cL_st_add4 i a k : cL_st (i + (a + 4 * k)) = cL_st (i + a).

Lemma sstep_spec nu sg c c' b : sstep c = Some (c', b) -> Rel b (ev_cfg nu sg c) (ev_cfg nu sg c').

Lemma runp_spec nu sg p : forall c c' b, runp p c = Some (c', b) -> Rel b (ev_cfg nu sg c) (ev_cfg nu sg c').

Fixpoint strip0 (vs : list N) : list N :=
match vs with
| [] => []
| v :: vs' => match strip0 vs' with [] => if N.eqb v 0 then [] else [v] | w => v :: w end
end.

Fixpoint listN_eqb (a b : list N) : bool :=
match a, b with
| [], [] => true
| x :: a', y :: b' => andb (N.eqb x y) (listN_eqb a' b')
| _, _ => false
end.

Definition lf_eqb (a b : lf) : bool := andb (N.eqb (lc a) (lc b)) (listN_eqb (strip0 (lv a)) (strip0 (lv b))).

Definition runs_eqb (a b : list run) : bool :=
(fix f (a b : list run) := match a, b with
 | [], [] => true
 | (x, n) :: a', (y, m) :: b' => andb (andb (seqb x y) (lf_eqb n m)) (f a' b')
 | _, _ => false end) a b.

Definition tl_eqb (a b : tl_) : bool :=
match a, b with T0, T0 => true | TV i, TV j => Nat.eqb i j | _, _ => false end.

Definition sd_eqb (a b : sd) : bool := andb (runs_eqb (fst a) (fst b)) (tl_eqb (snd a) (snd b)).

Definition q_eqb (a b : Q) : bool :=
match a, b with A, A | B, B | C, C | D, D | E, E | F, F => true | _, _ => false end.

Definition cfg_eqb (a b : cfg) : bool :=
match a, b with
| Rc q l r, Rc q' l' r' => andb (q_eqb q q') (andb (sd_eqb l l') (sd_eqb r r'))
| Lc q l r, Lc q' l' r' => andb (q_eqb q q') (andb (sd_eqb l l') (sd_eqb r r'))
| _, _ => false
end.

Lemma dot_strip0 vs nu : dot (strip0 vs) nu = dot vs nu.

Lemma listN_eqb_eq a b : listN_eqb a b = true -> a = b.

Lemma lf_eqb_ev nu a b : lf_eqb a b = true -> ev nu a = ev nu b.

Lemma runs_eqb_ev nu a b s : runs_eqb a b = true -> ev_runs nu a s = ev_runs nu b s.

Lemma sd_eqb_ev nu sg a b : sd_eqb a b = true -> ev_sd nu sg a = ev_sd nu sg b.

Lemma q_eqb_eq a b : q_eqb a b = true -> a = b.

Lemma cfg_eqb_ev nu sg a b : cfg_eqb a b = true -> ev_cfg nu sg a = ev_cfg nu sg b.

Definition rstep (tgt : cfg) (st : cfg * bool * bool) : cfg * bool * bool :=
let '(c, pr, dn) := st in
if dn then st else
match sstep c with
| Some (c', b) => (c', orb pr b, cfg_eqb c' tgt)
| None => st
… +1 lines

Definition reach (fuel : positive) (c tgt : cfg) : bool :=
let '(c', pr, dn) := Pos.iter (rstep tgt) (c, false, false) fuel in andb pr dn.

Lemma reach_spec fuel c tgt : reach fuel c tgt = true ->
forall nu sg, ev_cfg nu sg c -->+ ev_cfg nu sg tgt.

Definition cn (n : N) : lf := LF n [].

Fixpoint mkruns (b : Sym) (ns : list lf) : list run :=
match ns with [] => [] | n :: ns' => (b, n) :: mkruns (lastb b n) ns' end.

Definition vt c := LF c [4;0;0;0]%N.

Definition vs c := LF c [0;4;0;0]%N.

Definition va c := LF c [0;0;4;0]%N.

Definition vl c := LF c [0;0;0;4]%N.

Inductive lab := U0 | U1 | U2 | W0 | W1 | D0 | D1 | D2.

Definition lens (s : lab) : list lf :=
match s with
| U0 => [cn 3; vt 4; vs 4; va 1; vl 2]
| U1 => [cn 3; vt 4; vs 4; va 2; vl 1]
| U2 => [cn 3; vt 4; vs 4; va 3; vl 0]
| W0 => [cn 3; vt 1; vs 6; va 4; vl 0]
… +5 lines

Definition blk (s : lab) : list run := mkruns S0 (lens s).

Definition rlens (s : lab) : list lf :=
match s with
| D0 => [vl 0; va 4; vs 4; vt 3; cn 3]
| _  => [vl 0; va 3; vs 4; vt 4; cn 3]
end%N.

Definition rblk (s : lab) : list run := mkruns S0 (rlens s).

Inductive lab1 := P0 | P1 | PD0 | PD1 | PD2.

Definition lens1 (s : lab1) : list lf :=
match s with
| P0 => [cn 3; cn 1; cn 3] | P1 => [cn 3; cn 2; cn 2] | PD0 => [cn 3; cn 3; cn 1]
| PD1 => [cn 2; cn 4; cn 1] | PD2 => [cn 1; cn 5; cn 1]
end%N.

Definition blk1 (s : lab1) : list run := mkruns S0 (lens1 s).

Definition rblk1 : list run := mkruns S1 [cn 1; cn 3; cn 3]%N.

Definition stp (p : bool) : Q := if p then A else B.

Definition turn (s : lab) : option (lab * bool) :=
match s with
| U0 => Some (U1, true) | U1 => Some (U2, true) | W0 => Some (W1, true) | W1 => Some (D0, true)
| D1 => Some (D0, false) | D2 => Some (D1, false) | _ => None
end.

Definition reset (s : lab) (p : bool) : option (lab * bool) :=
match s, p with
| U2, true => Some (U0, true) | U2, false => Some (W0, true) | D0, false => Some (D2, false)
| _, _ => None
end.

Definition turn1 (s : lab1) : option (lab1 * bool) :=
match s with
| P0 => Some (P1, true) | P1 => Some (PD0, true) | PD1 => Some (PD0, false) | PD2 => Some (PD1, false)
| PD0 => None
end.

Definition sg2 (L R : side) : nat -> side := fun k => match k with O => L | _ => R end.

Lemma reach_LR fuel q q' l l' nu L R :
reach fuel (Lc q (l, TV 0) ([], TV 1)) (Rc q' (l', TV 0) ([], TV 1)) = true ->
ev_runs nu l L <{{q}} R -->+ ev_runs nu l' L {{q'}}> R.

Lemma reach_LL fuel q q' l r' nu L R :
reach fuel (Lc q (l, TV 0) ([], TV 1)) (Lc q' ([], TV 0) (r', TV 1)) = true ->
ev_runs nu l L <{{q}} R -->+ L <{{q'}} ev_runs nu r' R.

Lemma reach_RR fuel q q' r l' nu L R :
reach fuel (Rc q ([], TV 0) (r, TV 1)) (Rc q' (l', TV 0) ([], TV 1)) = true ->
L {{q}}> ev_runs nu r R -->+ ev_runs nu l' L {{q'}}> R.

Lemma blk_turn s s' p nu L R : turn s = Some (s', p) ->
ev_runs nu (blk s) L <{{D}} R -->+ ev_runs nu (blk s') L {{stp p}}> R.

Lemma blk_pass s nu L R : turn s = None ->
ev_runs nu (blk s) L <{{D}} R -->+ L <{{D}} ev_runs nu (rblk s) R.

Lemma blk_reset s p s' p' nu L R : reset s p = Some (s', p') ->
L {{stp p}}> ev_runs nu (rblk s) R -->+ ev_runs nu (blk s') L {{stp p'}}> R.

Lemma blk1_turn s s' p L R : turn1 s = Some (s', p) ->
ev_runs [] (blk1 s) L <{{D}} R -->+ ev_runs [] (blk1 s') L {{stp p}}> R.

Lemma blk1_pass L R : ev_runs [] (blk1 PD0) L <{{D}} R -->+ L <{{E}} ev_runs [] rblk1 R.

Lemma blk1_back L R : L {{B}}> ev_runs [] rblk1 R -->+ ev_runs [] (blk1 PD2) L {{B}}> R.

Definition dgr (v : nat) : list run :=
match v with
| O => [(S0, cn 1); (S0, cn 5)]
| S O => [(S0, cn 2); (S1, cn 4)]
| _ => [(S0, cn 3); (S0, cn 3)]
end%N.

Definition lw (i : nat) : list run :=
if Nat.ltb i 81 then
  [(S1, cn 3); (S1, cn 4)] ++ dgr (i mod 3) ++ dgr (i / 3 mod 3) ++ dgr (i / 9 mod 3) ++ dgr (i / 27 mod 3)
    ++ [(S0, cn 2)]
else [(S0, cn 6); (S1, cn 4)] ++ dgr 0 ++ dgr 0 ++ dgr 0 ++ dgr 0 ++ [(S0, cn 2)].

Definition LWs (i : nat) : side := ev_runs [] (lw i) (const S0).

Lemma reach_T0 fuel q q' l l' (Y : side) :
reach fuel (Lc q (l, T0) ([], TV 0)) (Rc q' (l', T0) ([], TV 0)) = true ->
ev_runs [] l (const S0) <{{q}} Y -->+ ev_runs [] l' (const S0) {{q'}}> Y.

Definition lw_ok (i : nat) : bool := reach 1000 (Lc E (lw i, T0) ([], TV 0)) (Rc B (lw (S i), T0) ([], TV 0)).

Lemma lw_all : forallb lw_ok (seq 0 81) = true.

Lemma lw_ok_spec i Y : lw_ok i = true ->
ev_runs [] (lw i) (const S0) <{{E}} Y -->+ ev_runs [] (lw (S i)) (const S0) {{B}}> Y.

Lemma lw_ok_lt i : i < 81 -> lw_ok i = true.

Lemma lw_ep i Y : i < 81 -> LWs i <{{E}} Y -->+ LWs (S i) {{B}}> Y.

Fixpoint chs (ls : list lab) (nus : list (list N)) (L : side) : side :=
match ls, nus with
| s :: ls', nu :: nus' => ev_runs nu (blk s) (chs ls' nus' L)
| _, _ => L
end.

Fixpoint rchs (ls : list lab) (nus : list (list N)) (R : side) : side :=
match ls, nus with
| s :: ls', nu :: nus' => rchs ls' nus' (ev_runs nu (rblk s) R)
| _, _ => R
end.

Fixpoint visit3 (ls : list lab) : option (list lab * bool) :=
match ls with
| [] => None
| s :: ls' =>
  match turn s with
  | Some (s', p) => Some (s' :: ls', p)
… +7 lines

Fixpoint cb (ls : list lab) (p : bool) : option (list lab * bool) :=
match ls with
| [] => Some ([], p)
| s :: ls' =>
  match cb ls' p with
  | Some (ls'', p') => match reset s p' with Some (s'', p'') => Some (s'' :: ls'', p'') | None => None end
… +3 lines

Definition fullb (s : lab) : bool := match turn s with None => true | Some _ => false end.

Lemma visit3_spec ls : forall ls' p nus L R, visit3 ls = Some (ls', p) -> length ls = length nus ->
chs ls nus L <{{D}} R -->+ chs ls' nus L {{stp p}}> R.

Lemma pass_spec ls : forall nus L R, forallb fullb ls = true -> length ls = length nus ->
chs ls nus L <{{D}} R -->* L <{{D}} rchs ls nus R.

Lemma cb_spec ls : forall p ls' p' nus L R, cb ls p = Some (ls', p') -> length ls = length nus ->
L {{stp p}}> rchs ls nus R -->* chs ls' nus L {{stp p'}}> R.

Lemma visit3_len ls : forall ls' p, visit3 ls = Some (ls', p) -> length ls' = length ls.

Lemma cb_len ls : forall p ls' p', cb ls p = Some (ls', p') -> length ls' = length ls.

Definition vst : Type := (list lab * lab1 * nat)%type.

Definition lab1_eqb (a b : lab1) : bool :=
match a, b with P0, P0 | P1, P1 | PD0, PD0 | PD1, PD1 | PD2, PD2 => true | _, _ => false end.

Definition vis (st : vst) : option (vst * bool) :=
let '(ls, b, i) := st in
match visit3 ls with
| Some (ls', p) => Some ((ls', b, i), p)
| None =>
  if forallb fullb ls then
… +9 lines

Definition b1s (b : lab1) (X : side) : side := ev_runs [] (blk1 b) X.

Definition Gc (st : vst) (nus : list (list N)) (R : side) : Q * tape :=
let '(ls, b, i) := st in chs ls nus (b1s b (LWs i)) <{{D}} R.

Definition Gx (st : vst) (nus : list (list N)) (p : bool) (R : side) : Q * tape :=
let '(ls, b, i) := st in chs ls nus (b1s b (LWs i)) {{stp p}}> R.

Definition vlen (st : vst) : nat := let '(ls, _, _) := st in length ls.

Lemma lab1_eqb_eq a b : lab1_eqb a b = true -> a = b.

Lemma vis_spec st st' p nus R : vis st = Some (st', p) -> vlen st = length nus ->
Gc st nus R -->+ Gx st' nus p R /\ vlen st' = vlen st.

Definition Ep (p : bool) (R R' : side) : Prop := forall l, l {{stp p}}> R -->* l <{{D}} R'.

Fixpoint EpSeq (ps : list bool) (R R' : side) : Prop :=
match ps with
| [] => R = R'
| p :: ps' => exists R1, Ep p R R1 /\ EpSeq ps' R1 R'
end.

Fixpoint runv (n : nat) (st : vst) : option (vst * list bool) :=
match n with
| O => Some (st, [])
| S n' =>
  match vis st with
  | Some (st1, p) => match runv n' st1 with Some (st2, ps) => Some (st2, p :: ps) | None => None end
… +3 lines

Lemma runv_spec n : forall st st' ps nus R R', runv n st = Some (st', ps) -> vlen st = length nus ->
EpSeq ps R R' -> Gc st nus R -->* Gc st' nus R'.

Lemma runv_add a : forall b st st1 ps1 st2 ps2,
runv a st = Some (st1, ps1) -> runv b st1 = Some (st2, ps2) -> runv (a + b) st = Some (st2, ps1 ++ ps2).

Lemma runv_one st st' p : vis st = Some (st', p) -> runv 1 st = Some (st', [p]).

Lemma vis3 ls ls' p b i : visit3 ls = Some (ls', p) -> vis (ls, b, i) = Some ((ls', b, i), p).

Lemma repeat_add {X} (x : X) n m : repeat x (n + m) = repeat x n ++ repeat x m.

Lemma repeat_snoc {X} (x : X) n l : repeat x n ++ x :: l = repeat x (S n) ++ l.

Lemma pow3_pos j : 1 <= 3 ^ j.

Lemma visit3_U2 j X X' : visit3 X = Some (X', true) -> visit3 (repeat U2 j ++ X) = Some (repeat U0 j ++ X', true).

Lemma cb_U2 j X p X' : cb X p = Some (X', true) -> cb (repeat U2 j ++ X) p = Some (repeat U0 j ++ X', true).

Lemma visit3_full ls : forallb fullb ls = true -> visit3 ls = None.

Lemma fullb_U2 j : forallb fullb (repeat U2 j) = true.

Lemma fullb_D0 j : forallb fullb (repeat D0 j) = true.

Lemma fullb_app a b : forallb fullb a = true -> forallb fullb b = true -> forallb fullb (a ++ b) = true.

Lemma rep_app {X} (x : X) a b : repeat x a ++ repeat x b = repeat x (a + b).

Lemma CU j : forall rest b i,
runv (3 ^ j - 1) (repeat U0 j ++ rest, b, i) = Some ((repeat U2 j ++ rest, b, i), repeat true (3 ^ j - 1)).

Lemma CW j : forall rest b i,
runv (3 ^ S j - 1) (repeat U0 j ++ W0 :: rest, b, i) =
  Some ((repeat U2 j ++ D0 :: rest, b, i), repeat true (3 ^ S j - 1)).

Fixpoint tc (j : nat) : nat :=
match j with
| O => 0
| S O => 2
| S j' => 3 ^ j + tc j'
end.

Lemma tc_closed j : 2 * tc (S j) + 5 = 3 ^ S (S j).

Lemma S3 j : forall d d' rest b i, turn d = Some (d', false) ->
runv (tc (S j) + 1) (repeat U0 j ++ W0 :: d :: rest, b, i) =
  Some ((D2 :: repeat D1 j ++ d' :: rest, b, i), repeat true (tc (S j)) ++ [false]).

Definition isD (s : lab) : bool := match s with D0 | D1 | D2 => true | _ => false end.

Definition dv (s : lab) : nat := match s with D1 => 1 | D0 => 2 | _ => 0 end.

Fixpoint dval (ls : list lab) : nat := match ls with [] => 0 | s :: ls' => dv s + 3 * dval ls' end.

Definition dv1 (b : lab1) : nat := match b with PD1 => 1 | PD0 => 2 | _ => 0 end.

Definition isD1 (b : lab1) : bool := match b with PD0 | PD1 | PD2 => true | _ => false end.

Lemma dval_lt ls : forallb isD ls = true -> dval ls < 3 ^ length ls.

Lemma dval_max ls : forallb isD ls = true -> dval ls + 1 = 3 ^ length ls -> ls = repeat D0 (length ls).

Lemma visit3_D ls : forallb isD ls = true -> dval ls + 1 < 3 ^ length ls ->
exists ls', visit3 ls = Some (ls', false) /\ forallb isD ls' = true /\ dval ls' = dval ls + 1 /\
  length ls' = length ls.

Lemma cb_D0 j : cb (repeat D0 j) false = Some (repeat D2 j, false).

Lemma isD_D2 j : forallb isD (repeat D2 j) = true.

Lemma dval_D2 j : dval (repeat D2 j) = 0.

Lemma dval_D1 j : 2 * dval (repeat D1 j) + 1 = 3 ^ j.

Lemma isD_D1 j : forallb isD (repeat D1 j) = true.

Lemma vis_b1 ls b b' p1 ls' p i : forallb fullb ls = true -> turn1 b = Some (b', p1) -> cb ls p1 = Some (ls', p) ->
vis (ls, b, i) = Some ((ls', b', i), p).

Lemma vis_co ls ls' p i : forallb fullb ls = true -> i < 80 -> cb ls false = Some (ls', p) ->
vis (ls, PD0, i) = Some ((ls', PD2, S i), p).

Lemma allD n : forall ls b i, forallb isD ls = true -> isD1 b = true ->
dval ls + 3 ^ length ls * dv1 b + n + 1 = 3 ^ S (length ls) ->
runv n (ls, b, i) = Some ((repeat D0 (length ls), PD0, i), repeat false n).

Lemma cyc m i : i < 80 ->
runv (3 ^ S m) (repeat D0 m, PD0, i) = Some ((repeat D0 m, PD0, S i), repeat false (3 ^ S m)).

Lemma cycs c : forall m i, i + c <= 80 ->
runv (c * 3 ^ S m) (repeat D0 m, PD0, i) = Some ((repeat D0 m, PD0, i + c), repeat false (c * 3 ^ S m)).

Lemma rep_app_cons {X} (x : X) a b l : repeat x a ++ (repeat x b ++ l) = repeat x (a + b) ++ l.

Lemma odd_pow3 j : exists k, 3 ^ j = 2 * k + 1.

Lemma half9 j : 2 * ((9 * 3 ^ j + 1) / 2) = 9 * 3 ^ j + 1.

Lemma interval m : 2 <= m ->
exists T, 2 * T + 5 = 3 ^ S (S m) /\
runv (81 * 3 ^ S m - 1) (repeat U0 m, P0, 0) =
  Some ((repeat D0 m, PD0, 80), repeat true T ++ repeat false (81 * 3 ^ S m - 1 - T)).

Lemma interval_tm m nus R R' : 2 <= m -> length nus = m ->
(forall T, 2 * T + 5 = 3 ^ S (S m) -> EpSeq (repeat true T ++ repeat false (81 * 3 ^ S m - 1 - T)) R R') ->
Gc (repeat U0 m, P0, 0) nus R -->* Gc (repeat D0 m, PD0, 80) nus R'.

Lemma record_visit m nus R : length nus = m ->
Gc (repeat D0 m, PD0, 80) nus R -->+ chs (repeat D2 m) nus (b1s PD2 (LWs 81)) {{B}}> R.

Fixpoint urun (p : positive) (c : cfg) : cfg * bool :=
match p with
| xH => match sstep c with Some (c', _) => (c', false) | None => (c, true) end
| xO p' => let '(c1, s1) := urun p' c in if s1 then (c1, true) else urun p' c1
| xI p' =>
  match sstep c with
… +4 lines

Lemma sstep_ev nu sg c c' b : sstep c = Some (c', b) -> ev_cfg nu sg c -->* ev_cfg nu sg c'.

Lemma urun_spec p : forall c nu sg, ev_cfg nu sg c -->* ev_cfg nu sg (fst (urun p c)).

Definition tgtD (c : cfg) : option (list run) :=
match c with
| Lc D ([], TV O) (rr, T0) => Some rr
| _ => None
end.

Lemma tgtD_spec c rr : tgtD c = Some rr -> c = Lc D ([], TV 0) (rr, T0).

Definition evR (nu : list N) (rr : list run) : side := ev_runs nu rr (const S0).

Definition ep_run (p : bool) (rr : list run) : option (list run) :=
tgtD (fst (urun 50000 (Rc (stp p) ([], TV 0) (rr, T0)))).

Lemma ep_run_spec p rr rr' : ep_run p rr = Some rr' -> forall nu, Ep p (evR nu rr) (evR nu rr').

Fixpoint eps (ps : list bool) (rr : list run) : option (list run) :=
match ps with
| [] => Some rr
| p :: ps' => match ep_run p rr with Some rr' => eps ps' rr' | None => None end
end.

Lemma eps_spec ps : forall rr rr', eps ps rr = Some rr' -> forall nu, EpSeq ps (evR nu rr) (evR nu rr').

Lemma EpSeq_app a : forall b R R1 R2, EpSeq a R R1 -> EpSeq b R1 R2 -> EpSeq (a ++ b) R R2.

Definition evN (nu : list N) (a : lf) : N := (lc a + dot (lv a) nu)%N.

Lemma dot_zadd2 v : forall a b, dot v (zadd a b) = (dot v a + dot v b)%N.

Definition vscale (k : N) (w : list N) : list N := map (N.mul k) w.

Lemma dot_vscale v : forall k w, dot v (vscale k w) = (k * dot v w)%N.

Lemma ev_runs_dot nu nu' T X : (forall v, dot v nu = dot v nu') -> ev_runs nu T X = ev_runs nu' T X.

Definition subst_lf (w : list N) (a : lf) : lf := LF (lc a + dot (lv a) w) (lv a).

Definition subst_runs (w : list N) (T : list run) : list run := map (fun r => (fst r, subst_lf w (snd r))) T.

Lemma ev_runs_subst nu w T X : ev_runs nu (subst_runs w T) X = ev_runs (zadd nu w) T X.

Definition lf_scale (k : N) (a : lf) : lf := LF (k * lc a) (map (N.mul k) (lv a)).

Lemma dot_scale_l vs : forall k nu, dot (map (N.mul k) vs) nu = (k * dot vs nu)%N.

Lemma evN_add nu a b : evN nu (lf_add a b) = (evN nu a + evN nu b)%N.

Lemma evN_scale nu k a : evN nu (lf_scale k a) = (k * evN nu a)%N.

Fixpoint comp_aux (vs : list N) (sg : list lf) : lf :=
match vs, sg with
| v :: vs', s :: sg' => lf_add (lf_scale v s) (comp_aux vs' sg')
| _, _ => LF 0 []
end.

Definition compose_lf (sg : list lf) (a : lf) : lf := lf_add (LF (lc a) []) (comp_aux (lv a) sg).

Definition comp_runs (sg : list lf) (T : list run) : list run := map (fun r => (fst r, compose_lf sg (snd r))) T.

Lemma evN_comp_aux nu vs : forall sg, evN nu (comp_aux vs sg) = dot vs (map (evN nu) sg).

Lemma evN_compose nu sg a : evN nu (compose_lf sg a) = evN (map (evN nu) sg) a.

Lemma ev_runs_comp nu sg T X : ev_runs nu (comp_runs sg T) X = ev_runs (map (evN nu) sg) T X.

Lemma jump_lemma T p dec inc :
(forall nu, EpSeq [p; p; p; p] (evR nu (subst_runs dec T)) (evR nu (subst_runs inc T))) ->
forall k nu, EpSeq (repeat p (4 * k)) (evR (zadd nu (vscale (N.of_nat k) dec)) T)
                                      (evR (zadd nu (vscale (N.of_nat k) inc)) T).

Definition uvar (i : nat) (c : N) : lf := LF c (repeat 0%N i ++ [4%N]).

Fixpoint zsub (a b : list N) : list N :=
match a, b with
| x :: a', y :: b' => (x - y)%N :: zsub a' b'
| _, [] => a
| [], _ => []
end.

Fixpoint mk_jump (i : nat) (rr rr4 : list run) (c : lf) : option (list run * list N * list N * list lf) :=
match rr, rr4 with
| [], [] => Some ([], [], [], [])
| (b, a) :: rr', (b4, a4) :: rr4' =>
  if negb (seqb b b4) then None else
  if negb (listN_eqb (strip0 (lv a)) (strip0 (lv a4))) then None else
… +19 lines

Fixpoint mapadd (c : lf) (sg : list lf) (w : list N) : list lf :=
match sg, w with
| s :: sg', x :: w' => lf_add s (lf_scale x c) :: mapadd c sg' w'
| _, _ => []
end.

Lemma mapadd_ev nu c sg : forall w, length sg = length w ->
map (evN nu) (mapadd c sg w) = zadd (map (evN nu) sg) (vscale (evN nu c) w).

Definition cyc4 (p : bool) : list bool := [p; p; p; p].

Definition jump_run (p : bool) (c : lf) (rr : list run) : option (list run) :=
match eps (cyc4 p) rr with
| None => None
| Some rr4 =>
  match mk_jump 0 rr rr4 c with
  | None => None
… +11 lines

Lemma jump_run_spec p c rr rr' : jump_run p c rr = Some rr' ->
forall nu, EpSeq (repeat p (4 * ev nu c)) (evR nu rr) (evR nu rr').

Inductive instr := ISingle (p : bool) | IJump (p : bool) (c : lf).

Definition seg : Type := (bool * lf)%type.

Fixpoint segs_ev (nu : list N) (ss : list seg) : list bool :=
match ss with [] => [] | (p, n) :: ss' => repeat p (ev nu n) ++ segs_ev nu ss' end.

Fixpoint exec (prog : list instr) (rr : list run) : option (list run * list seg) :=
match prog with
| [] => Some (rr, [])
| ISingle p :: prog' =>
  match ep_run p rr with
  | Some rr1 => match exec prog' rr1 with Some (rr2, ss) => Some (rr2, (p, cn 1) :: ss) | None => None end
… +8 lines

Lemma ev_scale4 nu c : ev nu (lf_scale 4 c) = 4 * ev nu c.

Lemma exec_spec prog : forall rr rr' ss, exec prog rr = Some (rr', ss) ->
forall nu, EpSeq (segs_ev nu ss) (evR nu rr) (evR nu rr').

Fixpoint sum_ph (p : bool) (ss : list seg) : lf :=
match ss with
| [] => LF 0 []
| (q, n) :: ss' => if Bool.eqb p q then lf_add n (sum_ph p ss') else sum_ph p ss'
end.

Fixpoint split_ok (seen_false : bool) (ss : list seg) : bool :=
match ss with
| [] => true
| (true, _) :: ss' => andb (negb seen_false) (split_ok false ss')
| (false, _) :: ss' => split_ok true ss'
end.

Lemma ev_lf_add nu a b : ev nu (lf_add a b) = ev nu a + ev nu b.

Lemma split_false ss nu : split_ok true ss = true -> segs_ev nu ss = repeat false (ev nu (sum_ph false ss)).

Lemma sum_false_true ss : split_ok true ss = true -> sum_ph true ss = LF 0 [] \/ True.

Lemma split_spec ss nu : split_ok false ss = true ->
segs_ev nu ss = repeat true (ev nu (sum_ph true ss)) ++ repeat false (ev nu (sum_ph false ss)).

Definition prog_check (prog : list instr) (rs re : list run) (T F : lf) : bool :=
match exec prog rs with
| Some (re', ss) =>
  andb (andb (runs_eqb re' re) (split_ok false ss)) (andb (lf_eqb (sum_ph true ss) T) (lf_eqb (sum_ph false ss) F))
| None => false
end.

Lemma prog_check_spec prog rs re T F : prog_check prog rs re T F = true ->
forall nu, EpSeq (repeat true (ev nu T) ++ repeat false (ev nu F)) (evR nu rs) (evR nu re).

Definition tl1 (c a : N) : lf := LF c [a].

Definition Rs_r5 : list run := mkruns S0 [tl1 224492 1796256; tl1 673559 5388768; cn 8; tl1 9836 78732; tl1 1942069 15536448]%N.

Definition prog_r5 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 817 6561)] ++ repeat (ISingle true) 6 ++ repeat (ISingle false) 13 ++ [IJump false (tl1 43462 347733)] ++ repeat (ISingle false) 7.

Definition Rs_r0 : list run := mkruns S0 [tl1 74804 598752; tl1 224495 1796256; tl1 673560 5388768; tl1 2020752 16166304; cn 4; tl1 521610 4172796; cn 1]%N.

Definition prog_r0 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 817 6561)] ++ repeat (ISingle true) 6 ++ repeat (ISingle false) 9 ++ [IJump false (tl1 43463 347733)] ++ repeat (ISingle false) 7.

Definition Rs_r1 : list run := mkruns S0 [tl1 2020748 16166304; cn 7; tl1 551120 4408992; tl1 1564809 12518388; cn 2]%N.

Definition prog_r1 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 2457 19683)] ++ repeat (ISingle true) 7 ++ repeat (ISingle false) 5 ++ [IJump false (tl1 130398 1043199)] ++ repeat (ISingle false) 4.

Definition Rs_r2 : list run := mkruns S0 [tl1 8276 66528; tl1 24911 199584; tl1 74808 598752; tl1 224496 1796256; tl1 673559 5388768; tl1 2020751 16166304; cn 8; tl1 29514 236196; tl1 5826224 46609344; cn 2]%N.

Definition prog_r2 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 817 6561)] ++ repeat (ISingle true) 6 ++ repeat (ISingle false) 8 ++ [IJump false (tl1 43464 347733)] ++ repeat (ISingle false) 4.

Definition Rs_r3 : list run := mkruns S0 [tl1 224492 1796256; tl1 673559 5388768; tl1 2020752 16166304; tl1 6062328 48498912; cn 4; tl1 1564810 12518388]%N.

Definition prog_r3 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 2457 19683)] ++ repeat (ISingle true) 7 ++ repeat (ISingle false) 9 ++ [IJump false (tl1 130397 1043199)] ++ repeat (ISingle false) 4.

Definition Rs_r4 : list run := mkruns S0 [tl1 74804 598752; tl1 224495 1796256; tl1 673560 5388768; tl1 2020752 16166304; tl1 6062327 48498912; cn 7; tl1 1653368 13226976; tl1 4694422 37555164; cn 1]%N.

Definition prog_r4 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 2457 19683)] ++ repeat (ISingle true) 7 ++ repeat (ISingle false) 6 ++ [IJump false (tl1 130397 1043199)] ++ repeat (ISingle false) 7.

Definition Re_r5 : list run := [(S0, tl1 224492 1796256); (S1, tl1 673560 5388768); (S0, tl1 2020752 16166304); (S1, cn 4); (S0, tl1 521602 4172796)]%N.

Lemma int_r5 : prog_check prog_r5 Rs_r5 Re_r5 (tl1 3278 26244) (tl1 173868 1390932) = true.

Definition Re_r0 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, tl1 2020751 16166304); (S1, cn 7); (S1, tl1 551120 4408992); (S0, tl1 1564798 12518388); (S1, cn 1)]%N.

Lemma int_r0 : prog_check prog_r0 Rs_r0 Re_r0 (tl1 3278 26244) (tl1 173868 1390932) = true.

Definition Re_r1 : list run := [(S0, tl1 2020748 16166304); (S1, cn 8); (S0, tl1 29521 236196); (S0, tl1 5826161 46609344); (S0, cn 2)]%N.

Lemma int_r1 : prog_check prog_r1 Rs_r1 Re_r1 (tl1 9839 78732) (tl1 521601 4172796) = true.

Definition Re_r2 : list run := [(S0, tl1 8276 66528); (S1, tl1 24912 199584); (S0, tl1 74808 598752); (S1, tl1 224495 1796256); (S1, tl1 673559 5388768); (S1, tl1 2020752 16166304); (S0, tl1 6062328 48498912); (S1, cn 3); (S1, tl1 1564801 12518388); (S1, cn 1)]%N.

Lemma int_r2 : prog_check prog_r2 Rs_r2 Re_r2 (tl1 3278 26244) (tl1 173868 1390932) = true.

Definition Re_r3 : list run := [(S0, tl1 224492 1796256); (S1, tl1 673560 5388768); (S0, tl1 2020752 16166304); (S1, tl1 6062327 48498912); (S1, cn 7); (S1, tl1 1653368 13226976); (S0, tl1 4694397 37555164); (S0, cn 2)]%N.

Lemma int_r3 : prog_check prog_r3 Rs_r3 Re_r3 (tl1 9839 78732) (tl1 521601 4172796) = true.

Definition Re_r4 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, tl1 2020751 16166304); (S1, tl1 6062327 48498912); (S1, cn 7); (S1, tl1 88573 708588); (S1, tl1 17478488 139828032); (S0, cn 2)]%N.

Lemma int_r4 : prog_check prog_r4 Rs_r4 Re_r4 (tl1 9839 78732) (tl1 521601 4172796) = true.

Definition rtop (qs : list (list N)) (z : N) : N :=
match qs with [] => z | q :: _ => nth 0 q 0%N end.

Fixpoint rshift (qs : list (list N)) (z : N) : list (list N) :=
match qs with
| [] => []
| q :: qs' => [nth 1 q 0; nth 2 q 0; nth 3 q 0; rtop qs' z]%N :: rshift qs' z
end.

Lemma shift_len qs z : length (rshift qs z) = length qs.

Lemma dot4 (a b c d : N) q :
dot [a; b; c; d] q = (a * nth 0 q 0 + b * nth 1 q 0 + c * nth 2 q 0 + d * nth 3 q 0)%N.

Lemma alt_split b m k : Nat.eqb (m mod 2) 0 = true -> alt b (m + k) = alt b m ++ alt b k.

Lemma ev_q nu c a : ev nu (LF c a) = N.to_nat (c + dot a nu).

Lemma regroup qs : forall z X X',
X = alt S0 1 *> (alt S0 (2 + 4 * N.to_nat z) *> X') ->
chs (repeat D2 (length qs)) qs X =
  alt S0 1 *> (alt S0 (2 + 4 * N.to_nat (rtop qs z)) *> chs (repeat U0 (length qs)) (rshift qs z) X').

Lemma regroup_b1 : b1s PD2 (LWs 81) = alt S0 1 *> (alt S0 (2 + 4 * N.to_nat 0) *> b1s P0 (LWs 0)).

Lemma drop_step L Re Rs nu X' :
reach 100000 (Rc B (L, TV 0) (Re, T0)) (Lc D ([], TV 0) (Rs, T0)) = true ->
ev_runs nu L X' {{B}}> evR nu Re -->+ X' <{{D}} evR nu Rs.

Definition W5t (t : N) : N := (18701 + 149688 * t)%N.

Definition W5s (t : N) : N := (6227 + 49896 * t)%N.

Definition W5a (t : N) : N := (2069 + 16632 * t)%N.

Lemma rec_r5_ok : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 74806 598752)], TV 0) (Re_r5, T0)) (Lc D ([], TV 0) (Rs_r0, T0)) = true.

Lemma step_r5 t f1 deep :
chs (repeat D2 (S (length deep))) ([W5t t; W5s t; W5a t; f1] :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r5 -->+
Gc (repeat U0 (S (length deep)), P0, 0) ([W5s t; W5a t; f1; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r0).

Lemma pow_K0 k0 e : 2 <= e -> 3 ^ (k0 + 2 * e) = 3 ^ (k0 + 4) * 9 ^ (e - 2).

Lemma S_r5 e t f1 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
Gc (repeat U0 (S (length deep)), P0, 0) ([W5t t; W5s t; W5a t; f1] :: deep) (evR [t] Rs_r5) -->+
Gc (repeat U0 (S (length deep)), P0, 0) ([W5s t; W5a t; f1; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r0).

Definition wv (c a t : N) : N := (c + a * t)%N.

Lemma evN_tl1 c a t : evN [t] (tl1 c a) = wv c a t.

Lemma take_step L first4 Re' Rs nu sg X' :
reach 100000 (Rc B (L, TV 0) (first4, TV 1)) (Rc A (comp_runs sg (blk U0), TV 0) ([], TV 1)) = true ->
ep_run true Re' = Some Rs ->
ev_runs nu L X' {{B}}> ev_runs nu first4 (evR nu Re') -->+
  ev_runs (map (evN nu) sg) (blk U0) X' <{{D}} evR nu Rs.

Lemma split4 nu r1 r2 r3 b c v rest X :
ev_runs nu (r1 :: r2 :: r3 :: (b, LF (3 + c) v) :: rest) X =
ev_runs nu [r1; r2; r3; (b, cn 3)] (ev_runs nu ((sneg b, LF c v) :: rest) X).

Definition W0t := wv 6227 49896.

Definition W0s := wv 2069 16632.

Definition W1t := wv 168389 1347192.

Definition W1s := wv 56123 449064.

Definition W1a := wv 18701 149688.

Definition W1I := wv 6227 49896.

Definition W1u := wv 2069 16632.

Definition sig01 : list lf := [tl1 168389 1347192; tl1 56123 449064; tl1 18701 149688; tl1 6227 49896]%N.

Definition f4_r0 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, cn 3)]%N.

Definition Rp_r0 : list run := [(S0, tl1 2020748 16166304); (S1, cn 7); (S1, tl1 551120 4408992); (S0, tl1 1564798 12518388); (S1, cn 1)]%N.

Lemma rec_r0a : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 24910 199584)], TV 0) (f4_r0, TV 1))
(Rc A (comp_runs sig01 (blk U0), TV 0) ([], TV 1)) = true.

Lemma rec_r0b : ep_run true Rp_r0 = Some Rs_r1.

Lemma split_r0 t : evR [t] Re_r0 = ev_runs [t] f4_r0 (evR [t] Rp_r0).

Lemma step_r0 t f1 f2 deep :
chs (repeat D2 (S (length deep))) ([W0t t; W0s t; f1; f2] :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r0 -->+
Gc (repeat U0 (S (S (length deep))), P0, 0)
   ([W1t t; W1s t; W1a t; W1I t] :: [W0s t; f1; f2; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r1).

Definition W3t := wv 18701 149688.

Lemma rec_r3_ok : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 74806 598752)], TV 0) (Re_r3, T0)) (Lc D ([], TV 0) (Rs_r4, T0)) = true.

Lemma step_r3 t f1 f2 f3 deep :
chs (repeat D2 (S (length deep))) ([W3t t; f1; f2; f3] :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r3 -->+
Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r4).

Definition sig12 : list lf := [tl1 56123 449064; tl1 18701 149688; tl1 6227 49896; tl1 2069 16632]%N.

Lemma rec_r1_ok : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 673558 5388768)] ++ comp_runs sig12 (blk U0), TV 0) (Re_r1, T0))
(Lc D ([], TV 0) (Rs_r2, T0)) = true.

Lemma step_r1 t f1 f2 f3 deep :
chs (repeat D2 (S (S (length deep)))) ([W1t t; W1s t; W1a t; W1I t] :: [W1u t; f1; f2; f3] :: deep) (b1s PD2 (LWs 81))
  {{B}}> evR [t] Re_r1 -->+
Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r2).

Definition xv : lf := LF 2 [0; 4]%N.

Definition sig23 : list lf := [tl1 18701 149688; tl1 6227 49896; tl1 2069 16632; LF 0 [0; 1]]%N.

Definition f4_r2 : list run := [(S0, tl1 8276 66528); (S1, tl1 24912 199584); (S0, tl1 74808 598752); (S1, cn 3)]%N.

Definition Rp_r2 : list run := [(S0, tl1 224492 1796256); (S1, tl1 673559 5388768); (S1, tl1 2020752 16166304);
(S0, tl1 6062328 48498912); (S1, cn 3); (S1, tl1 1564801 12518388); (S1, cn 1)]%N.

Lemma rec_r2a : reach 100000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (f4_r2, TV 1))
(Rc A (comp_runs sig23 (blk U0), TV 0) ([], TV 1)) = true.

Lemma rec_r2b : ep_run true Rp_r2 = Some Rs_r3.

Lemma split_r2 nu : evR nu Re_r2 = ev_runs nu f4_r2 (evR nu Rp_r2).

Lemma step_r2 t q deep :
chs (repeat D2 (S (length deep))) (q :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r2 -->+
Gc (repeat U0 (S (S (length deep))), P0, 0)
   ([W3t t; wv 6227 49896 t; wv 2069 16632 t; nth 0 q 0%N] :: rshift (q :: deep) 0%N) (evR [t] Rs_r3).

Definition sub9_lf (l : lf) : lf := match lv l with [a] => LF (lc l + a) [9 * a] | _ => l end%N.

Definition sub9 (rs : list run) : list run := map (fun r => (fst r, sub9_lf (snd r))) rs.

Lemma ev_runs_sub9 t rs X : forallb (fun r => Nat.leb (length (lv (snd r))) 1) rs = true ->
ev_runs [t] (sub9 rs) X = ev_runs [(1 + 9 * t)%N] rs X.

Lemma evR_sub9_r5 t : evR [t] (sub9 Rs_r5) = evR [(1 + 9 * t)%N] Rs_r5.

Definition sig45 : list lf := [tl1 168389 1347192; tl1 56123 449064; tl1 18701 149688; LF 0 [0; 1]]%N.

Definition f4_r4 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, cn 3)]%N.

Definition Rp_r4 : list run := [(S0, tl1 2020748 16166304); (S1, tl1 6062327 48498912); (S1, cn 7);
(S1, tl1 88573 708588); (S1, tl1 17478488 139828032); (S0, cn 2)]%N.

Lemma rec_r4a : reach 100000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (f4_r4, TV 1))
(Rc A (comp_runs sig45 (blk U0), TV 0) ([], TV 1)) = true.

Lemma rec_r4b : ep_run true Rp_r4 = Some (sub9 Rs_r5).

Lemma split_r4 nu : evR nu Re_r4 = ev_runs nu f4_r4 (evR nu Rp_r4).

Lemma step_r4 t q deep :
chs (repeat D2 (S (length deep))) (q :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r4 -->+
Gc (repeat U0 (S (S (length deep))), P0, 0)
   ([W5t (1 + 9 * t); W5s (1 + 9 * t); W5a (1 + 9 * t); nth 0 q 0%N] :: rshift (q :: deep) 0%N)
   (evR [(1 + 9 * t)%N] Rs_r5).

Lemma S_r0 e t f1 f2 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
Gc (repeat U0 (S (length deep)), P0, 0) ([W0t t; W0s t; f1; f2] :: deep) (evR [t] Rs_r0) -->+
Gc (repeat U0 (S (S (length deep))), P0, 0) ([W1t t; W1s t; W1a t; W1I t] :: [W0s t; f1; f2; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r1).

Lemma S_r1 e t f1 f2 f3 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
Gc (repeat U0 (S (S (length deep))), P0, 0) ([W1t t; W1s t; W1a t; W1I t] :: [W1u t; f1; f2; f3] :: deep) (evR [t] Rs_r1) -->+
Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r2).

Lemma S_r2 e t q deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
Gc (repeat U0 (S (length deep)), P0, 0) (q :: deep) (evR [t] Rs_r2) -->+
Gc (repeat U0 (S (S (length deep))), P0, 0) ([W3t t; wv 6227 49896 t; wv 2069 16632 t; nth 0 q 0%N] :: rshift (q :: deep) 0%N) (evR [t] Rs_r3).

Lemma S_r3 e t f1 f2 f3 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 2 + 2 * e ->
Gc (repeat U0 (S (length deep)), P0, 0) ([W3t t; f1; f2; f3] :: deep) (evR [t] Rs_r3) -->+
Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r4).

Lemma S_r4 e t q deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 2 + 2 * e ->
Gc (repeat U0 (S (length deep)), P0, 0) (q :: deep) (evR [t] Rs_r4) -->+
Gc (repeat U0 (S (S (length deep))), P0, 0) ([W5t (1 + 9 * t); W5s (1 + 9 * t); W5a (1 + 9 * t); nth 0 q 0%N] :: rshift (q :: deep) 0%N) (evR [(1 + 9 * t)%N] Rs_r5).

Definition mkc (rc : bool) (q : Q) (l r : list (Sym * N)) : cfg :=
let f := map (fun x : Sym * N => (fst x, cn (snd x))) in
if rc then Rc q (f l, T0) (f r, T0) else Lc q (f l, T0) (f r, T0).

Lemma ck_0 : runp 500000 b28_0 = Some (b28_1, true).

Lemma ck_1 : runp 500000 b28_1 = Some (b28_2, true).

Lemma ck_2 : runp 500000 b28_2 = Some (b28_3, true).

Lemma ck_3 : runp 500000 b28_3 = Some (b28_4, true).

Lemma ck_4 : runp 500000 b28_4 = Some (b28_5, true).

Lemma ck_5 : runp 500000 b28_5 = Some (b28_6, true).

Lemma ck_6 : runp 500000 b28_6 = Some (b28_7, true).

Lemma ck_7 : runp 500000 b28_7 = Some (b28_8, true).

Lemma ck_8 : runp 500000 b28_8 = Some (b28_9, true).

Lemma ck_9 : runp 500000 b28_9 = Some (b28_10, true).

Lemma ck_10 : runp 500000 b28_10 = Some (b28_11, true).

Lemma ck_11 : runp 500000 b28_11 = Some (b28_12, true).

Lemma ck_12 : runp 500000 b28_12 = Some (b28_13, true).

Lemma ck_13 : runp 500000 b28_13 = Some (b28_14, true).

Lemma ck_14 : runp 500000 b28_14 = Some (b28_15, true).

Lemma ck_15 : runp 500000 b28_15 = Some (b28_16, true).

Lemma ck_16 : runp 500000 b28_16 = Some (b28_17, true).

Lemma ck_17 : runp 500000 b28_17 = Some (b28_18, true).

Lemma ck_18 : runp 500000 b28_18 = Some (b28_19, true).

Lemma ck_19 : runp 500000 b28_19 = Some (b28_20, true).

Lemma ck_20 : runp 500000 b28_20 = Some (b28_21, true).

Lemma ck_21 : runp 500000 b28_21 = Some (b28_22, true).

Lemma ck_22 : runp 500000 b28_22 = Some (b28_23, true).

Lemma ck_23 : runp 500000 b28_23 = Some (b28_24, true).

Lemma ck_24 : runp 500000 b28_24 = Some (b28_25, true).

Lemma ck_25 : runp 500000 b28_25 = Some (b28_26, true).

Lemma ck_26 : runp 500000 b28_26 = Some (b28_27, true).

Lemma ck_27 : runp 500000 b28_27 = Some (b28_28, true).

Lemma ck_28 : runp 500000 b28_28 = Some (b28_29, true).

Lemma ck_29 : runp 500000 b28_29 = Some (b28_30, true).

Lemma ck_30 : runp 500000 b28_30 = Some (b28_31, true).

Lemma ck_31 : runp 500000 b28_31 = Some (b28_32, true).

Lemma ck_32 : runp 500000 b28_32 = Some (b28_33, true).

Lemma ck_33 : runp 500000 b28_33 = Some (b28_34, true).

Lemma ck_34 : runp 500000 b28_34 = Some (b28_35, true).

Lemma ck_35 : runp 500000 b28_35 = Some (b28_36, true).

Lemma ck_36 : runp 500000 b28_36 = Some (b28_37, true).

Lemma ck_ev p c c' : runp p c = Some (c', true) ->
ev_cfg [] (fun _ => const S0) c -->* ev_cfg [] (fun _ => const S0) c'.

Inductive cls := C5 | C0 | C1 | C2 | C3 | C4.

Definition Rs (r : cls) : list run :=
match r with C5 => Rs_r5 | C0 => Rs_r0 | C1 => Rs_r1 | C2 => Rs_r2 | C3 => Rs_r3 | C4 => Rs_r4 end.

Definition ist : Type := (cls * nat * N * list (list N))%type.

Definition cfgI (s : ist) : Q * tape :=
let '(r, e, t, nus) := s in Gc (repeat U0 (length nus), P0, 0) nus (evR [t] (Rs r)).

Definition win (r : cls) (e : nat) (t : N) (nus : list (list N)) : Prop :=
match r with
| C5 => exists f1 deep, nus = [W5t t; W5s t; W5a t; f1] :: deep /\ length deep = 1 + 2 * e
| C0 => exists f1 f2 deep, nus = [W0t t; W0s t; f1; f2] :: deep /\ length deep = 1 + 2 * e
| C1 => exists f1 f2 f3 deep, nus = [W1t t; W1s t; W1a t; W1I t] :: [W1u t; f1; f2; f3] :: deep /\
          length deep = 1 + 2 * e
… +4 lines

Definition Inv (s : ist) : Prop :=
let '(r, e, t, nus) := s in 2 <= e /\ 1 + 8 * N.to_nat t = 9 ^ (e - 2) /\ win r e t nus.

Lemma inv_step s : Inv s -> exists s', cfgI s -->+ cfgI s' /\ Inv s'.

Definition R28 : list run := [(S0, cn 224492); (S1, cn 673559); (S1, cn 7); (S1, cn 9841); (S1, cn 1942040); (S0, cn 2)]%N.

Lemma inv28 : Inv (C5, 2, 0%N, nus28).

Lemma split1 nu b c v rest X :
ev_runs nu ((b, LF (3 + c) v) :: rest) X = ev_runs nu [(b, cn 3)] (ev_runs nu ((sneg b, LF c v) :: rest) X).

Lemma b28a : reach 1000 (Rc B (L28, T0) ([(S1, cn 3)], TV 1)) (Rc A ((S0, cn 3) :: L28, T0) ([], TV 1)) = true.

Lemma b28b : ep_run true R28 = Some (map (fun r => (fst r, cn (evN [0%N] (snd r)))) Rs_r5).

Lemma b28_chain : ev_runs [] ((S0, cn 3) :: L28) (const S0) = chs (repeat U0 6) nus28 (b1s P0 (LWs 0)).

Lemma b28_right : evR [] (map (fun r => (fst r, cn (evN [0%N] (snd r)))) Rs_r5) = evR [0%N] Rs_r5.

Lemma base28 :
ev_runs [] L28 (const S0) {{B}}> ev_runs [] ((S1, cn 224495) :: tl R28) (const S0) -->*
cfgI (C5, 2, 0%N, nus28).