-include "turing/while_machine.ma".
-
-definition mcc_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
-
-definition mcc0 : initN 5 ≝ mk_Sig ?? 0 (leb_true_to_le 1 5 (refl …)).
-definition mcc1 : initN 5 ≝ mk_Sig ?? 1 (leb_true_to_le 2 5 (refl …)).
-definition mcc2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)).
-definition mcc3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)).
-definition mcc4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)).
-
-definition mcc_step ≝
- λalpha:FinSet.λsep:alpha.
- mk_TM alpha (mcc_states alpha)
- (λp.let 〈q,a〉 ≝ p in
- let 〈q',b〉 ≝ q in
- let q' ≝ pi1 nat (λi.i<5) q' in (* perche' devo passare il predicato ??? *)
- match a with
- [ None ⇒ 〈〈mcc4,sep〉,None ?〉
- | Some a' ⇒
- match q' with
- [ O ⇒ (* qinit *)
- match a' == sep with
- [ true ⇒ 〈〈mcc4,sep〉,None ?〉
- | false ⇒ 〈〈mcc1,a'〉,Some ? 〈a',L〉〉 ]
- | S q' ⇒ match q' with
- [ O ⇒ (* q1 *)
- 〈〈mcc2,a'〉,Some ? 〈b,R〉〉
- | S q' ⇒ match q' with
- [ O ⇒ (* q2 *)
- 〈〈mcc3,sep〉,Some ? 〈b,R〉〉
- | S q' ⇒ match q' with
- [ O ⇒ (* qacc *)
- 〈〈mcc3,sep〉,None ?〉
- | S q' ⇒ (* qfail *)
- 〈〈mcc4,sep〉,None ?〉 ] ] ] ] ])
- 〈mcc0,sep〉
- (λq.let 〈q',a〉 ≝ q in q' == mcc3 ∨ q' == mcc4).
-
-lemma mcc_q0_q1 :
- ∀alpha:FinSet.∀sep,a,ls,a0,rs.
- a0 == sep = false →
- step alpha (mcc_step alpha sep)
- (mk_config ?? 〈mcc0,a〉 (mk_tape … ls (Some ? a0) rs)) =
- mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc1,a0〉
- (tape_move_left alpha ls a0 rs).
-#alpha #sep #a *
-[ #a0 #rs #Ha0 whd in ⊢ (??%?);
- normalize in match (trans ???); >Ha0 %
-| #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
- normalize in match (trans ???); >Ha0 %
-]
-qed.
-
-lemma mcc_q1_q2 :
- ∀alpha:FinSet.∀sep,a,ls,a0,rs.
- step alpha (mcc_step alpha sep)
- (mk_config ?? 〈mcc1,a〉 (mk_tape … ls (Some ? a0) rs)) =
- mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc2,a0〉
- (tape_move_right alpha ls a rs).
-#alpha #sep #a #ls #a0 * //
-qed.