/machines/1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---/rocq/conj_test.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
From BusyCoq Require Import Individual62.
Require Import Arith Lia List.
Require Import String.
Import ListNotations.

Definition tm := Eval compute in (TM_from_str "1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---").
Definition tm3 := Eval compute in (TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---").

Definition phi (q : Q) : Q :=
  match q with A => D | B => A | C => B | D => C | E => E | F => F end.

Lemma perm_twin : Perm (flip tm) tm3 phi.
Proof.
  split.
  - intros [] [] H; cbn in *; try discriminate; reflexivity.
  - intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
Qed.

Lemma twin_of_parent : ~ halts tm3 (D;; tape0) -> ~ halts tm c0.
Proof.
  intros H3 H. apply flip_halts in H.
  change (halts (flip tm) (A;; tape0)) in H.
  exact (H3 (perm_halts _ _ _ _ _ perm_twin H)).
Qed.

Print Assumptions twin_of_parent.