---

Step * 1 of Lemma rec-combined-class-opt-1-single-val0


1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. F : A ─→ B ─→ B
6. X : EClass(A)
7. init : Id ─→ bag(B)
8. e : E@i
9. ∀e':E
     ((e' < e)
     ⇒ (∀v1,v2:B.
           (single-valued-bag(init loc(e');B)
           ⇒ single-valued-classrel(es;X;A)
           ⇒ v2 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ v1 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ (v1 = v2 ∈ B))))
10. v1 : B@i
11. v2 : B@i
12. single-valued-bag(init loc(e);B)@i
13. single-valued-classrel(es;X;A)@i
14. a : A
15. b : B
16. v2 = (F a b) ∈ B
17. e' : E
18. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'))) e e'
19. b ∈ lifting-2(F)|X,Prior(self)?init|(e')
20. a ∈ X(e)
21. a1 : A
22. b1 : B
23. v1 = (F a1 b1) ∈ B
24. e1 : E
25. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'))) e e1
26. b1 ∈ lifting-2(F)|X,Prior(self)?init|(e1)
27. a1 ∈ X(e)
28. a = a1 ∈ A
⊢ b1 = b ∈ B
BY
{ (All (RepUR ``es-p-local-pred``) THEN RepD THEN UseLoclTri ⌈es⌉⌈e'⌉⌈e1⌉⋅) }

1
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. F : A ─→ B ─→ B
6. X : EClass(A)
7. init : Id ─→ bag(B)
8. e : E@i
9. ∀e':E
     ((e' < e)
     ⇒ (∀v1,v2:B.
           (single-valued-bag(init loc(e');B)
           ⇒ single-valued-classrel(es;X;A)
           ⇒ v2 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ v1 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ (v1 = v2 ∈ B))))
10. v1 : B@i
11. v2 : B@i
12. single-valued-bag(init loc(e);B)@i
13. single-valued-classrel(es;X;A)@i
14. a : A
15. b : B
16. v2 = (F a b) ∈ B
17. e' : E
18. (e' <loc e)
19. ↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e')
20. ∀e'':E. ((e'' <loc e) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'')))
21. b ∈ lifting-2(F)|X,Prior(self)?init|(e')
22. a ∈ X(e)
23. a1 : A
24. b1 : B
25. v1 = (F a1 b1) ∈ B
26. e1 : E
27. (e1 <loc e)
28. ↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e1)
29. ∀e'':E. ((e'' <loc e) ⇒ (e1 <loc e'') ⇒ (¬↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'')))
30. b1 ∈ lifting-2(F)|X,Prior(self)?init|(e1)
31. a1 ∈ X(e)
32. a = a1 ∈ A
33. (e' <loc e1)
⊢ b1 = b ∈ B

2
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. F : A ─→ B ─→ B
6. X : EClass(A)
7. init : Id ─→ bag(B)
8. e : E@i
9. ∀e':E
     ((e' < e)
     ⇒ (∀v1,v2:B.
           (single-valued-bag(init loc(e');B)
           ⇒ single-valued-classrel(es;X;A)
           ⇒ v2 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ v1 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ (v1 = v2 ∈ B))))
10. v1 : B@i
11. v2 : B@i
12. single-valued-bag(init loc(e);B)@i
13. single-valued-classrel(es;X;A)@i
14. a : A
15. b : B
16. v2 = (F a b) ∈ B
17. e' : E
18. (e' <loc e)
19. ↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e')
20. ∀e'':E. ((e'' <loc e) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'')))
21. b ∈ lifting-2(F)|X,Prior(self)?init|(e')
22. a ∈ X(e)
23. a1 : A
24. b1 : B
25. v1 = (F a1 b1) ∈ B
26. e1 : E
27. (e1 <loc e)
28. ↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e1)
29. ∀e'':E. ((e'' <loc e) ⇒ (e1 <loc e'') ⇒ (¬↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'')))
30. b1 ∈ lifting-2(F)|X,Prior(self)?init|(e1)
31. a1 ∈ X(e)
32. a = a1 ∈ A
33. (e1 <loc e')
⊢ b1 = b ∈ B

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  F  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
6.  X  :  EClass(A)
7.  init  :  Id  {}\mrightarrow{}  bag(B)
8.  e  :  E@i
9.  \mforall{}e':E
          ((e'  <  e)
          {}\mRightarrow{}  (\mforall{}v1,v2:B.
                      (single-valued-bag(init  loc(e');B)
                      {}\mRightarrow{}  single-valued-classrel(es;X;A)
                      {}\mRightarrow{}  v2  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
                      {}\mRightarrow{}  v1  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
                      {}\mRightarrow{}  (v1  =  v2))))
10.  v1  :  B@i
11.  v2  :  B@i
12.  single-valued-bag(init  loc(e);B)@i
13.  single-valued-classrel(es;X;A)@i
14.  a  :  A
15.  b  :  B
16.  v2  =  (F  a  b)
17.  e'  :  E
18.  es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:B.  w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')))  e  e'
19.  b  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
20.  a  \mmember{}  X(e)
21.  a1  :  A
22.  b1  :  B
23.  v1  =  (F  a1  b1)
24.  e1  :  E
25.  es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:B.  w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')))  e  e1
26.  b1  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e1)
27.  a1  \mmember{}  X(e)
28.  a  =  a1
\mvdash{}  b1  =  b


By

---

Latex:
(All  (RepUR  ``es-p-local-pred``)  THEN  RepD  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e'\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mcdot{})

---

Home Index