(* ---------- #11's orientation-free list definitions, verbatim ---------- *)
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.

(* ---------- the list sweeps (mirrors of #11's LbS, RbS, RoS) ---------- *)
(* left-side accumulator: what Lb leaves behind for each all-ones digit (u+1,1,v+1) *)
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.
Proof. induction xs; cbn; congruence. Qed.

Lemma LbS os: forall l r, l {{E}}> app_ds r (map1 os) -->* rw os l {{E}}> r.
Proof.
  induction os as [|[u v] t IH]; intros.
  - finish.
  - cbn [map1 map app_ds dr rw]. follow Lb. apply IH.
Qed.

Lemma RbS os: forall l r, rw os l <* [1;1] <{{D}} r -->* l <* [1;1] <{{D}} app_ds r (map0 os).
Proof.
  induction os as [|[u v] t IH]; intros.
  - finish.
  - cbn [map0 map app_ds dr rw]. follow IH. apply Rb.
Qed.

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.

Lemma RoS os: forall l r, rw os l <{{C}} [0;0;0] *> r -->* l <{{C}} [0;0;0] *> ro_out os r.
Proof.
  induction os as [|[u v] t IH]; intros.
  - finish.
  - cbn [ro_out rw]. follow IH. apply Ro.
Qed.

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).
Proof.
  induction t as [|[a b] t IH]; intros.
  - reflexivity.
  - cbn [ro_out Oz app_ds dr]. rewrite <- IH. reflexivity.
Qed.

(* ---------- edge chunks (mirrors of #11's chunkA, chunkC, chunkO) ---------- *)
(* left-edge chunk shared by M and O: <C (01)^b 000 (01)^a -> (10)^(b+2) 110 (10)^a E> *)
Lemma chunkA a b r:
  0inf <{{C}} [0;1]^^b *> [0;0;0] *> [0;1]^^a *> r -->+
  0inf <* [0;1]^^(S (S b)) <* [0;1;1] <* [0;1]^^a {{E}}> r.
Proof. es. Qed.

(* end of M: (10)^(b+2) 110 (10)^a 11 <D -> <C (01)^(b+2) 000 (01)^(a+1) *)
Lemma chunkC a b r:
  0inf <* [0;1]^^(S (S b)) <* [0;1;1] <* [0;1]^^a <* [1;1] <{{D}} r -->*
  0inf <{{C}} [0;1]^^(S (S b)) *> [0;0;0] *> [0;1]^^(S a) *> r.
Proof.
  follow S5. follow T8. follow S1. fin.
Qed.

(* end of O: (10)^(b+2) 110 (10)^(a+1) <C 000 -> <C 01 000 (01)^(b+3) (10)^(a+1) 01 *)
Lemma chunkO a b r:
  0inf <* [0;1]^^(S (S b)) <* [0;1;1] <* [0;1]^^(S a) <{{C}} [0;0;0] *> r -->*
  0inf <{{C}} [0;1] *> [0;0;0] *> [0;1]^^(S (S (S b))) *> [1;0]^^(S a) *> [0;1] *> r.
Proof.
  follow S1. follow T11. follow S5. follow T12. follow S4. follow T13. follow S4. follow T2. follow S1. follow S1_1.
  rewrite (rot01 (S (S b))).
  follow (S6 (0inf <* [1;1;0;1]) ([1] *> [0;1]^^a *> [0;0;1] *> r) (S (S (S b)))).
  follow T14. fin.
Qed.

(* ---------- the three rules, statements verbatim from #11 ---------- *)
(* M: carry *)
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)).
Proof.
  unfold K. rewrite !app_ds_app.
  follow10 chunkA.
  follow LbS.
  cbn [app_ds dr].
  follow Lf.
  follow RbS.
  apply chunkC.
Qed.

(* M with the flipped digit dropping: (u+1,1,0) fuses into the digit below it *)
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)).
Proof.
  follow10 (M_spec (os ++ [(u2,v2)]) u 0 rest a b).
  assert (E: app_ds R0 (map0 (os ++ [(u2,v2)]) ++ d1 (S u) 0 :: rest) =
             app_ds R0 (map0 os ++ d0 (S u2 + S u) v2 :: rest)).
  { unfold map0. rewrite map_app, <- app_assoc. cbn [map app].
    rewrite !app_ds_app. f_equal. cbn [app_ds dr].
    rewrite (lpow_add _ (S u2) (S u)), Str_app_assoc. reflexivity. }
  unfold K. rewrite E. finish.
Qed.

(* O: overflow *)
Lemma O_spec os a b: os <> [] ->
  K (map1 os) (S a) b -->+ K (Oout os (S a)) (S (S (S b))) 1.
Proof.
  intro H. destruct os as [|[u v] t]; [congruence|].
  unfold K.
  follow10 chunkA.
  follow LbS.
  unfold R0. follow T9.
  follow RoS.
  follow chunkO.
  apply evstep_refl'. cbn [Oout app_ds dr ro_out]. rewrite <- Ozeq. reflexivity.
Qed.