Step
*
1
6
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. ¬↑first(e)
17. ¬↑e ∈b X2
18. ¬↑e ∈b X1
19. ∀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])))
20. ∀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
21. v : B@i
22. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
23. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
⊢ P[e;state-class2(init;tr1;X1;tr2;X2)(pred(e))]
BY
{ (InstHyp [⌈state-class2(init;tr1;X1;tr2;X2)(pred(e))⌉;⌈e⌉] (-4)⋅ THENA (Auto THEN ProveFunctional THEN Auto)) }
1
.....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 X2
18. ¬↑e ∈b X1
19. ∀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])))
20. ∀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
21. v : B@i
22. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
23. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
⊢ 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
2
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 X2
18. ¬↑e ∈b X1
19. ∀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])))
20. ∀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
21. v : B@i
22. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
23. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
24. if e ∈b X1 then ∀a:A1. (a ∈ X1(e) ⇒ P[e;tr1 loc(e) a state-class2(init;tr1;X1;tr2;X2)(pred(e))])
if e ∈b X2 then ∀a:A2. (a ∈ X2(e) ⇒ P[e;tr2 loc(e) a state-class2(init;tr1;X1;tr2;X2)(pred(e))])
else P[e;state-class2(init;tr1;X1;tr2;X2)(pred(e))]
fi
⊢ P[e;state-class2(init;tr1;X1;tr2;X2)(pred(e))]
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{}first(e)
17. \mneg{}\muparrow{}e \mmember{}\msubb{} X2
18. \mneg{}\muparrow{}e \mmember{}\msubb{} X1
19. \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])))
20. \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
21. v : B@i
22. v \mmember{} state-class2(init;tr1;X1;tr2;X2)(e)@i
23. v = state-class2(init;tr1;X1;tr2;X2)(e)
\mvdash{} P[e;state-class2(init;tr1;X1;tr2;X2)(pred(e))]
By
Latex:
(InstHyp [\mkleeneopen{}state-class2(init;tr1;X1;tr2;X2)(pred(e))\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}] (-4)\mcdot{}
THENA (Auto THEN ProveFunctional THEN Auto)
)
Home
Index