Step
*
1
of Lemma
prior-as-rec-bind-class-in-property
1. Info : Type
2. A : Type
3. X : EClass(A)
4. x : bag(A)
5. a : bag(A) + (bag(A)?)
6. es : EO+(Info)
7. e : E
8. a ↓∈ ∪x1∈(Skip(send-class({x})) until Skip(X)) es e.{inl x1}
9. w : bag(A) + (bag(A)?)
10. e ∈ E
11. w ∈ prior-as-rec-bind-class-in(X;a)(e)@i
⊢ (Skip(send-class({x})) until Skip(X)) es e ∈ bag(bag(A))
BY
{ (GenConclAtAddr [2;1;1] THEN Auto)⋅ }
Latex:
Latex:
1. Info : Type
2. A : Type
3. X : EClass(A)
4. x : bag(A)
5. a : bag(A) + (bag(A)?)
6. es : EO+(Info)
7. e : E
8. a \mdownarrow{}\mmember{} \mcup{}x1\mmember{}(Skip(send-class(\{x\})) until Skip(X)) es e.\{inl x1\}
9. w : bag(A) + (bag(A)?)
10. e \mmember{} E
11. w \mmember{} prior-as-rec-bind-class-in(X;a)(e)@i
\mvdash{} (Skip(send-class(\{x\})) until Skip(X)) es e \mmember{} bag(bag(A))
By
Latex:
(GenConclAtAddr [2;1;1] THEN Auto)\mcdot{}
Home
Index