+(****************************** lifting lemmas ********************************)
+lemma trans_if_liftM1 : ∀sig,M1,M2,M3,acc,s,a,news,move.
+ halt ? M1 s = false →
+ trans sig M1 〈s,a〉 = 〈news,move〉 →
+ trans sig (ifTM sig M1 M2 M3 acc) 〈inl … s,a〉 = 〈inl … news,move〉.
+#sig * #Q1 #T1 #init1 #halt1 #M2 #M3 #acc #s #a #news #move
+#Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
+qed.
+
+lemma trans_if_liftM2 : ∀sig,M1,M2,M3,acc,s,a,news,move.
+ halt ? M2 s = false →
+ trans sig M2 〈s,a〉 = 〈news,move〉 →
+ trans sig (ifTM sig M1 M2 M3 acc) 〈inr … (inl … s),a〉 = 〈inr… (inl … news),move〉.
+#sig #M1 * #Q2 #T2 #init2 #halt2 #M3 #acc #s #a #news #move
+#Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
+qed.
+
+lemma trans_if_liftM3 : ∀sig,M1,M2,M3,acc,s,a,news,move.
+ halt ? M3 s = false →
+ trans sig M3 〈s,a〉 = 〈news,move〉 →
+ trans sig (ifTM sig M1 M2 M3 acc) 〈inr … (inr … s),a〉 = 〈inr… (inr … news),move〉.
+#sig #M1 * #Q2 #T2 #init2 #halt2 #M3 #acc #s #a #news #move
+#Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
+qed.
+
+lemma step_if_liftM1 : ∀sig,M1,M2,M3,acc,c0.
+ halt ? M1 (cstate ?? c0) = false →
+ step sig (ifTM sig M1 M2 M3 acc) (lift_confL sig (states ? M1) ? c0) =
+ lift_confL sig (states ? M1) ? (step sig M1 c0).
+#sig #M1 #M2 #M3 #acc * #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_if_liftM1 … Hhalt Heq) //
+qed.
+
+lemma step_if_liftM2 : ∀sig,M1,M2,M3,acc,c0.
+ halt ? M2 (cstate ?? c0) = false →
+ step sig (ifTM sig M1 M2 M3 acc) (lift_confR sig ?? (lift_confL sig ?? c0)) =
+ lift_confR sig ?? (lift_confL sig ?? (step sig M2 c0)).
+#sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 #M3 #acc * #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 match (step ? M2 ?); >Heq whd in ⊢ (???%);
+ whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_if_liftM2 … Hhalt Heq) //
+qed.
+
+lemma step_if_liftM3 : ∀sig,M1,M2,M3,acc,c0.
+ halt ? M3 (cstate ?? c0) = false →
+ step sig (ifTM sig M1 M2 M3 acc) (lift_confR sig ?? (lift_confR sig ?? c0)) =
+ lift_confR sig ?? (lift_confR sig ?? (step sig M3 c0)).
+#sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 #M3 #acc * #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 match (step ? M3 ?); >Heq whd in ⊢ (???%);
+ whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_if_liftM3 … Hhalt Heq) //
+qed.
+
+lemma trans_if_M1true_acc : ∀sig,M1,M2,M3,acc,s,a.
+ halt ? M1 s = true → s==acc = true →
+ trans sig (ifTM sig M1 M2 M3 acc) 〈inl … s,a〉 = 〈inr … (inl … (start ? M2)),None ?〉.
+#sig #M1 #M2 #M3 #acc #s #a #Hhalt #Hacc whd in ⊢ (??%?); >Hhalt >Hacc %
+qed.
+
+lemma trans_if_M1true_notacc : ∀sig,M1,M2,M3,acc,s,a.
+ halt ? M1 s = true → s==acc = false →
+ trans sig (ifTM sig M1 M2 M3 acc) 〈inl … s,a〉 = 〈inr … (inr … (start ? M3)),None ?〉.
+#sig #M1 #M2 #M3 #acc #s #a #Hhalt #Hacc whd in ⊢ (??%?); >Hhalt >Hacc %
+qed.
+
+(******************************** semantics ***********************************)
+lemma sem_if: ∀sig.∀M1,M2,M3:TM sig.∀Rtrue,Rfalse,R2,R3,acc.
+ M1 ⊨ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 →
+ ifTM sig M1 M2 M3 acc ⊨ (Rtrue ∘ R2) ∪ (Rfalse ∘ R3).
+#sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
+cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
+cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
+ [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
+ @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2))) %
+ [@(loop_merge ?????????
+ (mk_config ? (FinSum (states sig M1) (FinSum (states sig M2) (states sig M3)))
+ (inr (states sig M1) ? (inl (states sig M2) (states sig M3) (start sig M2))) (ctape ?? outc1) )
+ ?
+ (loop_lift ???
+ (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
+ (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
+ (λc.halt sig M1 (cstate … c))
+ (λc.halt_liftL ?? (halt sig M1) (cstate … c))
+ … Hloop1))
+ [* *
+ [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+ | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+ |#c0 #Hhalt >(step_if_liftM1 … Hhalt) //
+ |#x <p_halt_liftL %
+ |whd in ⊢ (??%?); >(config_expand ?? outc1);
+ whd in match (lift_confL ????);
+ >(trans_if_M1true_acc … Hacc)
+ [% | @(loop_Some ?????? Hloop1)]
+ |cases outc1 #s1 #t1 %
+ |@(loop_lift ???
+ (λc.(lift_confR … (lift_confL sig (states ? M2) (states ? M3) c)))
+ … Hloop2)
+ [ * #s2 #t2 %
+ | #c0 #Hhalt >(step_if_liftM2 … Hhalt) // ]
+ ]
+ |%1 @(ex_intro … (ctape ?? outc1)) %
+ [@HMtrue @(\P Hacc) | >(config_expand ?? outc2) @HM2 ]
+ ]
+ |cases (HR3 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM3
+ @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confR … outc2))) %
+ [@(loop_merge ?????????
+ (mk_config ? (FinSum (states sig M1) (FinSum (states sig M2) (states sig M3)))
+ (inr (states sig M1) ? (inr (states sig M2) (states sig M3) (start sig M3))) (ctape ?? outc1) )
+ ?
+ (loop_lift ???
+ (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
+ (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
+ (λc.halt sig M1 (cstate … c))
+ (λc.halt_liftL ?? (halt sig M1) (cstate … c))
+ … Hloop1))
+ [* *
+ [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+ | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+ |#c0 #Hhalt >(step_if_liftM1 … Hhalt) //
+ |#x <p_halt_liftL %
+ |whd in ⊢ (??%?); >(config_expand ?? outc1);
+ whd in match (lift_confL ????);
+ >(trans_if_M1true_notacc … Hacc)
+ [% | @(loop_Some ?????? Hloop1)]
+ |cases outc1 #s1 #t1 %
+ |@(loop_lift ???
+ (λc.(lift_confR … (lift_confR sig (states ? M2) (states ? M3) c)))
+ … Hloop2)
+ [ * #s2 #t2 %
+ | #c0 #Hhalt >(step_if_liftM3 … Hhalt) // ]
+ ]
+ |%2 @(ex_intro … (ctape ?? outc1)) %
+ [@HMfalse @(\Pf Hacc) | >(config_expand ?? outc2) @HM3 ]
+ ]
+ ]
+qed.
+