Step
*
of Lemma
primed-classrel-opt
∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[b:Id ─→ bag(T)]. ∀[es:EO+(Info)]. ∀[v:T]. ∀[e:E].
uiff(v ∈ Prior(X)?b(e);↓∃e'<e.v ∈ X(e') ∧ ∀e''<e.∀w:T. (w ∈ X(e'')
⇒ e'' ≤loc e' )
∨ (v ↓∈ b loc(e) ∧ ∀e'<e.∀w:T. (¬w ∈ X(e'))))
BY
{ (Auto
THEN Try ((Unhide THEN Auto))
THEN (MoveToConcl (-1)
THEN RepUR ``classrel primed-class-opt`` 0
THEN ((GenConclAtAddr[2;3;1] THENA Auto) ORELSE (GenConclAtAddr[1;3;1] THENA Auto))
THEN (Reduce (-2) THEN D -2 THEN Reduce 0 THEN Auto)⋅)⋅) }
1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. b : Id ─→ bag(T)
5. es : EO+(Info)
6. v : T
7. e : E
8. x : ∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')) ∧ (∀e'':E. ((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑0 <z #(X es e'')))))}@i
9. (last(λe'.0 <z #(X es e')) e)
= (inl x)
∈ ((∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(X es e')) e'))
∧ (∀e'':E. ((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑((λe'.0 <z #(X es e')) e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(X es e')) e')))})))@i
10. v ↓∈ X es x@i
⊢ ↓∃e'<e.v ↓∈ X es e' ∧ ∀e''<e.∀w:T. (w ↓∈ X es e''
⇒ e'' ≤loc e' ) ∨ (v ↓∈ b loc(e) ∧ ∀e'<e.∀w:T. (¬w ↓∈ X es e'))
2
1. Info : Type
2. T : Type
3. X : EClass(T)
4. b : Id ─→ bag(T)
5. es : EO+(Info)
6. v : T
7. e : E
8. y : ¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')))})@i
9. (last(λe'.0 <z #(X es e')) e)
= (inr y )
∈ ((∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(X es e')) e'))
∧ (∀e'':E. ((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑((λe'.0 <z #(X es e')) e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(X es e')) e')))})))@i
10. v ↓∈ b loc(e)@i
⊢ ↓∃e'<e.v ↓∈ X es e' ∧ ∀e''<e.∀w:T. (w ↓∈ X es e''
⇒ e'' ≤loc e' ) ∨ (v ↓∈ b loc(e) ∧ ∀e'<e.∀w:T. (¬w ↓∈ X es e'))
3
1. Info : Type
2. T : Type
3. X : EClass(T)
4. b : Id ─→ bag(T)
5. es : EO+(Info)
6. v : T
7. e : E
8. x : ∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')) ∧ (∀e'':E. ((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑0 <z #(X es e'')))))}@i
9. (last(λe'.0 <z #(X es e')) e)
= (inl x)
∈ ((∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(X es e')) e'))
∧ (∀e'':E. ((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑((λe'.0 <z #(X es e')) e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(X es e')) e')))})))@i
10. ↓∃e'<e.v ↓∈ X es e' ∧ ∀e''<e.∀w:T. (w ↓∈ X es e''
⇒ e'' ≤loc e' ) ∨ (v ↓∈ b loc(e) ∧ ∀e'<e.∀w:T. (¬w ↓∈ X es e'))@i
⊢ v ↓∈ X es x
4
1. Info : Type
2. T : Type
3. X : EClass(T)
4. b : Id ─→ bag(T)
5. es : EO+(Info)
6. v : T
7. e : E
8. y : ¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')))})@i
9. (last(λe'.0 <z #(X es e')) e)
= (inr y )
∈ ((∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(X es e')) e'))
∧ (∀e'':E. ((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑((λe'.0 <z #(X es e')) e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(X es e')) e')))})))@i
10. ↓∃e'<e.v ↓∈ X es e' ∧ ∀e''<e.∀w:T. (w ↓∈ X es e''
⇒ e'' ≤loc e' ) ∨ (v ↓∈ b loc(e) ∧ ∀e'<e.∀w:T. (¬w ↓∈ X es e'))@i
⊢ v ↓∈ b loc(e)
Latex:
Latex:
\mforall{}[Info,T:Type]. \mforall{}[X:EClass(T)]. \mforall{}[b:Id {}\mrightarrow{} bag(T)]. \mforall{}[es:EO+(Info)]. \mforall{}[v:T]. \mforall{}[e:E].
uiff(v \mmember{} Prior(X)?b(e);\mdownarrow{}\mexists{}e'<e.v \mmember{} X(e') \mwedge{} \mforall{}e''<e.\mforall{}w:T. (w \mmember{} X(e'') {}\mRightarrow{} e'' \mleq{}loc e' )
\mvee{} (v \mdownarrow{}\mmember{} b loc(e) \mwedge{} \mforall{}e'<e.\mforall{}w:T. (\mneg{}w \mmember{} X(e'))))
By
Latex:
(Auto
THEN Try ((Unhide THEN Auto))
THEN (MoveToConcl (-1)
THEN RepUR ``classrel primed-class-opt`` 0
THEN ((GenConclAtAddr[2;3;1] THENA Auto) ORELSE (GenConclAtAddr[1;3;1] THENA Auto))
THEN (Reduce (-2) THEN D -2 THEN Reduce 0 THEN Auto)\mcdot{})\mcdot{})
Home
Index