Step
*
1
1
1
2
1
1
2
of Lemma
es-cut-induction
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. P : Cut(X;f) ─→ ℙ
6. (∃R:E(X) ─→ E(X) ─→ ℙ. (Linorder(E(X);x,y.R[x;y]) ∧ (∀x,y:E(X). Dec(R[x;y])))) ∨ (∀c:Cut(X;f). SqStable(P[c]))@i'
7. P[{}]@i
8. c : Cut(X;f)@i
9. e : E(X)@i
10. P[c]@i
11. (¬((f e) = e ∈ E(X))) ⇒ f e ∈ c@i
12. ¬e ∈ c
13. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
14. c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
15. ∀[i:Id]. c+e(i) = c(i) ∈ ({e:E(X)| loc(e) = i ∈ Id} List) supposing ¬(i = loc(e) ∈ Id)
16. ¬e ∈ c
17. e ∈ c+e
18. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
19. c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
20. ↑e ∈b prior(X)@i
21. prior(X)(e) ∈ c
22. prior(X)(e) ∈ c@i
⊢ c(loc(e)) = ≤(X)(prior(X)(e)) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
BY
{ Assert ⌈(c(loc(e)) @ [e]) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)⌉⋅ }
1
.....assertion.....
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. P : Cut(X;f) ─→ ℙ
6. (∃R:E(X) ─→ E(X) ─→ ℙ. (Linorder(E(X);x,y.R[x;y]) ∧ (∀x,y:E(X). Dec(R[x;y])))) ∨ (∀c:Cut(X;f). SqStable(P[c]))@i'
7. P[{}]@i
8. c : Cut(X;f)@i
9. e : E(X)@i
10. P[c]@i
11. (¬((f e) = e ∈ E(X))) ⇒ f e ∈ c@i
12. ¬e ∈ c
13. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
14. c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
15. ∀[i:Id]. c+e(i) = c(i) ∈ ({e:E(X)| loc(e) = i ∈ Id} List) supposing ¬(i = loc(e) ∈ Id)
16. ¬e ∈ c
17. e ∈ c+e
18. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
19. c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
20. ↑e ∈b prior(X)@i
21. prior(X)(e) ∈ c
22. prior(X)(e) ∈ c@i
⊢ (c(loc(e)) @ [e]) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
2
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. P : Cut(X;f) ─→ ℙ
6. (∃R:E(X) ─→ E(X) ─→ ℙ. (Linorder(E(X);x,y.R[x;y]) ∧ (∀x,y:E(X). Dec(R[x;y])))) ∨ (∀c:Cut(X;f). SqStable(P[c]))@i'
7. P[{}]@i
8. c : Cut(X;f)@i
9. e : E(X)@i
10. P[c]@i
11. (¬((f e) = e ∈ E(X))) ⇒ f e ∈ c@i
12. ¬e ∈ c
13. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
14. c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
15. ∀[i:Id]. c+e(i) = c(i) ∈ ({e:E(X)| loc(e) = i ∈ Id} List) supposing ¬(i = loc(e) ∈ Id)
16. ¬e ∈ c
17. e ∈ c+e
18. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
19. c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
20. ↑e ∈b prior(X)@i
21. prior(X)(e) ∈ c
22. prior(X)(e) ∈ c@i
23. (c(loc(e)) @ [e]) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
⊢ c(loc(e)) = ≤(X)(prior(X)(e)) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id} List)
Latex:
Latex:
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. P : Cut(X;f) {}\mrightarrow{} \mBbbP{}
6. (\mexists{}R:E(X) {}\mrightarrow{} E(X) {}\mrightarrow{} \mBbbP{}. (Linorder(E(X);x,y.R[x;y]) \mwedge{} (\mforall{}x,y:E(X). Dec(R[x;y]))))
\mvee{} (\mforall{}c:Cut(X;f). SqStable(P[c]))@i'
7. P[\{\}]@i
8. c : Cut(X;f)@i
9. e : E(X)@i
10. P[c]@i
11. (\mneg{}((f e) = e)) {}\mRightarrow{} f e \mmember{} c@i
12. \mneg{}e \mmember{} c
13. c+e(loc(e)) = (c(loc(e)) @ [e])
14. c+e(loc(e)) = \mleq{}(X)(e)
15. \mforall{}[i:Id]. c+e(i) = c(i) supposing \mneg{}(i = loc(e))
16. \mneg{}e \mmember{} c
17. e \mmember{} c+e
18. c+e(loc(e)) = (c(loc(e)) @ [e])
19. c+e(loc(e)) = \mleq{}(X)(e)
20. \muparrow{}e \mmember{}\msubb{} prior(X)@i
21. prior(X)(e) \mmember{} c
22. prior(X)(e) \mmember{} c@i
\mvdash{} c(loc(e)) = \mleq{}(X)(prior(X)(e))
By
Latex:
Assert \mkleeneopen{}(c(loc(e)) @ [e]) = \mleq{}(X)(e)\mkleeneclose{}\mcdot{}
Home
Index