1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA

Definition tm := Eval compute in (TM_from_str "1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA").

Lemma LP0 l r : l <* <[0;1;1] {{C}}> [0] *> r -->+ l <{{A}} [1;0;0;1] *> r.

Lemma LP0z l : l <* <[0;1;1] {{C}}> 0inf -->+ l <{{A}} [1;0;0;1] *> 0inf.

Lemma LP11 l r : l <* <[0;1;1] {{C}}> [1;1;0] *> r -->+ l <{{A}} [1;0;1;0;0;0] *> r.

Lemma LPCr l e r : l <* <[0;1;1] {{C}}> [1;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <* <[0;1;1] {{C}}> r.

Lemma LPCl0 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+
l <{{A}} [1;0;0;0;0;1] *> [0;0;1]^^e *> [0;0;0] *> r.

Lemma LPCl1 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+
l <{{A}} [1;0;0;0;0;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.

Lemma LP5r l e r : l <* <[0;1;1] {{C}}> [1;0;0;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <* <[0;1;1] {{C}}> r.

Lemma LP5l0 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;0] *> r -->+
l <{{A}} [1;0;0;0;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.

Lemma LP5l1 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;1;0;0;0] *> r -->+
l <{{A}} [1;0;0;0;1] *> [0;0;1]^^(S (S e)) *> [0;0;0] *> r.

Lemma LP6r l e r : l <* <[0;1;1] {{C}}> [1;0;1;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
l <* <[0;1;1;1] <* <[1;1;0] <* [0] <* <[0;1;1]^^(S e) {{C}}> r.

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

Lemma RP0 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;0] *> r -->+
l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S n) {{C}}> r.

Lemma RP1 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;1;0;0;0] *> r -->+
l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S (S n)) {{C}}> r.

Lemma E1r l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;0;1]^^(S e) *> [0;0;0] *> r -->+
l <* <[1;1;0]^^(S (S a)) <* [0] <* <[0;1;1]^^(S e) {{C}}> r.

Lemma E2l0 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;1] *> [0;0;1]^^e *> [0;0;0] *> r.

Lemma E2l1 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.

Lemma Et0 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> 0inf -->+
l <{{E}} [0;1] *> [0;0;1]^^(S a) *> [0;0;0;1] *> 0inf.

Lemma Et1 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1] *> 0inf -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.

Lemma Et2 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;1;0;0;0;1] *> 0inf -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.

Lemma Et3 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1;1;0;0;0;1] *> 0inf -->+
l <* <[1;1;0]^^(S a) <* [0] <* <[0;1;1] {{C}}> [0;0;1] *> 0inf.

Lemma Rst k r : const 0 <{{E}} [0;1] *> [0;0;1]^^k *> [0;0;0] *> r -->+
const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^(S k) {{C}}> r.

Lemma LPT1 l : l <* <[0;1;1] {{C}}> [1] *> 0inf -->+ l <{{A}} [1;0;0;0;1;0;0;0;1] *> 0inf.

Lemma LPT2 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.

Lemma LPT3 l : l <* <[0;1;1] {{C}}> [1;0;1;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.

Lemma LPT4 l : l <* <[0;1;1] {{C}}> [1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.

Lemma LPT5 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.

Lemma LPT6 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.

Lemma z3 : [0;0;0] *> const 0 = const 0.

Inductive word : Type :=
| t0 | t1 | t2 | t3
| blk (d : bool) (e : nat) (w : word)
| p11 (x : nat) (w : word)
| p01 (x : nat) (w : word)
| p00 (w : word)
… +1 lines

Definition dsym (d : bool) : Sym := if d then S1 else S0.

Fixpoint enc (w : word) : side :=
match w with
| t0 => const 0
| t1 => [1] *> const 0
| t2 => [0;1;0;0;0;1] *> const 0
| t3 => [1;1;0;0;0;1] *> const 0
… +6 lines

Definition addb (e : nat) (d : bool) : nat := if d then S e else e.

Inductive LP : word -> word -> bool -> Prop :=
| LP_a e w : LP (blk false e w) (blk true e w) false
| LP_b e w w' d : LP w w' d -> LP (blk true e w) (blk false (addb e d) w') false
| LP_t0 : LP t0 t1 false
| LP_t1 : LP t1 t2 false
| LP_t2 : LP t2 t3 false
… +22 lines

Definition outp (d : bool) (r : side) : side :=
if d then [1;0;1;0;0;0] *> r else [1;0;0] *> r.

Definition LPspec (w w' : word) (d : bool) : Prop :=
forall l, l <* <[0;1;1] {{C}}> enc w -->+ l <{{A}} outp d (enc w').

Definition Phispec (a b : nat) (w : word) (k : nat) (y : word) : Prop :=
forall l, l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^b {{C}}> enc w -->+
          l <{{E}} [0;1] *> [0;0;1]^^k *> [0;0;0] *> enc y.

Lemma enc_a0 : enc (blk false 0 t0) = [0;0;1] *> const 0.

Theorem sound :
(forall w w' d, LP w w' d -> LPspec w w' d) /\
(forall a b w k y, Phi a b w k y -> Phispec a b w k y).

Definition K (N : nat) (y : word) : Q * tape :=
const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^N {{C}}> enc y.

Lemma epoch_tm N y k y' : Phi 1 N y k y' -> K N y -->+ K (S k) y'.

Fixpoint lpf (n : nat) (w : word) {struct n} : option (word * bool) :=
  match n with
  | O => None
  | S n' =>
    match w with
    | t0 => Some (t1, false)
… +58 lines

Lemma enc_p10t0 : enc (p10 t0) = enc t1.

Lemma enc_p10t1 : enc (p10 t1) = enc (blk true 0 t0).

Lemma enc_p00t0 : enc (p00 t0) = enc t0.

Lemma enc_p00t1 : enc (p00 t1) = enc (blk false 0 t0).

Lemma enc_p10p00t0 : enc (p10 (p00 t0)) = enc t1.

Lemma enc_p10p00t1 : enc (p10 (p00 t1)) = enc (p10 (blk false 0 t0)).

Lemma model_sound n :
(forall w w' d, lpf n w = Some (w', d) -> LP w w' d) /\
(forall a b w k y, phif n a b w = Some (k, y) -> Phi a b w k y).

Definition tl_of (s : nat) : word :=
match s with O => t0 | 1 => t1 | 2 => t2 | _ => t3 end.

Fixpoint gw (bs : list (bool * nat)) (s : nat) : word :=
match bs with [] => tl_of s | (d, e) :: bs => blk d e (gw bs s) end.

Fixpoint ginc (bs : list (bool * nat)) (s : nat) : list (bool * nat) * nat * bool :=
match bs with
| [] => match s with O => ([], 1, false) | 1 => ([], 2, false) | 2 => ([], 3, false)
        | _ => ([(false, 0)], O, true) end
| (false, e) :: bs => ((true, e) :: bs, s, false)
| (true, e) :: bs => let '(bs', s', d) := ginc bs s in ((false, addb e d) :: bs', s', false)
… +1 lines

Fixpoint gval (bs : list (bool * nat)) (s : nat) : nat :=
match bs with [] => 4 + s | (d, _) :: bs => (if d then 1 else 0) + 2 * gval bs s end.

Fixpoint gsum (bs : list (bool * nat)) : nat :=
match bs with [] => O | (_, e) :: bs => e + gsum bs end.

Lemma ginc_LP bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) -> LP (gw bs s) (gw bs' s') d.

Lemma ginc_val bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) ->
gval bs' s' = S (gval bs s) /\ s' <= 3 /\
gsum bs' + length bs + (if d then 1 else 0) = gsum bs + length bs' /\
(d = true -> bs = []) /\ length bs <= length bs'.

Lemma gval_ge bs s : 4 <= gval bs s.

Lemma gval_len bs s : length bs <= gval bs s.

Definition Psi (bs : list (bool * nat)) (s b : nat) : nat := gval bs s + b + gsum bs - length bs.

Definition blks := list (bool * nat).

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

Lemma addb_b2n e d : addb e d = e + b2n d.

Inductive GRes : Type := RE2 (k x : nat) (bs : blks) (s : nat) | RSp (k : nat) (y : word).

Definition rk (r : GRes) : nat := match r with RE2 k _ _ _ => k | RSp k _ => k end.

Definition ry (r : GRes) : word := match r with RE2 _ x bs s => p11 x (gw bs s) | RSp _ y => y end.

Inductive GPhi : nat -> nat -> blks -> nat -> GRes -> Prop :=
| GB a b bs s bs' s' d r : ginc bs s = (bs', s', d) -> GPhi (S a) (addb (S b) d) bs' s' r ->
    GPhi a (S (S b)) bs s r
| GE1 a e bs s r : GPhi (S (S a)) (S e) bs s r -> GPhi a 1 ((false, e) :: bs) s r
| GE2 a e bs s bs' s' d : ginc bs s = (bs', s', d) ->
    GPhi a 1 ((true, e) :: bs) s (RE2 a (addb e d) bs' s')
… +4 lines

Lemma ginc_s3 bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> s' <= 3.

Lemma GPhi_sound a b bs s r : GPhi a b bs s r -> s <= 3 -> Phi a b (gw bs s) (rk r) (ry r).

Lemma GPhi_s3 a b bs s r : GPhi a b bs s r -> s <= 3 ->
match r with RE2 _ _ _ s2 => s2 <= 3 | RSp _ y => y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) end.

Lemma GPhi_rk a b bs s r : GPhi a b bs s r -> a + b <= S (rk r).

Lemma gcount : forall P bs s a b, s <= 3 -> 1 <= b -> Psi bs s b <= P -> exists r, GPhi a b bs s r.

Inductive LPs : word -> word -> nat -> nat -> Prop :=
| LPs_eq w w' : enc w = enc w' -> LPs w w' 0 0
| LPs_step w w1 w2 d n c : LP w w1 d -> LPs w1 w2 n c -> LPs w w2 (S n) (c + b2n d).

Lemma LPs_step' w w1 w2 d n c c' : LP w w1 d -> LPs w1 w2 n c -> c' = c + b2n d -> LPs w w2 (S n) c'.

Lemma LPs_eql w0 w1 w2 n c : enc w0 = enc w1 -> LPs w1 w2 n c -> LPs w0 w2 n c.

Lemma LPs_trans w1 w2 w3 n c n' c' : LPs w1 w2 n c -> LPs w2 w3 n' c' -> LPs w1 w3 (n + n') (c + c').

Lemma LPs_cn w w' n c : LPs w w' n c -> c <= n.

Lemma LPs_hub w w' n c : LPs w w' n c -> forall a B k y, n + 2 <= B + c ->
Phi (a + n) (B + c - n) w' k y -> Phi a B w k y.

Lemma LPs_nest y y' n c : LPs y y' n c -> forall k, LPs (blk false k y) (blk false (k + c) y') (2 * n) 0.

Inductive DigE : word -> nat -> nat -> blks -> nat -> Prop :=
| DE0 : DigE (p10 t0) 0 0 [] 1
| DE1 : DigE (p10 t1) 0 0 [(true, 0)] 0
| DE2 : DigE (p10 t2) 13 5 [(false, 0)] 2
| DE3 : DigE (p10 t3) 7 2 [(false, 0)] 2
| DEs0 : DigE t1 0 0 [] 1
… +2 lines

Lemma DigE_sound y n c bs s : DigE y n c bs s -> LPs y (gw bs s) n c.

Lemma DigE_props y n c bs s : DigE y n c bs s ->
n <= 13 /\ c <= 5 /\ length bs <= 1 /\ s <= 3 /\ Forall (fun e => e = 0) (map snd bs).

Inductive DigP : nat -> blks -> nat -> nat -> nat -> blks -> nat -> Prop :=
| DP x bs s n c bsp sp : DigT bs s n c bsp sp -> DigP x bs s (2 * x + 2 + n) (S x + c) bsp sp
with DigT : blks -> nat -> nat -> nat -> blks -> nat -> Prop :=
| DTa e bs s bs' s' d n c bsp sp : ginc bs s = (bs', s', d) ->
    DigP (S (addb e d)) bs' s' n c bsp sp -> DigT ((false, e) :: bs) s (S (S n)) c bsp sp
| DTb e bs s k x bs2 s2 n c bsp sp : GPhi 1 (S e) bs s (RE2 k x bs2 s2) ->
… +4 lines

Lemma prefix_LPs x w : LPs (p11 x w) (p10 w) (2 * x + 2) (S x).

Lemma Dig_sound :
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> LPs (p11 x (gw bs s)) (gw bsp sp) n c) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> LPs (p10 (gw bs s)) (gw bsp sp) n c).

Lemma Dig_sp :
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> sp <= 3) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> sp <= 3).

Lemma epoch_ord N x bs s n c bsp sp r : s <= 3 -> DigP x bs s n c bsp sp -> n + 2 <= N ->
GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N (p11 x (gw bs s)) (rk r) (ry r).

Lemma epoch_spec N y n c bsp sp r : DigE y n c bsp sp -> n + 2 <= N ->
GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N y (rk r) (ry r).

Definition exs (bs : blks) : list nat := map snd bs.

Fixpoint bumpl (l : list nat) : list nat :=
match l with [] => [] | e :: l' => match l' with [] => [S e] | _ => e :: bumpl l' end end.

Lemma length_bumpl l : length (bumpl l) = length l.

Lemma length_exs bs : length (exs bs) = length bs.

Lemma ginc_exps bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) ->
(exs bs' = exs bs /\ d = false) \/
(exs bs' = bumpl (exs bs) ++ [0] /\ d = match bs with [] => true | _ => false end).

Fixpoint qsum (l : list nat) : nat := match l with [] => 0 | e :: l => S e + 2 * qsum l end.

Definition Qp (f : nat) (bs : blks) (s p : nat) : nat := 2 ^ f * (gval bs s + 2 * qsum (exs bs) + p).

Definition QI (Q0 f : nat) (bs : blks) (s p : nat) : Prop := Qp f bs s p <= Q0 + 3 * 2 ^ (f + length bs).

Lemma qsum_app0 l : qsum (l ++ [0]) = qsum l + 2 ^ length l.

Lemma qsum_bumpl l : l <> [] -> 2 * qsum (bumpl l) = 2 * qsum l + 2 ^ length l.

Lemma gval_lb bs s : 4 * 2 ^ length bs <= gval bs s.

Lemma gval_ub bs s : s <= 3 -> gval bs s < 8 * 2 ^ length bs.

Lemma QI_low Q0 f bs s p : QI Q0 f bs s p -> 2 ^ (f + length bs) <= Q0.

Lemma QI_Ps Q0 Ps f bs s p : QI Q0 f bs s p -> Q0 < 2 ^ (Ps + 1) -> f + length bs <= Ps.

Lemma QI_drop Q0 f bs s p : QI Q0 f bs s p -> QI Q0 f bs s 0.

Lemma QI_cons Q0 f dd e bs s p : QI Q0 f ((dd, e) :: bs) s 0 -> p <= S e -> QI Q0 (S f) bs s p.

Lemma QI_inc Q0 f bs s p bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) ->
QI Q0 f bs s (S p) -> QI Q0 f bs' s' (p + b2n d).

Lemma QI_et3 Q0 f : QI Q0 f [] 3 0 -> QI Q0 f [(false, 0)] 0 0.

Fixpoint wpot (v : nat -> nat) (al be f : nat) (l : list nat) : nat :=
match l with [] => 0 | e :: l => v f * (al * e + be) + wpot v al be (S f) l end.

Fixpoint vsum (v : nat -> nat) (f m : nat) : nat :=
match m with 0 => 0 | S m => v f + vsum v (S f) m end.

Definition Pot (v : nat -> nat) (al be ga Ps f : nat) (l : list nat) : nat :=
wpot v al be f l + ga * vsum v (f + length l) (Ps - (f + length l)).

Definition mono (v : nat -> nat) : Prop := forall i j, i <= j -> v i <= v j.

Lemma Pot_cons v al be ga Ps f e l :
Pot v al be ga Ps f (e :: l) = v f * (al * e + be) + Pot v al be ga Ps (S f) l.

Lemma wpot_app1 v al be f l x : wpot v al be f (l ++ [x]) = wpot v al be f l + v (f + length l) * (al * x + be).

Lemma wpot_bumpl v al be f l : mono v -> wpot v al be f (bumpl l) <= wpot v al be f l + al * v (f + length l).

Lemma Pot_ov v al be ga Ps f l : mono v -> al + be + 1 <= ga -> f + length l + 1 <= Ps ->
Pot v al be ga Ps f (bumpl l ++ [0]) + v (f + length l) <= Pot v al be ga Ps f l.

Lemma Pot_inc v al be ga Ps Q0 f bs s p bs' s' d : mono v -> al + be + 1 <= ga -> Q0 < 2 ^ (Ps + 1) -> s <= 3 ->
ginc bs s = (bs', s', d) -> QI Q0 f bs s (S p) ->
Pot v al be ga Ps f (exs bs') + b2n d * v f <= Pot v al be ga Ps f (exs bs).

Lemma GPhi_pot v al be ga Ps Q0 : mono v -> al + be + 1 <= ga -> 1 <= al -> 2 <= be -> Q0 < 2 ^ (Ps + 1) ->
forall a b bs s r, GPhi a b bs s r -> s <= 3 -> forall f U, QI Q0 f bs s (b - 1) ->
(forall q, f <= q -> U <= v q) ->
match r with
| RE2 k x bs2 s2 => exists h, QI Q0 (f + S h) bs2 s2 0 /\
    U * k + Pot v al be ga Ps (f + S h) (exs bs2) + v (f + h) * (al * x + be) <=
… +3 lines

Definition w (q : nat) : nat := 2 ^ ((q + 1) / 2).

Lemma w_mono : mono w.

Lemma w_lev l q : 2 * l <= q -> 2 ^ l <= w q.

Lemma w_lev1 l q : 2 * l + 1 <= q -> 2 ^ S l <= w q.

Lemma GPhi_QI Q0 Ps a b bs s k x bs2 s2 f : Q0 < 2 ^ (Ps + 1) -> GPhi a b bs s (RE2 k x bs2 s2) -> s <= 3 ->
QI Q0 f bs s (b - 1) -> exists h, QI Q0 (f + S h) bs2 s2 0.

Lemma Dig_cost Q0 Ps : Q0 < 2 ^ (Ps + 1) ->
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 2 ^ l * (2 * x + 2) + 13 * w Ps) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 13 * w Ps).

Fixpoint MO (u : nat -> nat) (l : nat) (es : list nat) : nat :=
match es with [] => 0 | e :: es => u l * e + MO u (S l) es end.

Definition pu (u : nat -> nat) (l : nat) : nat := match l with 0 => 0 | S l' => u l' end.

Lemma pu_le u l : mono u -> pu u l <= u l.

Lemma MO_zero u l es : Forall (fun e => e = 0) es -> MO u l es = 0.

Lemma Dig_mass u v Q0 Ps : mono v -> mono u -> (forall l q, 2 * l <= q -> u l <= v q) -> Q0 < 2 ^ (Ps + 1) ->
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + pu u l * S x + 6 * v Ps) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + 6 * v Ps).

Lemma Dig_len Q0 Ps : Q0 < 2 ^ (Ps + 1) ->
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 * (l + length bsp) <= Ps + 3) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 * (l + length bsp) <= Ps + 3).

Lemma pow_gt_self n : n < 2 ^ (n + 1).

Lemma DigE_ex y : y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) -> exists n c bsp sp, DigE y n c bsp sp.

Lemma DigT_exists Q0 : forall D f bs s, s <= 3 -> QI Q0 f bs s 0 -> Q0 + 1 - 2 ^ f <= D ->
exists n c bsp sp, DigT bs s n c bsp sp.

Definition Rel (orig cur : list nat) : Prop :=
(forall i, S i < length cur -> nth i cur 0 <= nth i orig 0 + 1) /\
(forall i, length cur <= S i -> nth i cur 0 <= nth i orig 0).

Lemma nth_bumpl l i : nth i (bumpl l) 0 = nth i l 0 + (if Nat.eqb (S i) (length l) then 1 else 0).

Lemma nth_app0 l i : nth i (l ++ [0]) 0 = nth i l 0.

Lemma Rel_ov orig l : Rel orig l -> Rel orig (bumpl l ++ [0]).

Lemma Rel_inc orig bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> Rel orig (exs bs) -> Rel orig (exs bs').

Lemma Rel_tl orig cur : Rel orig cur -> Rel (tl orig) (tl cur).

Lemma Rel_refl l : Rel l l.

Lemma GPhi_rel a b bs s r : GPhi a b bs s r -> s <= 3 -> forall orig, Rel orig (exs bs) ->
match r with
| RE2 k x bs2 s2 => exists h, Rel (skipn (S h) orig) (exs bs2) /\ x <= nth h orig 0 + 1
| RSp _ _ => True
end.

Lemma GPhi_val a b bs s r : GPhi a b bs s r -> s <= 3 ->
match r with RE2 k x bs2 s2 => 2 * gval bs2 s2 + a <= gval bs s + k + 2 | RSp _ _ => True end.

Definition v2 (q : nat) : nat := 2 ^ (q / 2).

Definition p2 (q : nat) : nat := 2 ^ S q.

Definition cst1 (q : nat) : nat := 1.

Definition u1 (l : nat) : nat := match l with 0 => 0 | S l' => 2 * w l' end.

Definition u2 (l : nat) : nat := match l with 0 => 0 | S l' => 2 ^ S l' end.

Lemma v2_mono : mono v2.

Lemma p2_mono : mono p2.

Lemma cst1_mono : mono cst1.

Lemma v2_le_w q : v2 q <= w q.

Lemma cst1_le_w q : cst1 q <= w q.

Lemma u1_mono : mono u1.

Lemma u1_w l q : 2 * l <= q -> u1 l <= w q.

Lemma u2_mono : mono u2.

Lemma u2_v2 l q : 2 * l <= q -> u2 l <= v2 q.

Lemma MO_u1 l es : MO u1 (S l) es = 2 * wpot w 1 0 l es.

Lemma MO_u1_0 es : MO u1 0 es = 2 * wpot w 1 0 0 (tl es).

Lemma MO_u2 l es : MO u2 (S l) es = wpot p2 1 0 l es.

Lemma MO_u2_0 es : MO u2 0 es = wpot p2 1 0 0 (tl es).

Lemma nth_le_MO h es : forall l, nth h es 0 <= MO cst1 l es.

Lemma wpot_shift v al be f f' l : mono v -> f <= f' -> wpot v al be f l <= wpot v al be f' l.

Lemma wpot_drop v al be f h l : wpot v al be (f + h) (skipn h l) <= wpot v al be f l.

Lemma wpot_skipn_tl v h l : mono v -> wpot v 1 0 0 (skipn (S h) l) <= wpot v 1 0 0 (tl l).

Lemma wpot_le_nth v l1 : mono v -> forall l2 f, (forall i, nth i l1 0 <= nth i l2 0 + 1) ->
wpot v 1 0 f l1 <= wpot v 1 0 f l2 + vsum v f (length l1).

Lemma Rel_nth orig cur : Rel orig cur -> forall i, nth i cur 0 <= nth i orig 0 + 1.

Lemma wpot_split v al be f l : wpot v al be f l = wpot v al 0 f l + be * vsum v f (length l).

Lemma wpot_scale2 v f l : wpot v 2 0 f l = 2 * wpot v 1 0 f l.

Lemma wpot_le_v v v' al be f l : (forall q, v q <= v' q) -> wpot v al be f l <= wpot v' al be f l.

Lemma vsum_add v f m m' : vsum v f (m + m') = vsum v f m + vsum v (f + m) m'.

Lemma vsum_mono_m v f m m' : m <= m' -> vsum v f m <= vsum v f m'.

Lemma vsum_cst1 f m : vsum cst1 f m = m.

Lemma vsum_p2 f m : vsum p2 f m + 2 ^ S f = 2 ^ S (f + m).

Lemma wpot_p2_S f l : wpot p2 1 0 (S f) l = 2 * wpot p2 1 0 f l.

Lemma qsum_p2 l : 2 * qsum l + 2 = 2 ^ S (length l) + wpot p2 1 0 0 l.

Lemma wpot_zero v f l : Forall (fun e => e = 0) l -> wpot v 1 0 f l = 0.

Lemma Pot_top v al be ga Ps l : be <= ga -> length l <= Ps ->
Pot v al be ga Ps 0 l <= wpot v al 0 0 l + ga * vsum v 0 Ps.

Definition Ws (P : nat) : nat := vsum w 0 P.

Definition V2s (P : nat) : nat := vsum v2 0 P.

Definition Pf (k : nat) : nat := Nat.max 12 (k + 3).

Definition Af (k : nat) : nat := 5 * Ws (Pf k) + 6 * w (Pf k) + 2 * Ws k.

Definition Bf (k : nat) : nat := Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) + 2 ^ (k + 1).

Definition Xf (k : nat) : nat := Af k + 5 * Pf k + 7.

Definition Costf (k : nat) : nat := 2 * Xf k + 2 + 2 * Af k + 11 * Ws (Pf k) + 13 * w (Pf k).

Definition Nlo (k : nat) : nat := 2 ^ (k + 3) - 8 * 2 ^ ((Pf k + 3) / 2).

Definition Nstar : nat := 17705.

Lemma Pf_mono k k' : k <= k' -> Pf k <= Pf k'.

Lemma Ws_mono P P' : P <= P' -> Ws P <= Ws P'.

Lemma V2s_mono P P' : P <= P' -> V2s P <= V2s P'.

Lemma Af_mono k k' : k <= k' -> Af k <= Af k'.

Lemma w_SS q : w (S (S q)) = 2 * w q.

Lemma v2_SS q : v2 (S (S q)) = 2 * v2 q.

Lemma vsum_SS_w f m : vsum w (S (S f)) m = 2 * vsum w f m.

Lemma vsum_SS_v2 f m : vsum v2 (S (S f)) m = 2 * vsum v2 f m.

Lemma Ws_SS P : Ws (S (S P)) = 2 * Ws P + 3.

Lemma V2s_SS P : V2s (S (S P)) = 2 * V2s P + 2.

Lemma Pf_big k : 9 <= k -> Pf k = k + 3.

Lemma Af_SS k : 9 <= k -> Af (S (S k)) = 2 * Af k + 21.

Definition gB (k : nat) : nat := Af k + 5 * V2s (k + 3) + 6 * v2 (k + 3).

Lemma gB_SS k : 9 <= k -> gB (S (S k)) = 2 * gB k + 31.

Lemma gB_all m : gB (10 + 2 * m) + 31 < 7 * 2 ^ (10 + 2 * m) /\ gB (11 + 2 * m) + 31 < 7 * 2 ^ (11 + 2 * m).

Lemma gB_ge k : 10 <= k -> gB k + 31 < 7 * 2 ^ k.

Lemma N1 k : 7 * 2 ^ k + Bf k < 2 ^ (Pf k + 1).

Lemma Costf_SS k : 9 <= k -> Costf (S (S k)) + 10 * (k + 3) = 2 * Costf k + 121.

Lemma Nlo_SS k : 9 <= k -> Nlo (S (S k)) = 4 * 2 ^ (k + 3) - 16 * 2 ^ ((k + 6) / 2) /\
Nlo k = 2 ^ (k + 3) - 8 * 2 ^ ((k + 6) / 2).

Lemma D_all m : Costf (12 + 2 * m) + 123 <= Nlo (12 + 2 * m) /\ Costf (13 + 2 * m) + 123 <= Nlo (13 + 2 * m).

Lemma N2 k : Costf k + 2 <= Nstar \/ Costf k + 2 <= Nlo k.

Lemma Nstar_ge : 15 <= Nstar.

Definition Mw (bs : blks) : nat := wpot w 1 0 0 (exs bs).

Definition M2 (bs : blks) : nat := wpot p2 1 0 0 (exs bs).

Definition Inv (k N : nat) (y : word) : Prop :=
Nstar <= N /\ Nlo k <= N /\
((exists x bs s, y = p11 x (gw bs s) /\ s <= 3 /\ length bs <= k /\
    Mw bs <= Af k /\ M2 bs <= Bf k /\ x <= Xf k)
 \/ y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2)).

Lemma next_inv k N n c bsp sp r :
GPhi (1 + n) (N + c - n) bsp sp r -> sp <= 3 -> n + 2 <= N -> Nstar <= N -> Nlo k <= N ->
MO u1 0 (exs bsp) <= Af k + 5 * Ws (Pf k) + 6 * w (Pf k) ->
MO u2 0 (exs bsp) <= Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) ->
MO cst1 0 (exs bsp) + 1 <= Xf k ->
2 * length bsp <= Pf k + 3 ->
… +1 lines

Lemma inv_step k N y : Inv k N y -> exists kk y', Phi 1 N y kk y' /\ exists k', Inv k' (S kk) y'.

Fixpoint orbit (f n N : nat) (y : word) : option (nat * word) :=
match n with
| O => Some (N, y)
| S n => match phif f 1 N y with Some (k, y') => orbit f n (S k) y' | None => None end
end.

Lemma orbit_sound f n : forall N y N' y', orbit f n N y = Some (N', y') -> K N y -->* K N' y'.