/machines/1RB0RA_1RC0RD_1RD0LC_1LE1RA_---1LF_1RB0LC/rocq/try_T2000.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
From BusyCoq Require Import Individual62.
Require Import Lia.
Require Import ZArith.
Require Import String.
From BusyCoq Require Import Inductive.
From BusyCoq Require Import UnaryCounter.

Module Inductive62 := Inductive BB62.
Import Inductive62.

Lemma progress_rw tm c1 c2:
  progress tm c1 c2 <->
  Compute.TM.progress tm c1 c2.
Proof.
  split; intro H.
  - induction H.
    + constructor.
      destruct H; auto.
    + eapply Compute.TM.progress_step; eauto.
      destruct H; auto.
  - induction H.
    + constructor.
      destruct H; auto.
    + eapply progress_step; eauto.
      destruct H; auto.
Qed.

Ltac solve_hlin_nonhalt_T cfg T :=
  apply (decide_hlin_nonhalt_spec cfg T);
  [ unfold Config_WF; cbn;
    repeat rewrite List.Forall_cons_iff;
    repeat rewrite List.Forall_nil_iff;
    cbn;
    repeat split;
    intros;
    unfold s0;
    rewrite progress_rw;
    try (es; fail)
  | native_cast_no_check (eq_refl true)].

Ltac solve_hlin_nonhalt cfg :=
  match goal with
  | |- ~halts (TM_from_str ?x) c0 =>
    idtac x;
    (solve_hlin_nonhalt_T cfg 1000000%N)
  end.

Lemma nonhalt_T2000: ~halts (TM_from_str "1LB0LA_1LC0LD_1LD0RC_1RE1LA_---1RF_1LB0RC") c0.
Proof.
  solve_hlin_nonhalt
  (upd_config [
    add_ex_rules [side_3ary_Pos_inc_rule [0;0;0;0] [1;1;0;0] [0;1;0;0] [1;1] [0;1] [1;1;1;1] [1] [0] C C]
  ]
  (config_T_bsz 2000%N 3)).
Time Qed.