---

Step * 2 2 of Lemma hdf-union-eq-disju


1. A : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. valueall-type(B)
6. u : A@i
7. v : A List@i
8. ∀X:hdataflow(A;B). ∀Y:hdataflow(A;C). ∀a:A.
     (hdf-out(X + Y*(v);a) = hdf-out((λx.(inl x)) o X || (λx.(inr x )) o Y*(v);a) ∈ bag(B + C))@i
9. X : hdataflow(A;B)@i
10. Y : hdataflow(A;C)@i
11. a : A@i
⊢ hdf-out(fst(X + Y(u))*(v);a) = hdf-out(fst((λx.(inl x)) o X || (λx.(inr x )) o Y(u))*(v);a) ∈ bag(B + C)
BY
{ ((RWO "hdf-union-ap" 0
    THENA (Try (Complete (Auto))
           THEN Fold `member` 0
           THEN GenConclAtAddrType ⌈hdataflow(A;B + C) × bag(B + C)⌉ [2;1;1;1]⋅
           THEN Auto)
    )
   THEN Reduce 0
   THEN (RWO "-4" 0
         THENA (Try (Complete (Auto))
                THEN Fold `member` 0
                THEN GenConclAtAddrType ⌈hdataflow(A;B + C) × bag(B + C)⌉ [2;1;1;1]⋅
                THEN Auto)
         )
   THEN (InstLemma `hdf-parallel-ap` [⌈A⌉;⌈B + C⌉;⌈(λx.(inl x)) o X⌉;⌈(λx.(inr x )) o Y⌉;⌈u⌉]⋅ THENA Auto)
   THEN (HypSubst' -1 0 THENA (GenConclAtAddrType ⌈hdataflow(A;B + C)⌉ [2;2;1;1]⋅ THEN Auto))
   THEN Reduce 0
   THEN (InstLemma `hdf-compose1-ap` [⌈A⌉;⌈B⌉;⌈B + C⌉;⌈X⌉;⌈λx.(inl x)⌉;⌈u⌉]⋅ THENA Auto)
   THEN (HypSubst' -1 0
         THENA (GenConclAtAddrType ⌈hdataflow(A;B + C)⌉ [2;2;1;1]⋅
                THEN Try (Complete (Auto))
                THEN GenConclAtAddrType ⌈hdataflow(A;B + C)⌉ [2;3;1;1]⋅
                THEN Try (Complete (Auto)))
         )
   THEN Reduce 0
   THEN (InstLemma `hdf-compose1-ap` [⌈A⌉;⌈C⌉;⌈B + C⌉;⌈Y⌉;⌈λx.(inr x )⌉;⌈u⌉]⋅ THENA Auto)
   THEN (HypSubst' -1 0
         THENA (GenConclAtAddrType ⌈hdataflow(A;B + C)⌉ [2;2;1;1]⋅
                THEN Try (Complete (Auto))
                THEN GenConclAtAddrType ⌈hdataflow(A;B + C)⌉ [2;3;1;1]⋅
                THEN Try (Complete (Auto)))
         )
   THEN Reduce 0
   THEN GenConclAtAddrType ⌈hdataflow(A;B + C)⌉ [2;1;1]⋅
   THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  valueall-type(C)
5.  valueall-type(B)
6.  u  :  A@i
7.  v  :  A  List@i
8.  \mforall{}X:hdataflow(A;B).  \mforall{}Y:hdataflow(A;C).  \mforall{}a:A.
          (hdf-out(X  +  Y*(v);a)  =  hdf-out((\mlambda{}x.(inl  x))  o  X  ||  (\mlambda{}x.(inr  x  ))  o  Y*(v);a))@i
9.  X  :  hdataflow(A;B)@i
10.  Y  :  hdataflow(A;C)@i
11.  a  :  A@i
\mvdash{}  hdf-out(fst(X  +  Y(u))*(v);a)  =  hdf-out(fst((\mlambda{}x.(inl  x))  o  X  ||  (\mlambda{}x.(inr  x  ))  o  Y(u))*(v);a)


By

((RWO  "hdf-union-ap"  0
    THENA  (Try  (Complete  (Auto))
                  THEN  Fold  `member`  0
                  THEN  GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)  \mtimes{}  bag(B  +  C)\mkleeneclose{}  [2;1;1;1]\mcdot{}
                  THEN  Auto)
    )
  THEN  Reduce  0
  THEN  (RWO  "-4"  0
              THENA  (Try  (Complete  (Auto))
                            THEN  Fold  `member`  0
                            THEN  GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)  \mtimes{}  bag(B  +  C)\mkleeneclose{}  [2;1;1;1]\mcdot{}
                            THEN  Auto)
              )
  THEN  (InstLemma  `hdf-parallel-ap`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B  +  C\mkleeneclose{};\mkleeneopen{}(\mlambda{}x.(inl  x))  o  X\mkleeneclose{};\mkleeneopen{}(\mlambda{}x.(inr  x  ))  o  Y\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (HypSubst'  -1  0  THENA  (GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)\mkleeneclose{}  [2;2;1;1]\mcdot{}  THEN  Auto))
  THEN  Reduce  0
  THEN  (InstLemma  `hdf-compose1-ap`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}B  +  C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(inl  x)\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  -1  0
              THENA  (GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)\mkleeneclose{}  [2;2;1;1]\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)\mkleeneclose{}  [2;3;1;1]\mcdot{}
                            THEN  Try  (Complete  (Auto)))
              )
  THEN  Reduce  0
  THEN  (InstLemma  `hdf-compose1-ap`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}B  +  C\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(inr  x  )\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  -1  0
              THENA  (GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)\mkleeneclose{}  [2;2;1;1]\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)\mkleeneclose{}  [2;3;1;1]\mcdot{}
                            THEN  Try  (Complete  (Auto)))
              )
  THEN  Reduce  0
  THEN  GenConclAtAddrType  \mkleeneopen{}hdataflow(A;B  +  C)\mkleeneclose{}  [2;1;1]\mcdot{}
  THEN  Auto)

---

Home Index