Step
*
of Lemma
es-local-le-pred_wf
∀[Info:Type]. ∀[P:es:EO+(Info) ─→ E ─→ 𝔹]. (≤(P) ∈ EClass({e:E| ↑(P es e)} ))
BY
{ (Auto THEN Assert ⌈∀es:EO+(Info). ∀e:E. (≤(P) es e ∈ bag({e:E| ↑(P es e)} ))⌉⋅)⋅ }
1
.....assertion.....
1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ 𝔹
⊢ ∀es:EO+(Info). ∀e:E. (≤(P) es e ∈ bag({e:E| ↑(P es e)} ))
2
1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ 𝔹
3. ∀es:EO+(Info). ∀e:E. (≤(P) es e ∈ bag({e:E| ↑(P es e)} ))
⊢ ≤(P) ∈ EClass({e:E| ↑(P es e)} )
Latex:
Latex:
\mforall{}[Info:Type]. \mforall{}[P:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbB{}]. (\mleq{}(P) \mmember{} EClass(\{e:E| \muparrow{}(P es e)\} ))
By
Latex:
(Auto THEN Assert \mkleeneopen{}\mforall{}es:EO+(Info). \mforall{}e:E. (\mleq{}(P) es e \mmember{} bag(\{e:E| \muparrow{}(P es e)\} ))\mkleeneclose{}\mcdot{})\mcdot{}
Home
Index