---

Step * 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. 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))
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.  v1  \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
19.  v2  \mdownarrow{}\mmember{}  concat-lifting-loc-3(F)  loc(e)  (X  es  e)  (Y  es  e)  (Z  es  e)@i
\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