---

Step * 1 2 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. (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
BY
{ ((Assert ⌈False⌉⋅ THEN Auto) THEN (InstHyp [⌈e'⌉] (-5)⋅ THENA Auto) THEN D (-1) THEN D 0 THEN MaAuto) }

---

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.  (e'  <loc  e)
19.  \mdownarrow{}\mexists{}w:B.  w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
20.  \mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (e'  <loc  e'')  {}\mRightarrow{}  (\mneg{}\mdownarrow{}\mexists{}w:B.  w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e'')))
21.  b  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
22.  a  \mmember{}  X(e)
23.  a1  :  A
24.  b1  :  B
25.  v1  =  (F  a1  b1)
26.  e1  :  E
27.  (e1  <loc  e)
28.  \mdownarrow{}\mexists{}w:B.  w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e1)
29.  \mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (e1  <loc  e'')  {}\mRightarrow{}  (\mneg{}\mdownarrow{}\mexists{}w:B.  w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e'')))
30.  b1  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e1)
31.  a1  \mmember{}  X(e)
32.  a  =  a1
33.  (e1  <loc  e')
\mvdash{}  b1  =  b


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  D  0
  THEN  MaAuto)

---

Home Index