-lemma step_seq_liftR : ∀sig,M1,M2,c0.
- halt ? M2 (cstate ?? c0) = false →
- step sig (seq sig M1 M2) (lift_confR sig (states ? M1) (states ? M2) c0) =
- lift_confR sig (states ? M1) (states ? M2) (step sig M2 c0).
-#sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
- lapply (refl ? (trans ?? 〈s,current sig t〉))
- cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %);
- #s0 #m0 cases t
- [ #Heq #Hhalt
- | 2,3: #s1 #l1 #Heq #Hhalt
- |#ls #s1 #rs #Heq #Hhalt ]
- whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%);
- whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftR … Heq) //
-qed.
-
-lemma step_seq_liftL : ∀sig,M1,M2,c0.
- halt ? M1 (cstate ?? c0) = false →
- step sig (seq sig M1 M2) (lift_confL sig (states ? M1) (states ? M2) c0) =
- lift_confL sig ?? (step sig M1 c0).
-#sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
- lapply (refl ? (trans ?? 〈s,current sig t〉))
- cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %);
- #s0 #m0 cases t
- [ #Heq #Hhalt
- | 2,3: #s1 #l1 #Heq #Hhalt
- |#ls #s1 #rs #Heq #Hhalt ]
- whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%);
- whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftL … Heq) //
-qed.
-
-lemma trans_liftL_true : ∀sig,M1,M2,s,a.
- halt ? M1 s = true →
- trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
-#sig #M1 #M2 #s #a #Hhalt whd in ⊢ (??%?); >Hhalt %
-qed.
-
-lemma eq_ctape_lift_conf_L : ∀sig,S1,S2,outc.
- ctape sig (FinSum S1 S2) (lift_confL … outc) = ctape … outc.
-#sig #S1 #S2 #outc cases outc #s #t %
+lemma step_seq_liftR : ∀sig,n,M1,M2,c0.
+ halt ?? M2 (cstate ??? c0) = false →
+ step sig n (seq sig n M1 M2) (lift_confR sig n (states ?? M1) (states ?? M2) c0) =
+ lift_confR sig n (states ?? M1) (states ?? M2) (step sig n M2 c0).
+#sig #n #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
+lapply (refl ? (trans ??? 〈s,current_chars sig n t〉))
+cases (trans ??? 〈s,current_chars sig n t〉) in ⊢ (???% → %);
+#s0 #m0 #Heq #Hhalt whd in ⊢ (???(?????%)); >Heq whd in ⊢ (???%);
+whd in ⊢ (??(????%)?); whd in ⊢ (??%?); >(trans_seq_liftR … Heq) //
+qed.
+
+lemma step_seq_liftL : ∀sig,n,M1,M2,c0.
+ halt ?? M1 (cstate ??? c0) = false →
+ step sig n (seq sig n M1 M2) (lift_confL sig n (states ?? M1) (states ?? M2) c0) =
+ lift_confL sig n ?? (step sig n M1 c0).
+#sig #n #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
+ lapply (refl ? (trans ??? 〈s,current_chars sig n t〉))
+ cases (trans ??? 〈s,current_chars sig n t〉) in ⊢ (???% → %);
+ #s0 #m0 #Heq #Hhalt
+ whd in ⊢ (???(?????%)); >Heq whd in ⊢ (???%);
+ whd in ⊢ (??(????%)?); whd in ⊢ (??%?); >(trans_seq_liftL … Heq) //
+qed.
+
+lemma trans_liftL_true : ∀sig,n,M1,M2,s,a.
+ halt ?? M1 s = true →
+ trans sig n (seq sig n M1 M2) 〈inl … s,a〉 = 〈inr … (start ?? M2),null_action sig n〉.
+#sig #n #M1 #M2 #s #a #Hhalt whd in ⊢ (??%?); >Hhalt %
+qed.
+
+lemma eq_ctape_lift_conf_L : ∀sig,n,S1,S2,outc.
+ ctapes sig (FinSum S1 S2) n (lift_confL … outc) = ctapes … outc.
+#sig #n #S1 #S2 #outc cases outc #s #t %