Step
*
1
4
1
of Lemma
state-class2-inv
.....antecedent.....
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. ¬↑first(e)
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. ↑e ∈b X2
⊢ if first(e)
then state-class2(init;tr1;X1;tr2;X2)(pred(e)) = (init loc(e)) ∈ B
else state-class2(init;tr1;X1;tr2;X2)(pred(e)) ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e))
∧ P[pred(e);state-class2(init;tr1;X1;tr2;X2)(pred(e))]
fi
BY
{ ((AutoSplit THEN Auto)
THEN Try (((BLemma `classrel-classfun` THEN Auto) THEN ProveFunctional THEN Auto))
THEN InstHyp [⌈pred(e)⌉;⌈state-class2(init;tr1;X1;tr2;X2)(pred(e))⌉] (-7)⋅
THEN Auto
THEN ProveFunctional
THEN Auto) }
Latex:
Latex:
.....antecedent.....
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{}first(e)
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{}e \mmember{}\msubb{} X2
\mvdash{} if first(e)
then state-class2(init;tr1;X1;tr2;X2)(pred(e)) = (init loc(e))
else state-class2(init;tr1;X1;tr2;X2)(pred(e)) \mmember{} state-class2(init;tr1;X1;tr2;X2)(pred(e))
\mwedge{} P[pred(e);state-class2(init;tr1;X1;tr2;X2)(pred(e))]
fi
By
Latex:
((AutoSplit THEN Auto)
THEN Try (((BLemma `classrel-classfun` THEN Auto) THEN ProveFunctional THEN Auto))
THEN InstHyp [\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}state-class2(init;tr1;X1;tr2;X2)(pred(e))\mkleeneclose{}] (-7)\mcdot{}
THEN Auto
THEN ProveFunctional
THEN Auto)
Home
Index