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

Definition k (n : N) : lf := LF n [].
Definition cfg28 : cfg :=
  Rc B
    ([(S0, k 74808); (S1, k 24912); (S0, k 8277); (S0, k 2737); (S0, k 972); (S1, k 36);
      (S0, k 37); (S0, k 37); (S0, k 44); (S1, k 24); (S0, k 13); (S0, k 9);
      (S0, k 4); (S1, k 4); (S0, k 1); (S0, k 5); (S0, k 4); (S1, k 4); (S0, k 1); (S0, k 5);
      (S0, k 4); (S1, k 4); (S0, k 1); (S0, k 5); (S0, k 1); (S0, k 6); (S1, k 4); (S0, k 1);
      (S0, k 5); (S0, k 1); (S0, k 5); (S0, k 1); (S0, k 5); (S0, k 1); (S0, k 5); (S0, k 2)], T0)
    ([(S1, k 224495); (S1, k 673559); (S1, k 7); (S1, k 9841); (S1, k 1942040); (S0, k 2)], T0).

Lemma init28 : c0 -->* ev_cfg [] (fun _ => const S0) cfg28.
Proof.
  assert (H : runp 18571896 (Rc A ([], T0) ([], T0)) = Some (cfg28, true)) by (native_compute; reflexivity).
  pose proof (runp_spec [] (fun _ => const S0) _ _ _ _ H) as R. cbn [Rel] in R.
  apply progress_evstep. exact R.
Qed.