/machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/rocq/t1.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
28
29
30
31
32
33
34
35
36
37
38
From BusyCoq Require Import Individual62.
Require Import ZifyNat Lia.
Require Import ZArith.
Require Import String.

Open Scope list.

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

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

Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0.

Lemma RS l n m:
  l {{B}}> R (S n) m -->+ l <{{A}} R n (S m).
Proof.
  unfold R. es.
Qed.

Lemma OVe l u m:
  ([0;0]^^u *> [1] *> l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0.
Proof.
  unfold R. es.
Qed.

Lemma OVo l u m:
  ([0;0]^^u *> [0;1;0;0] *> l) {{B}}> R 0 m -->+ l <{{A}} R 0 (m+u+2).
Proof.
  unfold R. es.
  execute.
  Show.
Admitted.

Lemma init0: c0 -->* (const 0) <* [1] <{{A}} R 0 1.
Proof.
  unfold R. esx.
Qed.