---

Step * 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). (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
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)⌉;⌈x⌉;⌈x@0⌉;⌈x@1⌉] (-17)⋅ THENA Auto)
   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. 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. v2 ↓∈ bag-union(lifting-gen-list-rev(3;λn.[X es e; Y es e; Z es e][n]) 0 (F loc(e)))@i
28. #(F loc(e) x x@0 x@1) ≤ 1
⊢ 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)
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

---

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.  \mdownarrow{}\mexists{}b:bag(D).  (v1  \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)))
19.  v2  \mdownarrow{}\mmember{}  concat-lifting-loc-3(F)  loc(e)  (X  es  e)  (Y  es  e)  (Z  es  e)@i
\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{}x\mkleeneclose{};\mkleeneopen{}x@0\mkleeneclose{};\mkleeneopen{}x@1\mkleeneclose{}]  (-17)\mcdot{}  THENA  Auto)
  THEN  BagMemberD  (-2))

---

Home Index