/machines/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF/rocq/c_S.v · raw
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
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.

Ltac ES_v3.es_v3_pre ::= unfold Kr, G.

Lemma S_step n a b c d:
  Kr n (5+a) (3+b) (3+c) (1+d) -->+ Kr (24+n) (1+a) (5+b) (3+c) (3+d).
Proof.
  es' n a b c d.
Qed.