---

Step * of Lemma simple-loc-comb-3-concat-single-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B,C,D:Type]. ∀[F:Id ─→ A ─→ B ─→ C ─→ bag(D)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
∀[Z:EClass(C)].
  single-valued-classrel(es;concat-lifting-loc-3(F)|Loc, X, Y, Z|;D) 
  supposing (∀i:Id. ∀a:A. ∀b:B. ∀c:C.  (#(F i a b c) ≤ 1))
  ∧ single-valued-classrel(es;X;A)
  ∧ single-valued-classrel(es;Y;B)
  ∧ single-valued-classrel(es;Z;C)
BY
{ (Unfold `single-valued-classrel` 0
   THEN (UnivCD THENA MaAuto)
   THEN RepD⋅
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN BagMemberD (-2)) }

1
.....wf..... 
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. D : Type
7. F : Id ─→ A ─→ B ─→ C ─→ bag(D)
8. X : EClass(A)
9. Y : EClass(B)
10. Z : EClass(C)
11. ∀i:Id. ∀a:A. ∀b:B. ∀c:C.  (#(F i a b c) ≤ 1)
12. ∀e:E. ∀v1,v2:A.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ A))
13. ∀e:E. ∀v1,v2:B.  (v1 ∈ Y(e) ⇒ v2 ∈ Y(e) ⇒ (v1 = v2 ∈ B))
14. ∀e:E. ∀v1,v2:C.  (v1 ∈ Z(e) ⇒ v2 ∈ Z(e) ⇒ (v1 = v2 ∈ C))
15. e : E@i
16. v1 : D@i
17. v2 : D@i
18. v1 ↓∈ bag-union(lifting-gen-list-rev(3;λn.[X es e; Y es e; Z es e][n]) 0 (F loc(e)))@i
19. v2 ↓∈ concat-lifting-loc-3(F) loc(e) (X es e) (Y es e) (Z es e)@i
⊢ lifting-gen-list-rev(3;λn.[X es e; Y es e; Z es e][n]) 0 (F loc(e)) ∈ bag(bag(D))

2
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. C : Type
6. D : Type
7. F : Id ─→ A ─→ B ─→ C ─→ bag(D)
8. X : EClass(A)
9. Y : EClass(B)
10. Z : EClass(C)
11. ∀i:Id. ∀a:A. ∀b:B. ∀c:C.  (#(F i a b c) ≤ 1)
12. ∀e:E. ∀v1,v2:A.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ A))
13. ∀e:E. ∀v1,v2:B.  (v1 ∈ Y(e) ⇒ v2 ∈ Y(e) ⇒ (v1 = v2 ∈ B))
14. ∀e:E. ∀v1,v2:C.  (v1 ∈ Z(e) ⇒ v2 ∈ Z(e) ⇒ (v1 = v2 ∈ C))
15. e : E@i
16. v1 : D@i
17. v2 : D@i
18. ↓∃b:bag(D). (v1 ↓∈ b ∧ b ↓∈ lifting-gen-list-rev(3;λn.[X es e; Y es e; Z es e][n]) 0 (F loc(e)))
19. v2 ↓∈ concat-lifting-loc-3(F) loc(e) (X es e) (Y es e) (Z es e)@i
⊢ v1 = v2 ∈ D

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B,C,D:Type].  \mforall{}[F:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C  {}\mrightarrow{}  bag(D)].  \mforall{}[X:EClass(A)].
\mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(C)].
    single-valued-classrel(es;concat-lifting-loc-3(F)|Loc,  X,  Y,  Z|;D) 
    supposing  (\mforall{}i:Id.  \mforall{}a:A.  \mforall{}b:B.  \mforall{}c:C.    (\#(F  i  a  b  c)  \mleq{}  1))
    \mwedge{}  single-valued-classrel(es;X;A)
    \mwedge{}  single-valued-classrel(es;Y;B)
    \mwedge{}  single-valued-classrel(es;Z;C)


By

---

Latex:
(Unfold  `single-valued-classrel`  0
  THEN  (UnivCD  THENA  MaAuto)
  THEN  RepD\mcdot{}
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  BagMemberD  (-2))

---

Home Index