---

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

.....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))
BY
{ (RepeatFor 4 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0)) THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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.  v2  \mdownarrow{}\mmember{}  bag-union(lifting-gen-list-rev(3;\mlambda{}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)  \mleq{}  1
\mvdash{}  lifting-gen-list-rev(3;\mlambda{}n.[X  es  e;  Y  es  e;  Z  es  e][n])  0  (F  loc(e))  \mmember{}  bag(bag(D))


By

---

Latex:
(RepeatFor  4  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0))  THEN  Auto)

---

Home Index