-]
-qed.
-
-lemma binaryTM_phase2_None_R :∀sig,M,q,ch,qn,ls,rs,k,csr.
- 〈qn,None ?,R〉 = trans sig M 〈q,ch〉 →
- ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
- |csl@cur::csr| = FS_crd sig →
- loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
- (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
- = loopM ? (mk_binaryTM sig M) k
- (mk_config ?? (〈qn,bin3,ch,O〉)
- (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs))). [2,3://]
-#sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
-[ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
- >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
- >loop_S_false // @eq_f >(binaryTM_bin2_O_R … Htrans)
- @eq_f cases rs //
-| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
- >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
- change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs))
- in match (tape_move ???); >reverse_cons >associative_append
- normalize in match ([b0]@cur::csl@ls); @IH
- <Hcrd >length_append >length_append normalize //
-]
-qed.
-
-lemma binaryTM_phase2_None_L : ∀sig,M,q,ch,qn,ls,rs,k,csr.
- 〈qn,None ?,L〉 = trans sig M 〈q,ch〉 →
- ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
- |csl@cur::csr| = FS_crd sig →
- loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
- (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
- = loopM ? (mk_binaryTM sig M) k
- (mk_config ?? (〈qn,bin3,ch,to_initN (2*FS_crd sig) ??〉)
- (tape_move ? (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
-#sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
-[ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
- >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
- >loop_S_false // @eq_f >(binaryTM_bin2_O_L … Htrans)
- @eq_f cases rs //
-| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
- >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
- change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs))
- in match (tape_move ???); >reverse_cons >associative_append
- normalize in match ([b0]@cur::csl@ls); @IH
- <Hcrd >length_append >length_append normalize //
-]
-qed.
-
-lemma binaryTM_phase2_None_N :∀sig,M,q,ch,qn,ls,rs,k,csr.
- 〈qn,None ?,N〉 = trans sig M 〈q,ch〉 →
- ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
- |csl@cur::csr| = FS_crd sig →
- loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
- (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
- = loopM ? (mk_binaryTM sig M) k
- (mk_config ?? (〈qn,bin3,ch,to_initN (FS_crd sig) ??〉)
- (tape_move ? (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
-#sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
-[ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
- >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
- >loop_S_false // @eq_f >(binaryTM_bin2_O_N … Htrans)
- @eq_f cases rs //
-| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
- >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
- change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs))
- in match (tape_move ???); >reverse_cons >associative_append
- normalize in match ([b0]@cur::csl@ls); @IH
- <Hcrd >length_append >length_append normalize //
-]