+
+(* composition with guards *)
+theorem sem_seq_guarded: ∀sig.∀M1,M2:TM sig.∀Pre1,Pre2,R1,R2.
+ GRealize sig M1 Pre1 R1 → GRealize sig M2 Pre2 R2 →
+ (∀t1,t2.Pre1 t1 → R1 t1 t2 → Pre2 t2) →
+ GRealize sig (M1 · M2) Pre1 (R1 ∘ R2).
+#sig #M1 #M2 #Pre1 #Pre2 #R1 #R2 #HGR1 #HGR2 #Hinv #t1 #HPre1
+cases (HGR1 t1 HPre1) #k1 * #outc1 * #Hloop1 #HM1
+cases (HGR2 (ctape sig (states ? M1) outc1) ?)
+ [2: @(Hinv … HPre1 HM1)]
+#k2 * #outc2 * #Hloop2 #HM2
+@(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
+%
+[@(loop_merge ???????????
+ (loop_lift ??? (lift_confL sig (states sig M1) (states sig M2))
+ (step sig M1) (step sig (seq sig M1 M2))
+ (λ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_seq_liftL //
+ | #x <p_halt_liftL %
+ |6:cases outc1 #s1 #t1 %
+ |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
+ [ * #s2 #t2 %
+ | #c0 #Hhalt <step_seq_liftR // ]
+ |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
+ generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
+ >(trans_liftL_true sig M1 M2 ??)
+ [ whd in ⊢ (??%?); whd in ⊢ (???%);
+ @config_eq whd in ⊢ (???%); //
+ | @(loop_Some ?????? Hloop10) ]
+ ]
+| @(ex_intro … (ctape ? (FinSum (states ? M1) (states ? M2)) (lift_confL … outc1)))
+ % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R //
+]
+qed.
+
+theorem sem_seq_app_guarded: ∀sig.∀M1,M2:TM sig.∀Pre1,Pre2,R1,R2,R3.
+ GRealize sig M1 Pre1 R1 → GRealize sig M2 Pre2 R2 →
+ (∀t1,t2.Pre1 t1 → R1 t1 t2 → Pre2 t2) → R1 ∘ R2 ⊆ R3 →
+ GRealize sig (M1 · M2) Pre1 R3.
+#sig #M1 #M2 #Pre1 #Pre2 #R1 #R2 #R3 #HR1 #HR2 #Hinv #Hsub
+#t #HPre1 cases (sem_seq_guarded … HR1 HR2 Hinv t HPre1)
+#k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
+% [@Hloop |@Hsub @Houtc]
+qed.