/machines/1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA/LocalRules.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
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
(** Local rules for 1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA.
    These statements concern explicitly given configurations. They do not
    establish the behavior from the blank initial configuration.
    AI assistance: GPT-6 Astra (OpenAI). *)

From BusyCoq Require Import Individual62.
Require Import Lia String List.
Open Scope list.

Definition tm := Eval compute in
  (TM_from_str "1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA").
Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

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

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

Lemma C_1 l r : l {{C}}> [1] *> r -->+ l <* [1] {{C}}> r.
Proof. es. Qed.

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

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

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

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

Lemma F_blank_progress r :
  0inf <{{F}} r -->+ 0inf <{{F}} [1] *> r.
Proof. es. Qed.

Lemma F_blank_nonhalt r : ~halts tm (0inf <{{F}} r).
Proof.
  apply (progress_nonhalt_simple tm side (fun r => 0inf <{{F}} r) r).
  intros x. exists ([1] *> x). apply F_blank_progress.
Qed.

Lemma D_zero_prefix_escape r :
  0inf {{D}}> [1;0] *> r -->+ 0inf <{{F}} [1;1] *> r.
Proof. es. Qed.

Lemma D_zero_prefix_nonhalt r : ~halts tm (0inf {{D}}> [1;0] *> r).
Proof.
  eapply multistep_nonhalt.
  - apply progress_evstep, D_zero_prefix_escape.
  - apply F_blank_nonhalt.
Qed.

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

Lemma A_zero_prefix_halt r : halts tm (0inf {{A}}> [1] *> r).
Proof.
  eapply halts_evstep with (c' := 0inf <{{E}} [1;0] *> r).
  - apply halted_halts. reflexivity.
  - es.
Qed.

Lemma A_zero_run l r n :
  l <* [1] <* [0]^^n <* <[1;1] <{{A}} r -->+
  l <{{A}} [0] *> [1]^^(n+2) *> r.
Proof. es. Qed.

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

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

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

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

Definition Qblk : list sym := [1;0;1;1;1;1;1;1;1;0;1;1;1;1;1;1;1;0;1;1;1;0;1;1;1;0;1;1;0;1;1;0;1;1;1;0;1;1;1;1;0;1;1;1;1;1;0;1;1;1;1].
Definition Pblk : list sym := [1;1;0;0;1;1;0;1;1;1;1;0;1;1;0;0;1;1;1;1;1;0;0;1;1;1;1;0;1;1;0;1;1;1;1;1;0;1;1;1;0;1;1;0;1;1;1;1;1;1;1].
Definition Rblk : list sym := [1;0;1;1;0;1;1;0;1;1;1;0;1;1;1;1;0;1;1;1;1;1;0;1;1;1;1;1;0;1;1;1;1;1;1;1;0;1;1;1;1;1;1;1;0;1;1;1;0;1;1].
Definition Wguard : list sym := [0;1;1;1;1;1;1;1;1;1;1;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1;1;1;0;1;1;1;1;1;1;1;0;1;1;1;1;1;1;1;1;1;0;1;1;0;1;1;1;1;1;0;1;1;1;0;1;1;0;1;1;1;1;1;1;1].
Definition Gguard : list sym := [1;0;1;1;1;1;1;1;1;0;1;1;1;1;1;1;1;0;1;1;1;0;1;1].
Definition Ttail : list sym := [1;1;0;1;1;0;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1;0;0;1;1;1;1;0;1;1;0;1;1;1;1;1;0;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1;1;0;1;1;0;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1;0;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1].

Lemma bulk_left_one l r :
  l <* (rev Qblk) <{{A}} r -->+ l <{{A}} Pblk *> r.
Proof. unfold Qblk, Pblk. es. Qed.

Lemma bulk_right_one l r :
  l <* (rev Wguard) {{C}}> Pblk *> r -->+
  l <* (rev Rblk) <* (rev Wguard) {{C}}> r.
Proof. unfold Wguard, Pblk, Rblk. es. Qed.

Lemma right_reflection l r :
  l <* (rev Gguard) <* (rev Wguard) {{C}}> Ttail *> [0;0;0;0;0;0;0;0] *> r -->+
  l <{{A}} Pblk *> Pblk *> Ttail *> r.
Proof. unfold Gguard, Wguard, Ttail, Pblk. es. Qed.

Print Assumptions A_zero_run.
Print Assumptions prefix_E.
Print Assumptions prefix_F.
Print Assumptions prefix_A_positive.
Print Assumptions easy_even_return.
Print Assumptions bulk_left_one.
Print Assumptions bulk_right_one.
Print Assumptions right_reflection.
Print Assumptions F_blank_nonhalt.
Print Assumptions D_zero_prefix_nonhalt.
Print Assumptions A_zero_prefix_halt.