---

Step * 2 2 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. v1 ↓∈ b
20. x : A
21. x ↓∈ X es e
22. x@0 : B
23. x@0 ↓∈ Y es e
24. x@1 : C
25. x@1 ↓∈ Z es e
26. b = (F loc(e) x x@0 x@1) ∈ bag(D)
27. ↓∃b:bag(D). (v2 ↓∈ b ∧ b ↓∈ lifting-gen-list-rev(3;λn.[X es e; Y es e; Z es e][n]) 0 (F loc(e)))
28. #(F loc(e) x x@0 x@1) ≤ 1
⊢ v1 = v2 ∈ D
BY
{ (SquashExRepD
   THEN RepeatFor 4 ((RecUnfold `lifting-gen-list-rev` (-2) THEN Reduce (-2)))
   THEN RepeatFor 4 ((BagMemberD (-2) THEN SquashExRepD))
   THEN (InstHyp [⌈loc(e)⌉;⌈x1⌉;⌈x2⌉;⌈x3⌉] (-26)⋅ THENA Auto)) }

1
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. v1 ↓∈ b
20. x : A
21. x ↓∈ X es e
22. x@0 : B
23. x@0 ↓∈ Y es e
24. x@1 : C
25. x@1 ↓∈ Z es e
26. b = (F loc(e) x x@0 x@1) ∈ bag(D)
27. b1 : bag(D)
28. v2 ↓∈ b1
29. x1 : A
30. x1 ↓∈ X es e
31. x2 : B
32. x2 ↓∈ Y es e
33. x3 : C
34. x3 ↓∈ Z es e
35. b1 = (F loc(e) x1 x2 x3) ∈ bag(D)
36. #(F loc(e) x x@0 x@1) ≤ 1
37. #(F loc(e) x1 x2 x3) ≤ 1
⊢ v1 = v2 ∈ D

---

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.  v1  \mdownarrow{}\mmember{}  b
20.  x  :  A
21.  x  \mdownarrow{}\mmember{}  X  es  e
22.  x@0  :  B
23.  x@0  \mdownarrow{}\mmember{}  Y  es  e
24.  x@1  :  C
25.  x@1  \mdownarrow{}\mmember{}  Z  es  e
26.  b  =  (F  loc(e)  x  x@0  x@1)
27.  \mdownarrow{}\mexists{}b:bag(D).  (v2  \mdownarrow{}\mmember{}  b  \mwedge{}  b  \mdownarrow{}\mmember{}  lifting-gen-list-rev(3;\mlambda{}n.[X  es  e;  Y  es  e;  Z  es  e][n])  0  (F  loc(e)))
28.  \#(F  loc(e)  x  x@0  x@1)  \mleq{}  1
\mvdash{}  v1  =  v2


By

---

Latex:
(SquashExRepD
  THEN  RepeatFor  4  ((RecUnfold  `lifting-gen-list-rev`  (-2)  THEN  Reduce  (-2)))
  THEN  RepeatFor  4  ((BagMemberD  (-2)  THEN  SquashExRepD))
  THEN  (InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}x3\mkleeneclose{}]  (-26)\mcdot{}  THENA  Auto))

---

Home Index