From BusyCoq Require Import Individual62.

Require Import ZArith Lia.
Require Import String.
Require Import List.
From BusyCoq Require Import ES_v3.

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

Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Definition G : list sym :=
  [0;0;1;1;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;0;1;1;0;1;1;1;1;1;0;0;1;1;0;1;1;1;1;1;0;1;1;0;0].

Definition Kr n a b c d :=
  0inf <{{F}} G *> [1] *> [1;1]^^n *> [0] *> [1;1]^^a *> [0;1;1;0] *> [1;1]^^b
    *> [0;0;0;0;0;0] *> [1] *> [1;1]^^c *> [0;1;1;0;1;1;1;1;0;0;0;0;0;0] *> [1;1]^^d
    *> [0;1;1;0;0;1;1;0;1;1;1] *> 0inf.

Fixpoint multistep_c' tm n1 n2 n3 c :=
match n1 with
| O => multistep_c tm n3 c
| S n1 =>
  match multistep_c tm n2 c with
  | Some c => multistep_c' tm n1 n2 n3 c
  | None => None
  end
end.

Lemma multistep_c'_spec tm n1 n2 n3 c c':
  multistep_c' tm n1 n2 n3 c = Some c' <-> c -[ tm ]->> (n1*n2+n3) / c'.
Proof.
  gen c c'.
  induction n1; cbn[multistep_c']; intros.
  1: apply multistep_c_spec.
  destruct (multistep_c tm n2 c) eqn:E.
  + apply multistep_c_spec in E.
    rewrite IHn1.
    replace (S n1*n2+n3) with (n2+(n1*n2+n3)) by lia.
    split; intro H.
    * eapply multistep_trans; eauto 1.
    * eapply rewind_split in H.
      destruct H as [c'0 [I1 I2]].
      multistep_deterministic.
      eauto 1.
  + split.
    1: congruence.
    replace (S n1*n2+n3) with (n2+(n1*n2+n3)) by lia.
    intro H.
    eapply rewind_split in H.
    destruct H as [c'0 [I1 I2]].
    eapply multistep_c_spec in I1.
    congruence.
Qed.

Lemma init:
  c0 -->* Kr 979 17 34 22 9.
Proof.
  eapply without_counter with (n:=4097*1000+897).
  eapply multistep_c'_spec.
  native_check_eq.
Time Qed.