---

Step * 1 1 of Lemma state-class2-inv


1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. P : E ─→ B ─→ ℙ@i'
12. single-valued-classrel(es;X1;A1)@i
13. single-valued-classrel(es;X2;A2)@i
14. disjoint-classrel(es;A1;X1;A2;X2)@i
15. e : E@i
16. ∀e1:E
      ((e1 < e)
      ⇒ (∀s:B. ∀e':E.
            (e' ≤loc e1 
            ⇒ if first(e')
               then s = (init loc(e')) ∈ B
               else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
               fi 
            ⇒ if e' ∈b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
               if e' ∈b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
               else P[e';s]
               fi ))
      ⇒ (∀v:B. (v ∈ state-class2(init;tr1;X1;tr2;X2)(e1) ⇒ P[e1;v])))
17. ∀s:B. ∀e':E.
      (e' ≤loc e 
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi 
      ⇒ if e' ∈b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
18. v : B@i
19. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
20. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
21. ↑e ∈b X1
22. ↑first(e)
⊢ P[e;tr1 loc(e) X1@e (init loc(e))]
BY
{ ((InstHyp [⌈init loc(e)⌉;⌈e⌉] (-6)⋅ THEN Auto)
   THEN (SplitOnHypITE (-1) THEN Auto)
   THEN BackThruSomeHyp
   THEN BLemma `classrel-classfun-res-alt2`
   THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  [B]  :  Type
3.  [A1]  :  Type
4.  [A2]  :  Type
5.  init  :  Id  {}\mrightarrow{}  B@i
6.  tr1  :  Id  {}\mrightarrow{}  A1  {}\mrightarrow{}  B  {}\mrightarrow{}  B@i
7.  tr2  :  Id  {}\mrightarrow{}  A2  {}\mrightarrow{}  B  {}\mrightarrow{}  B@i
8.  X1  :  EClass(A1)@i'
9.  X2  :  EClass(A2)@i'
10.  es  :  EO+(Info)@i'
11.  P  :  E  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}@i'
12.  single-valued-classrel(es;X1;A1)@i
13.  single-valued-classrel(es;X2;A2)@i
14.  disjoint-classrel(es;A1;X1;A2;X2)@i
15.  e  :  E@i
16.  \mforall{}e1:E
            ((e1  <  e)
            {}\mRightarrow{}  (\mforall{}s:B.  \mforall{}e':E.
                        (e'  \mleq{}loc  e1 
                        {}\mRightarrow{}  if  first(e')
                              then  s  =  (init  loc(e'))
                              else  s  \mmember{}  state-class2(init;tr1;X1;tr2;X2)(pred(e'))  \mwedge{}  P[pred(e');s]
                              fi 
                        {}\mRightarrow{}  if  e'  \mmember{}\msubb{}  X1  then  \mforall{}a:A1.  (a  \mmember{}  X1(e')  {}\mRightarrow{}  P[e';tr1  loc(e')  a  s])
                              if  e'  \mmember{}\msubb{}  X2  then  \mforall{}a:A2.  (a  \mmember{}  X2(e')  {}\mRightarrow{}  P[e';tr2  loc(e')  a  s])
                              else  P[e';s]
                              fi  ))
            {}\mRightarrow{}  (\mforall{}v:B.  (v  \mmember{}  state-class2(init;tr1;X1;tr2;X2)(e1)  {}\mRightarrow{}  P[e1;v])))
17.  \mforall{}s:B.  \mforall{}e':E.
            (e'  \mleq{}loc  e 
            {}\mRightarrow{}  if  first(e')
                  then  s  =  (init  loc(e'))
                  else  s  \mmember{}  state-class2(init;tr1;X1;tr2;X2)(pred(e'))  \mwedge{}  P[pred(e');s]
                  fi 
            {}\mRightarrow{}  if  e'  \mmember{}\msubb{}  X1  then  \mforall{}a:A1.  (a  \mmember{}  X1(e')  {}\mRightarrow{}  P[e';tr1  loc(e')  a  s])
                  if  e'  \mmember{}\msubb{}  X2  then  \mforall{}a:A2.  (a  \mmember{}  X2(e')  {}\mRightarrow{}  P[e';tr2  loc(e')  a  s])
                  else  P[e';s]
                  fi  )@i
18.  v  :  B@i
19.  v  \mmember{}  state-class2(init;tr1;X1;tr2;X2)(e)@i
20.  v  =  state-class2(init;tr1;X1;tr2;X2)(e)
21.  \muparrow{}e  \mmember{}\msubb{}  X1
22.  \muparrow{}first(e)
\mvdash{}  P[e;tr1  loc(e)  X1@e  (init  loc(e))]


By

---

Latex:
((InstHyp  [\mkleeneopen{}init  loc(e)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto)
  THEN  (SplitOnHypITE  (-1)  THEN  Auto)
  THEN  BackThruSomeHyp
  THEN  BLemma  `classrel-classfun-res-alt2`
  THEN  Auto)

---

Home Index