---

Step * of Lemma parallel-compose2-program-eq

∀[Info,B,C:Type]. ∀[X1,X2:Id ─→ hdataflow(Info;B ─→ bag(C))]. ∀[X:Id ─→ hdataflow(Info;B)].
  (X1 o X || X2 o X = X1 || X2 o X ∈ (Id ─→ hdataflow(Info;C))) supposing 
     (valueall-type(C) and 
     valueall-type(B) and 
     (↓B))
BY
{ (Auto
   THEN (Assert ⌈↓∃:B. value-type(bag(C))⌉⋅
         THENA (RenameVar `b' (-3) THEN D 0 THEN Auto THEN With ⌈b⌉ (D 0)⋅ THEN Auto)
         )
   THEN (InstLemma `local-class-equality` [⌈Info⌉;⌈C⌉;⌈(hdataflow-class(X1) || hdataflow-class(X2) o
                                                       hdataflow-class(X))⌉]⋅
         THENA Auto
         )⋅
   THEN (BHyp -1 
         THENA (Auto
                THEN Try ((SubsumeC ⌈LocalClass((hdataflow-class(X1) o hdataflow-class(X))
                                                || (hdataflow-class(X2) o hdataflow-class(X)))⌉⋅
                           THEN Try (Complete (Auto))
                           THEN (BLemma `subtype_rel-equal` THENM EqCD)
                           THEN Auto
                           THEN (BLemma `parallel-eclass2-left` THEN Auto)⋅))
                )
         )
   THEN RepUR ``parallel-class-program eclass2-program`` 0
   THEN Auto
   THEN (RWW "hdf-parallel-halted hdf-halted-compose2-iterate" 0 THENA Auto)
   THEN AutoBoolCase ⌈hdf-halted(X1 i*(inputs))⌉⋅
   THEN (AutoBoolCase ⌈hdf-halted(X i*(inputs))⌉⋅ THEN AutoBoolCase ⌈hdf-halted(X2 i*(inputs))⌉⋅))⋅ }

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X1,X2:Id  {}\mrightarrow{}  hdataflow(Info;B  {}\mrightarrow{}  bag(C))].  \mforall{}[X:Id  {}\mrightarrow{}  hdataflow(Info;B)].
    (X1  o  X  ||  X2  o  X  =  X1  ||  X2  o  X)  supposing  (valueall-type(C)  and  valueall-type(B)  and  (\mdownarrow{}B))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mdownarrow{}\mexists{}:B.  value-type(bag(C))\mkleeneclose{}\mcdot{}
              THENA  (RenameVar  `b'  (-3)  THEN  D  0  THEN  Auto  THEN  With  \mkleeneopen{}b\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
              )
  THEN  (InstLemma  `local-class-equality`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}(hdataflow-class(X1)  ||  hdataflow-class(X2)  o
                                                                                                          hdataflow-class(X))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )\mcdot{}
  THEN  (BHyp  -1 
              THENA  (Auto
                            THEN  Try  ((SubsumeC  \mkleeneopen{}LocalClass((hdataflow-class(X1)  o  hdataflow-class(X))
                                                                                            ||  (hdataflow-class(X2)  o  hdataflow-class(X)))\mkleeneclose{}\mcdot{}
                                                  THEN  Try  (Complete  (Auto))
                                                  THEN  (BLemma  `subtype\_rel-equal`  THENM  EqCD)
                                                  THEN  Auto
                                                  THEN  (BLemma  `parallel-eclass2-left`  THEN  Auto)\mcdot{}))
                            )
              )
  THEN  RepUR  ``parallel-class-program  eclass2-program``  0
  THEN  Auto
  THEN  (RWW  "hdf-parallel-halted  hdf-halted-compose2-iterate"  0  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}hdf-halted(X1  i*(inputs))\mkleeneclose{}\mcdot{}
  THEN  (AutoBoolCase  \mkleeneopen{}hdf-halted(X  i*(inputs))\mkleeneclose{}\mcdot{}  THEN  AutoBoolCase  \mkleeneopen{}hdf-halted(X2  i*(inputs))\mkleeneclose{}\mcdot{}))\mcdot{}

---

Home Index