---

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

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ lifting-2(F)|X,Prior(self)?init|(e) and 
     v2 ∈ lifting-2(F)|X,Prior(self)?init|(e) and 
     single-valued-classrel(es;X;A) and 
     single-valued-bag(init loc(e);B))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 7 (MoveToConcl (-1))
   THEN VrCausalInd'
   THEN Auto
   THEN RepeatFor 2 (MaUseClassRel (-2))
   THEN RepeatFor 2 (MaUseClassRel (-1))
   THEN (HypSubst' (-8) 0 THENA Auto)
   THEN (HypSubst' (-3) 0 THENA Auto)
   THEN UseSingleVal (-6) (-1)
   THEN (RevHypSubst' (-1) 0 THENA Auto)
   THEN MemCD
   THEN Auto
   THEN MaUseClassRel (-8)
   THEN MaUseClassRel (-3)) }

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. 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

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. 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. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ lifting-2(F)|X,Prior(self)?init|(e'))))
25. b1 ↓∈ init loc(e)
26. a1 ∈ X(e)
27. a = a1 ∈ A
⊢ b1 = b ∈ B

3
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. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ lifting-2(F)|X,Prior(self)?init|(e'))))
18. b ↓∈ init loc(e)
19. a ∈ X(e)
20. a1 : A
21. b1 : B
22. v1 = (F a1 b1) ∈ B
23. e' : E
24. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'))) e e'
25. b1 ∈ lifting-2(F)|X,Prior(self)?init|(e')
26. a1 ∈ X(e)
27. a = a1 ∈ A
⊢ b1 = b ∈ B

4
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. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ lifting-2(F)|X,Prior(self)?init|(e'))))
18. b ↓∈ init loc(e)
19. a ∈ X(e)
20. a1 : A
21. b1 : B
22. v1 = (F a1 b1) ∈ B
23. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ lifting-2(F)|X,Prior(self)?init|(e'))))
24. b1 ↓∈ init loc(e)
25. a1 ∈ X(e)
26. a = a1 ∈ A
⊢ b1 = b ∈ B

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[e:E].
\mforall{}[v1,v2:B].
    (v1  =  v2)  supposing 
          (v1  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e)  and 
          v2  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e)  and 
          single-valued-classrel(es;X;A)  and 
          single-valued-bag(init  loc(e);B))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  7  (MoveToConcl  (-1))
  THEN  VrCausalInd'
  THEN  Auto
  THEN  RepeatFor  2  (MaUseClassRel  (-2))
  THEN  RepeatFor  2  (MaUseClassRel  (-1))
  THEN  (HypSubst'  (-8)  0  THENA  Auto)
  THEN  (HypSubst'  (-3)  0  THENA  Auto)
  THEN  UseSingleVal  (-6)  (-1)
  THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
  THEN  MemCD
  THEN  Auto
  THEN  MaUseClassRel  (-8)
  THEN  MaUseClassRel  (-3))

---

Home Index