---

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


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)
19. x : A
20. x ↓∈ X es e
21. x@0 : B
22. x@0 ↓∈ Y es e
23. x@1 : C
24. x@1 ↓∈ Z es e
25. b = {only(F loc(e) x x@0 x@1)} ∈ bag(D)
26. b1 : bag(D)
27. x1 : A
28. x1 ↓∈ X es e
29. x2 : B
30. x2 ↓∈ Y es e
31. x3 : C
32. x3 ↓∈ Z es e
33. b1 = {only(F loc(e) x1 x2 x3)} ∈ bag(D)
34. #(F loc(e) x x@0 x@1) ≤ 1
35. #(F loc(e) x1 x2 x3) ≤ 1
36. #(F loc(e) x x@0 x@1) = 1 ∈ ℤ
37. #(F loc(e) x1 x2 x3) = 1 ∈ ℤ
38. F loc(e) x x@0 x@1 ~ {only(F loc(e) x x@0 x@1)}
39. F loc(e) x1 x2 x3 ~ {only(F loc(e) x1 x2 x3)}
40. v2 = only(F loc(e) x1 x2 x3) ∈ D
41. v1 = only(F loc(e) x x@0 x@1) ∈ D
⊢ v1 = v2 ∈ D
BY
{ ((InstHyp [⌈e⌉;⌈x1⌉;⌈x⌉] (-30)⋅ THENA (Auto THEN Unfold `classrel` 0 THEN Auto))
   THEN (InstHyp [⌈e⌉;⌈x2⌉;⌈x@0⌉] (-30)⋅ THENA (Auto THEN Unfold `classrel` 0 THEN Auto))
   THEN (InstHyp [⌈e⌉;⌈x3⌉;⌈x@1⌉] (-30)⋅ THENA (Auto THEN Unfold `classrel` 0 THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  B  :  Type
5.  C  :  Type
6.  D  :  Type
7.  F  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C  {}\mrightarrow{}  bag(D)
8.  X  :  EClass(A)
9.  Y  :  EClass(B)
10.  Z  :  EClass(C)
11.  \mforall{}i:Id.  \mforall{}a:A.  \mforall{}b:B.  \mforall{}c:C.    (\#(F  i  a  b  c)  \mleq{}  1)
12.  \mforall{}e:E.  \mforall{}v1,v2:A.    (v1  \mmember{}  X(e)  {}\mRightarrow{}  v2  \mmember{}  X(e)  {}\mRightarrow{}  (v1  =  v2))
13.  \mforall{}e:E.  \mforall{}v1,v2:B.    (v1  \mmember{}  Y(e)  {}\mRightarrow{}  v2  \mmember{}  Y(e)  {}\mRightarrow{}  (v1  =  v2))
14.  \mforall{}e:E.  \mforall{}v1,v2:C.    (v1  \mmember{}  Z(e)  {}\mRightarrow{}  v2  \mmember{}  Z(e)  {}\mRightarrow{}  (v1  =  v2))
15.  e  :  E@i
16.  v1  :  D@i
17.  v2  :  D@i
18.  b  :  bag(D)
19.  x  :  A
20.  x  \mdownarrow{}\mmember{}  X  es  e
21.  x@0  :  B
22.  x@0  \mdownarrow{}\mmember{}  Y  es  e
23.  x@1  :  C
24.  x@1  \mdownarrow{}\mmember{}  Z  es  e
25.  b  =  \{only(F  loc(e)  x  x@0  x@1)\}
26.  b1  :  bag(D)
27.  x1  :  A
28.  x1  \mdownarrow{}\mmember{}  X  es  e
29.  x2  :  B
30.  x2  \mdownarrow{}\mmember{}  Y  es  e
31.  x3  :  C
32.  x3  \mdownarrow{}\mmember{}  Z  es  e
33.  b1  =  \{only(F  loc(e)  x1  x2  x3)\}
34.  \#(F  loc(e)  x  x@0  x@1)  \mleq{}  1
35.  \#(F  loc(e)  x1  x2  x3)  \mleq{}  1
36.  \#(F  loc(e)  x  x@0  x@1)  =  1
37.  \#(F  loc(e)  x1  x2  x3)  =  1
38.  F  loc(e)  x  x@0  x@1  \msim{}  \{only(F  loc(e)  x  x@0  x@1)\}
39.  F  loc(e)  x1  x2  x3  \msim{}  \{only(F  loc(e)  x1  x2  x3)\}
40.  v2  =  only(F  loc(e)  x1  x2  x3)
41.  v1  =  only(F  loc(e)  x  x@0  x@1)
\mvdash{}  v1  =  v2


By

---

Latex:
((InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-30)\mcdot{}  THENA  (Auto  THEN  Unfold  `classrel`  0  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}x@0\mkleeneclose{}]  (-30)\mcdot{}  THENA  (Auto  THEN  Unfold  `classrel`  0  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x3\mkleeneclose{};\mkleeneopen{}x@1\mkleeneclose{}]  (-30)\mcdot{}  THENA  (Auto  THEN  Unfold  `classrel`  0  THEN  Auto))
  THEN  Auto)

---

Home Index