V_____________________________________________________________*)
include "basics/vectors.ma".
+include "basics/finset.ma".
(* include "basics/relations.ma". *)
record tape (sig:FinSet): Type[0] ≝
#sig #S1 #S2 #outc cases outc #s #t %
qed.
+axiom daemon :∀P:Prop.P.
+
theorem sem_seq: ∀sig,M1,M2,R1,R2.
Realize sig M1 R1 → Realize sig M2 R2 →
Realize sig (seq sig M1 M2) (R1 ∘ R2).
+@daemon (* this no longer works: TODO *) (*
#sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t #i #outc #Hloop
cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
cases (HR2 (ctape sig (states ? M1) outc1)) #k2 * #outc2 * #Hloop2 #HM2
| @(ex_intro … (ctape ? (FinSum (states ? M1) (states ? M2)) (lift_confL … outc1)))
% // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R //
]
+*)
qed.