-axiom terminate_UTM: ∀M:normalTM.∀t.
- M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
-
-
-
-
-
-
-
-
-lemma current_embedding: ∀c.
- high_c (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) = c.
- * normalize // qed.
-
-lemma tape_embedding: ∀ls,c,rs.
- high_tape
- (map ?? (λb.〈bit b,false〉) ls)
- (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉)
- (map ?? (λb.〈bit b,false〉) rs) = mk_tape ? ls c rs.
-#ls #c #rs >high_tape_eq >bool_embedding >bool_embedding
->current_embedding %
-qed.
-
-definition high_move ≝ λc,mv.
- match c with
- [ bit b ⇒ Some ? 〈b,move_of_unialpha mv〉
- | _ ⇒ None ?
- ].
-
-definition map_move ≝
- λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
-
-definition low_step_R_true ≝ λt1,t2.
- ∀M:normalTM.
- ∀c: nconfig (no_states M).
- t1 = low_config M c →
- halt ? M (cstate … c) = false ∧
- t2 = low_config M (step ? M c).
-
-definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝
-λM:normalTM.λt.
- let current_low ≝ match current … t with
- [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in
- let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in
- let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in
- mk_tape STape low_left current_low low_right.
-
-lemma left_of_low_tape: ∀M,t.
- left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t).
-#M * //
-qed.
-
-lemma right_of_low_tape: ∀M,t.
- right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t).
-#M * //
-qed.
-
-definition low_move ≝ λaction:option (bool × move).
- match action with
- [None ⇒ None ?
- |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)].
-
-(* simulation lemma *)
-lemma low_tape_move : ∀M,action,t.
- tape_move STape (low_tape_aux M t) (low_move action) =
- low_tape_aux M (tape_move FinBool t action).
-#M * // (* None *)
-* #b #mv #t cases mv cases t //
- [#ls #c #rs cases ls //|#ls #c #rs cases rs //]
-qed.
-
-lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls.
-#ls * #c #b #rs cases c // cases ls // cases rs //
-qed.
-
-lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs →
- right ? (lift_tape ls c rs) = rs.
-#ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr
-#H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct]
-qed.
-
-
-lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
- current STape (lift_tape ls 〈c,b〉 rs) =
- match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉].
-#ls #c #b #rs cases c // whd in ⊢ (%→?); * #_
-* [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //]
- |#Hrs >Hrs whd in ⊢ (??%%); cases ls //]
-qed.
-
-lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
- current STape (lift_tape ls 〈c,b〉 rs) = None ? →
- c = null.
-#ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
- [#b #H destruct |// |3,4,5:#H destruct ]
-qed.
-
-lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
- current STape (lift_tape ls c rs) = Some ? c1 →
- c = c1.
-#ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
- [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
-qed.
-
-lemma current_of_low_None: ∀M,t. current FinBool t = None ? →
- current STape (low_tape_aux M t) = None ?.
-#M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
-qed.
-
-lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b →
- current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
-#M #t cases t
- [#b whd in ⊢ ((??%?)→?); #H destruct
- |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
- |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
- |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
- ]
-qed.
-
-lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
- lift_tape ls c rs = low_tape_aux M tape →
- c = 〈match current … tape with
- [ None ⇒ null | Some b ⇒ bit b], false〉.
-#M #tape #ls * #c #cb #rs #Hlegal #Hlift
-cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
- [@eq_f @Hlift] -Hlift #Hlift
-cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
- [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *
- [#Hcurrent >Hcurrent normalize
- >(current_of_low_None …Hcurrent) in Hlift; #Hlift
- >(current_of_lift_None … Hlegal Hlift)
- @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
- |* #b #Hcurrent >Hcurrent normalize
- >(current_of_low_Some …Hcurrent) in Hlift; #Hlift
- @(current_of_lift_Some … Hlegal Hlift)
- ]
-qed.
-
-(*
-lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
- lift_tape ls c rs = low_tape_aux M tape →
- c = 〈match current … tape with
- [ None ⇒ null | Some b ⇒ bit b], false〉.
-#M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
- [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
- #b #_ #_ cases tape
- [whd in ⊢ ((??%%)→?); #H destruct
- |#a #l whd in ⊢ ((??%%)→?); #H destruct
- |#a #l whd in ⊢ ((??%%)→?); #H destruct
- |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
- ]
- |cases c
- [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
- |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
- #_ * [* [#Habs @False_ind /2/
- |#Hls >Hls whd in ⊢ ((??%%)→?); *)
-
-
-(* sufficent conditions to have a low_level_config *)
-lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
-legal_tape ls c rs →
-table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
-lift_tape ls c rs = low_tape_aux M tape →
-〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
-midtape STape (〈grid,false〉::ls)
- 〈qhd,false〉
- (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) =
- low_config M (mk_config ?? s tape).
-#ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
-#Hlift #Hstate whd in match (low_config ??); <Hstate
-@eq_f3
- [@eq_f <(left_of_lift ls c rs) >Hlift //
- | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
- [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
- @(Hcut …Hstate)
- |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
- <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape