---

Step * 1 5 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. ¬↑e ∈b X2
17. ¬↑e ∈b X1
18. ∀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])))
19. ∀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
20. v : B@i
21. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
22. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
23. ↑first(e)
⊢ P[e;init loc(e)]
BY
{ ((InstHyp [⌈init loc(e)⌉;⌈e⌉] (-5)⋅ THEN Auto) THEN SplitOnHypITE (-1) 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.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  X2
17.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  X1
18.  \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])))
19.  \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
20.  v  :  B@i
21.  v  \mmember{}  state-class2(init;tr1;X1;tr2;X2)(e)@i
22.  v  =  state-class2(init;tr1;X1;tr2;X2)(e)
23.  \muparrow{}first(e)
\mvdash{}  P[e;init  loc(e)]


By

---

Latex:
((InstHyp  [\mkleeneopen{}init  loc(e)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-5)\mcdot{}  THEN  Auto)  THEN  SplitOnHypITE  (-1)  THEN  Auto)

---

Home Index