Step
*
1
of Lemma
decidable__exists-pred-iterated-classrel-between3-sv
1. [Info] : Type
2. [T] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : T ─→ S ─→ S@i
6. X : EClass(T)@i'
7. es : EO+(Info)@i'
8. P : T ─→ S ─→ ℙ@i'
9. e1 : E@i
10. single-valued-classrel(es;X;T)@i
11. single-valued-bag(init loc(e1);S)@i
12. ∀v:T. ∀s:S. Dec(P[v;s])@i
13. e2 : E@i
14. ∀e':E
((e' < e2)
⇒ Dec(∃e:E
∃s:S
((e1 <loc e) ∧ e ≤loc e' ∧ iterated-classrel(es;S;T;f;init;X;pred(e);s) ∧ (∃v:T. (v ∈ X(e) ∧ P[v;s])))))
15. loc(e1) = loc(e2) ∈ Id
16. Dec(∃v:T. v ∈ X(e2))
⊢ Dec(∃e:E
∃s:S. ((e1 <loc e) ∧ e ≤loc e2 ∧ iterated-classrel(es;S;T;f;init;X;pred(e);s) ∧ (∃v:T. (v ∈ X(e) ∧ P[v;s]))))
BY
{ ((Assert ⌈Dec(↑first(e2))⌉⋅ THENA Auto) THEN D (-1)) }
1
1. [Info] : Type
2. [T] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : T ─→ S ─→ S@i
6. X : EClass(T)@i'
7. es : EO+(Info)@i'
8. P : T ─→ S ─→ ℙ@i'
9. e1 : E@i
10. single-valued-classrel(es;X;T)@i
11. single-valued-bag(init loc(e1);S)@i
12. ∀v:T. ∀s:S. Dec(P[v;s])@i
13. e2 : E@i
14. ∀e':E
((e' < e2)
⇒ Dec(∃e:E
∃s:S
((e1 <loc e) ∧ e ≤loc e' ∧ iterated-classrel(es;S;T;f;init;X;pred(e);s) ∧ (∃v:T. (v ∈ X(e) ∧ P[v;s])))))
15. loc(e1) = loc(e2) ∈ Id
16. Dec(∃v:T. v ∈ X(e2))
17. ↑first(e2)
⊢ Dec(∃e:E
∃s:S. ((e1 <loc e) ∧ e ≤loc e2 ∧ iterated-classrel(es;S;T;f;init;X;pred(e);s) ∧ (∃v:T. (v ∈ X(e) ∧ P[v;s]))))
2
1. [Info] : Type
2. [T] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : T ─→ S ─→ S@i
6. X : EClass(T)@i'
7. es : EO+(Info)@i'
8. P : T ─→ S ─→ ℙ@i'
9. e1 : E@i
10. single-valued-classrel(es;X;T)@i
11. single-valued-bag(init loc(e1);S)@i
12. ∀v:T. ∀s:S. Dec(P[v;s])@i
13. e2 : E@i
14. ∀e':E
((e' < e2)
⇒ Dec(∃e:E
∃s:S
((e1 <loc e) ∧ e ≤loc e' ∧ iterated-classrel(es;S;T;f;init;X;pred(e);s) ∧ (∃v:T. (v ∈ X(e) ∧ P[v;s])))))
15. loc(e1) = loc(e2) ∈ Id
16. Dec(∃v:T. v ∈ X(e2))
17. ¬↑first(e2)
⊢ Dec(∃e:E
∃s:S. ((e1 <loc e) ∧ e ≤loc e2 ∧ iterated-classrel(es;S;T;f;init;X;pred(e);s) ∧ (∃v:T. (v ∈ X(e) ∧ P[v;s]))))
Latex:
1. [Info] : Type
2. [T] : Type
3. [S] : Type
4. init : Id {}\mrightarrow{} bag(S)@i
5. f : T {}\mrightarrow{} S {}\mrightarrow{} S@i
6. X : EClass(T)@i'
7. es : EO+(Info)@i'
8. P : T {}\mrightarrow{} S {}\mrightarrow{} \mBbbP{}@i'
9. e1 : E@i
10. single-valued-classrel(es;X;T)@i
11. single-valued-bag(init loc(e1);S)@i
12. \mforall{}v:T. \mforall{}s:S. Dec(P[v;s])@i
13. e2 : E@i
14. \mforall{}e':E
((e' < e2)
{}\mRightarrow{} Dec(\mexists{}e:E
\mexists{}s:S
((e1 <loc e)
\mwedge{} e \mleq{}loc e'
\mwedge{} iterated-classrel(es;S;T;f;init;X;pred(e);s)
\mwedge{} (\mexists{}v:T. (v \mmember{} X(e) \mwedge{} P[v;s])))))
15. loc(e1) = loc(e2)
16. Dec(\mexists{}v:T. v \mmember{} X(e2))
\mvdash{} Dec(\mexists{}e:E
\mexists{}s:S
((e1 <loc e)
\mwedge{} e \mleq{}loc e2
\mwedge{} iterated-classrel(es;S;T;f;init;X;pred(e);s)
\mwedge{} (\mexists{}v:T. (v \mmember{} X(e) \mwedge{} P[v;s]))))
By
((Assert \mkleeneopen{}Dec(\muparrow{}first(e2))\mkleeneclose{}\mcdot{} THENA Auto) THEN D (-1))
Home
Index