Step
*
1
2
1
1
of Lemma
es-prior-val-equal
.....subterm..... T:t
1:n
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. ∀e':E. ((e' <loc e) ⇒ ((X es e') = (Y es e') ∈ bag(T)))
8. ∀e':E. ((e' <loc e) ⇒ (↑e' ∈b X ⇐⇒ ↑e' ∈b Y))
9. ↑e ∈b prior(X)
10. ↑e ∈b prior(Y)
11. (prior(X)(e) <loc e)
12. ↑prior(X)(e) ∈b X
13. ∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))
14. (prior(Y)(e) <loc e)
15. ↑prior(Y)(e) ∈b Y
16. ∀e'':E. ((e'' <loc e) ⇒ (prior(Y)(e) <loc e'') ⇒ (¬↑e'' ∈b Y))
⊢ X(prior(X)(e)) = Y(prior(Y)(e)) ∈ T
BY
{ (InstLemma `es-locl-total` [⌜es⌝;⌜prior(X)(e)⌝;⌜prior(Y)(e)⌝]⋅ THENA Auto)
THEN SplitOrHyps
THEN Auto⋅ }
1
.....wf.....
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. ∀e':E. ((e' <loc e) ⇒ ((X es e') = (Y es e') ∈ bag(T)))
8. ∀e':E. ((e' <loc e) ⇒ (↑e' ∈b X ⇐⇒ ↑e' ∈b Y))
9. ↑e ∈b prior(X)
10. ↑e ∈b prior(Y)
11. (prior(X)(e) <loc e)
12. ↑prior(X)(e) ∈b X
13. ∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))
14. (prior(Y)(e) <loc e)
15. ↑prior(Y)(e) ∈b Y
16. ∀e'':E. ((e'' <loc e) ⇒ (prior(Y)(e) <loc e'') ⇒ (¬↑e'' ∈b Y))
⊢ prior(X)(e) ∈ E
2
.....wf.....
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. ∀e':E. ((e' <loc e) ⇒ ((X es e') = (Y es e') ∈ bag(T)))
8. ∀e':E. ((e' <loc e) ⇒ (↑e' ∈b X ⇐⇒ ↑e' ∈b Y))
9. ↑e ∈b prior(X)
10. ↑e ∈b prior(Y)
11. (prior(X)(e) <loc e)
12. ↑prior(X)(e) ∈b X
13. ∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))
14. (prior(Y)(e) <loc e)
15. ↑prior(Y)(e) ∈b Y
16. ∀e'':E. ((e'' <loc e) ⇒ (prior(Y)(e) <loc e'') ⇒ (¬↑e'' ∈b Y))
⊢ prior(Y)(e) ∈ E
3
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. ∀e':E. ((e' <loc e) ⇒ ((X es e') = (Y es e') ∈ bag(T)))
8. ∀e':E. ((e' <loc e) ⇒ (↑e' ∈b X ⇐⇒ ↑e' ∈b Y))
9. ↑e ∈b prior(X)
10. ↑e ∈b prior(Y)
11. (prior(X)(e) <loc e)
12. ↑prior(X)(e) ∈b X
13. ∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))
14. (prior(Y)(e) <loc e)
15. ↑prior(Y)(e) ∈b Y
16. ∀e'':E. ((e'' <loc e) ⇒ (prior(Y)(e) <loc e'') ⇒ (¬↑e'' ∈b Y))
17. (prior(X)(e) <loc prior(Y)(e))
⊢ X(prior(X)(e)) = Y(prior(Y)(e)) ∈ T
4
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. ∀e':E. ((e' <loc e) ⇒ ((X es e') = (Y es e') ∈ bag(T)))
8. ∀e':E. ((e' <loc e) ⇒ (↑e' ∈b X ⇐⇒ ↑e' ∈b Y))
9. ↑e ∈b prior(X)
10. ↑e ∈b prior(Y)
11. (prior(X)(e) <loc e)
12. ↑prior(X)(e) ∈b X
13. ∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))
14. (prior(Y)(e) <loc e)
15. ↑prior(Y)(e) ∈b Y
16. ∀e'':E. ((e'' <loc e) ⇒ (prior(Y)(e) <loc e'') ⇒ (¬↑e'' ∈b Y))
17. prior(X)(e) = prior(Y)(e) ∈ E
⊢ X(prior(X)(e)) = Y(prior(Y)(e)) ∈ T
5
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. ∀e':E. ((e' <loc e) ⇒ ((X es e') = (Y es e') ∈ bag(T)))
8. ∀e':E. ((e' <loc e) ⇒ (↑e' ∈b X ⇐⇒ ↑e' ∈b Y))
9. ↑e ∈b prior(X)
10. ↑e ∈b prior(Y)
11. (prior(X)(e) <loc e)
12. ↑prior(X)(e) ∈b X
13. ∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))
14. (prior(Y)(e) <loc e)
15. ↑prior(Y)(e) ∈b Y
16. ∀e'':E. ((e'' <loc e) ⇒ (prior(Y)(e) <loc e'') ⇒ (¬↑e'' ∈b Y))
17. (prior(Y)(e) <loc prior(X)(e))
⊢ X(prior(X)(e)) = Y(prior(Y)(e)) ∈ T
Latex:
Latex:
.....subterm..... T:t
1:n
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. \mforall{}e':E. ((e' <loc e) {}\mRightarrow{} ((X es e') = (Y es e')))
8. \mforall{}e':E. ((e' <loc e) {}\mRightarrow{} (\muparrow{}e' \mmember{}\msubb{} X \mLeftarrow{}{}\mRightarrow{} \muparrow{}e' \mmember{}\msubb{} Y))
9. \muparrow{}e \mmember{}\msubb{} prior(X)
10. \muparrow{}e \mmember{}\msubb{} prior(Y)
11. (prior(X)(e) <loc e)
12. \muparrow{}prior(X)(e) \mmember{}\msubb{} X
13. \mforall{}e'':E. ((e'' <loc e) {}\mRightarrow{} (prior(X)(e) <loc e'') {}\mRightarrow{} (\mneg{}\muparrow{}e'' \mmember{}\msubb{} X))
14. (prior(Y)(e) <loc e)
15. \muparrow{}prior(Y)(e) \mmember{}\msubb{} Y
16. \mforall{}e'':E. ((e'' <loc e) {}\mRightarrow{} (prior(Y)(e) <loc e'') {}\mRightarrow{} (\mneg{}\muparrow{}e'' \mmember{}\msubb{} Y))
\mvdash{} X(prior(X)(e)) = Y(prior(Y)(e))
By
Latex:
(InstLemma `es-locl-total` [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}prior(X)(e)\mkleeneclose{};\mkleeneopen{}prior(Y)(e)\mkleeneclose{}]\mcdot{} THENA Auto)
THEN SplitOrHyps
THEN Auto\mcdot{}
Home
Index