---

Step * 2 of Lemma iterated_classrel-single-val

.....falsecase..... 
1. Info : Type
2. A : Type
3. S : Type
4. init : Id ─→ bag(S)
5. f : A ─→ S ─→ S
6. X : EClass(A)
7. es : EO+(Info)@i'
8. single-valued-classrel(es;X;A)@i
9. e : E@i
10. ∀e1:E
      ((e1 < e)
      ⇒ single-valued-bag(init loc(e1);S)
      ⇒ (∀v1,v2:S.
            (iterated_classrel(es;S;A;f;init;X;e1;v1) ⇒ iterated_classrel(es;S;A;f;init;X;e1;v2) ⇒ (v1 = v2 ∈ S))))
11. single-valued-bag(init loc(e);S)@i
12. v1 : S@i
13. v2 : S@i
14. z1 : S@i
15. iterated_classrel(es;S;A;f;init;X;pred(e);z1)@i
16. (∃a:A. (a ∈ X(e) ∧ (v1 = (f a z1) ∈ S))) ∨ ((∀a:A. (¬a ∈ X(e))) ∧ (v1 = z1 ∈ S))@i
17. z : S@i
18. iterated_classrel(es;S;A;f;init;X;pred(e);z)@i
19. (∃a:A. (a ∈ X(e) ∧ (v2 = (f a z) ∈ S))) ∨ ((∀a:A. (¬a ∈ X(e))) ∧ (v2 = z ∈ S))@i
20. ¬↑first(e)
21. ¬↑first(e)
⊢ v1 = v2 ∈ S
BY
{ ((InstHyp [⌈pred(e)⌉;⌈z1⌉;⌈z⌉] (-12)⋅ THENA Auto)
   THEN D (-7)
   THEN ExRepD
   THEN D (-4)
   THEN ExRepD
   THEN Auto
   THEN Try (Complete ((InstHyp [⌈a⌉] (-5)⋅ THEN Auto)))
   THEN Try (Complete ((InstHyp [⌈a⌉] (-10)⋅ THEN Auto)))
   THEN UseSingleVal (-10) (-5)
   THEN Auto) }

---

Latex:


.....falsecase..... 
1.  Info  :  Type
2.  A  :  Type
3.  S  :  Type
4.  init  :  Id  {}\mrightarrow{}  bag(S)
5.  f  :  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S
6.  X  :  EClass(A)
7.  es  :  EO+(Info)@i'
8.  single-valued-classrel(es;X;A)@i
9.  e  :  E@i
10.  \mforall{}e1:E
            ((e1  <  e)
            {}\mRightarrow{}  single-valued-bag(init  loc(e1);S)
            {}\mRightarrow{}  (\mforall{}v1,v2:S.
                        (iterated\_classrel(es;S;A;f;init;X;e1;v1)
                        {}\mRightarrow{}  iterated\_classrel(es;S;A;f;init;X;e1;v2)
                        {}\mRightarrow{}  (v1  =  v2))))
11.  single-valued-bag(init  loc(e);S)@i
12.  v1  :  S@i
13.  v2  :  S@i
14.  z1  :  S@i
15.  iterated\_classrel(es;S;A;f;init;X;pred(e);z1)@i
16.  (\mexists{}a:A.  (a  \mmember{}  X(e)  \mwedge{}  (v1  =  (f  a  z1))))  \mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(e)))  \mwedge{}  (v1  =  z1))@i
17.  z  :  S@i
18.  iterated\_classrel(es;S;A;f;init;X;pred(e);z)@i
19.  (\mexists{}a:A.  (a  \mmember{}  X(e)  \mwedge{}  (v2  =  (f  a  z))))  \mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(e)))  \mwedge{}  (v2  =  z))@i
20.  \mneg{}\muparrow{}first(e)
21.  \mneg{}\muparrow{}first(e)
\mvdash{}  v1  =  v2


By

((InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  (-12)\mcdot{}  THENA  Auto)
  THEN  D  (-7)
  THEN  ExRepD
  THEN  D  (-4)
  THEN  ExRepD
  THEN  Auto
  THEN  Try  (Complete  ((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-5)\mcdot{}  THEN  Auto)))
  THEN  Try  (Complete  ((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-10)\mcdot{}  THEN  Auto)))
  THEN  UseSingleVal  (-10)  (-5)
  THEN  Auto)

---

Home Index