/machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/rocq/dev_reach.v · raw
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
Require Import ssim.
From BusyCoq Require Import Individual62.
Require Import List NArith.
Import ListNotations.

Definition v (i : nat) (c : N) : lf := LF c (List.repeat 0%N i ++ [4%N]).
(* block U0 (m = 3), entered from the right at its phase c: U0 -> U1, leaves right at c + 2 *)
Definition U0c := Lc D ([(S0, LF 3 []); (S0, v 0 4); (S1, v 1 4); (S0, v 2 1); (S0, v 3 2)], TV 0) ([], TV 1).
Definition U1o := Rc A ([(S0, LF 3 []); (S0, v 0 4); (S1, v 1 4); (S0, v 2 2); (S1, v 3 1)], TV 0) ([], TV 1).
Lemma blk_U0 : forall nu sg, ev_cfg nu sg U0c -->+ ev_cfg nu sg U1o.
Proof. apply (reach_spec 100). vm_compute. reflexivity. Qed.

(* the TM-level reading: for all gaps and sides *)
Lemma blk_U0_tm (t s a lp : N) (L R : side) :
  ev_cfg [t; s; a; lp] (fun k => match k with O => L | _ => R end) U0c -->+
  ev_cfg [t; s; a; lp] (fun k => match k with O => L | _ => R end) U1o.
Proof. apply blk_U0. Qed.
Print Assumptions blk_U0_tm.