/machines/1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---/rocq/Low.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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
From BusyCoq Require Import Individual62.
Require Import Lia.
Require Import String.
Require Import List.

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

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

Open Scope list.

Lemma S0 l : l <* <[1;0;0] {{D}}> 0inf -->+ l <* <[1;0;0] <{{B}} [1;0;1;0] *> 0inf.
Proof. es. Qed.

Lemma L1 l r : l <* <[1;0;0] <{{B}} r -->+ l <{{B}} [1;0;0] *> r.
Proof. es. Qed.

Lemma L2 l j r : l <* <[1;0;0;0;0] <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  l <{{B}} [1;0;1;0;1;0;1;0]^^(S j) *> r.
Proof. es. Qed.

Lemma L3 l r : l <* <[1;1;0;0;1;1;0;0] <{{B}} r -->+ l <* <[1;1;0;0;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

Lemma L4 l r : l <* <[1;0;0;1;1;0;0] <{{B}} r -->+ l <* <[1;0;0;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

Lemma L5 l j i r : l <* <[1;1;0;0;0;0] <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> [1;0;1;0;1;0;1;0]^^i *> [1;0;0] *> r -->+
  l <* <[1;0;0;1;1;0;0] <* <[1;1;0;0;1;1;0;0]^^(i+j) <* <[1;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

Lemma L5e l j i : l <* <[1;1;0;0;0;0] <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> [1;0;1;0;1;0;1;0]^^i *> [1;0;1;0] *> 0inf -->+
  l <* <[1;0;0;1;1;0;0] <* <[1;1;0;0;1;1;0;0]^^(i+j) <* <[1;0;0] <* <[1;0;0] {{D}}> 0inf.
Proof. es. Qed.

Lemma L6 r : 0inf <* <[1;1;0;0] <{{B}} r -->+ 0inf <* <[1;0] {{A}}> r.
Proof. es. Qed.

Lemma L7 j r : 0inf <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  0inf <* <[1;1;0;0] <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1] {{E}}> r.
Proof. es. Qed.

Lemma RA1 l j r : l <* <[1;0] {{A}}> [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  l <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

Lemma RA3 l j : l <* <[1;0] {{A}}> [1;0;1;0;1;0;1;0]^^j *> [1;0;1;0] *> 0inf -->+
  l <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1;0;0] {{D}}> 0inf.
Proof. es. Qed.

Lemma RE1 l j r : l <* <[1;0;0] <* <[1] {{E}}> [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  l <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1;0;0] <* <[1] {{E}}> r.
Proof. es. Qed.

Lemma RE2 l : l <* <[1;0;0] <* <[1;0;0] <* <[1] {{E}}> [1;0;1;0] *> 0inf -->+
  l <* <[1;0;0;0;0] <* <[1;0;0] <* <[1;0;0] <* <[1;0;0] {{D}}> 0inf.
Proof. es. Qed.