---

Step * of Lemma hdf-halted-compose2-iterate

∀[A,B,C:Type]. ∀[inputs:A List]. ∀[X1:hdataflow(A;B ─→ bag(C))]. ∀[X2:hdataflow(A;B)].
  hdf-halted(X1 o X2*(inputs)) = hdf-halted(X1*(inputs)) ∨bhdf-halted(X2*(inputs)) supposing valueall-type(C)
BY
{ (InductionOnList
   THEN Auto
   THEN Reduce 0
   THEN Try (((BLemma `iff_imp_equal_bool` THENA Auto) THEN RWO "hdf-halted-compose2" 0⋅ THEN Auto))
   THEN (RWO "hdf-compose2-ap" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[inputs:A  List].  \mforall{}[X1:hdataflow(A;B  {}\mrightarrow{}  bag(C))].  \mforall{}[X2:hdataflow(A;B)].
    hdf-halted(X1  o  X2*(inputs))  =  hdf-halted(X1*(inputs))  \mvee{}\msubb{}hdf-halted(X2*(inputs)) 
    supposing  valueall-type(C)


By

(InductionOnList
  THEN  Auto
  THEN  Reduce  0
  THEN  Try  (((BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)  THEN  RWO  "hdf-halted-compose2"  0\mcdot{}  THEN  Auto))
  THEN  (RWO  "hdf-compose2-ap"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index