Step
*
1
2
1
of Lemma
is-rec-class
1. [Info] : Type
2. [T] : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)@i'
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)} ─→ bag(T)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. X : EClass(T)@i'
8. B : bag(E(X))@i
9. (prior(X) es e) = B ∈ bag(E(X))@i
10. #(B) = 1 ∈ ℤ
11. ↑e ∈b prior(X)
⊢ ↑(#(F[es;prior(X)(e);X(prior(X)(e));e]) =z 1)
⇐⇒ #(F[es;prior(X)(e);X(prior(X)(e));e]) = 1 ∈ ℤ
BY
{ (FLemma `es-prior-interface-val` [-1] THENA Auto) }
1
1. [Info] : Type
2. [T] : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)@i'
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)} ─→ bag(T)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. X : EClass(T)@i'
8. B : bag(E(X))@i
9. (prior(X) es e) = B ∈ bag(E(X))@i
10. #(B) = 1 ∈ ℤ
11. ↑e ∈b prior(X)
12. (prior(X)(e) <loc e)
⊢ ↑(#(F[es;prior(X)(e);X(prior(X)(e));e]) =z 1)
⇐⇒ #(F[es;prior(X)(e);X(prior(X)(e));e]) = 1 ∈ ℤ
Latex:
Latex:
1. [Info] : Type
2. [T] : Type
3. G : es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} bag(T)@i'
4. F : es:EO+(Info) {}\mrightarrow{} e':E {}\mrightarrow{} T {}\mrightarrow{} \{e:E| (e' <loc e)\} {}\mrightarrow{} bag(T)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. X : EClass(T)@i'
8. B : bag(E(X))@i
9. (prior(X) es e) = B@i
10. \#(B) = 1
11. \muparrow{}e \mmember{}\msubb{} prior(X)
\mvdash{} \muparrow{}(\#(F[es;prior(X)(e);X(prior(X)(e));e]) =\msubz{} 1) \mLeftarrow{}{}\mRightarrow{} \#(F[es;prior(X)(e);X(prior(X)(e));e]) = 1
By
Latex:
(FLemma `es-prior-interface-val` [-1] THENA Auto)
Home
Index