Step
*
1
of Lemma
class-opt-class-classrel
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. v : T
6. es : EO+(Info)
7. e : E
8. v ∈ X?Y(e)
⊢ ↓((↑bag-null(X es e)) ∧ v ∈ Y(e)) ∨ ((¬↑bag-null(X es e)) ∧ v ∈ X(e))
BY
{ (RepUR ``class-opt-class classrel`` (-1) THEN BagMemberD (-1) THEN D 0 THEN Try (Fold `classrel` (-1)⋅)⋅) }
1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. v : T
6. es : EO+(Info)
7. e : E
8. (X es e) = {} ∈ bag(T)
9. v ∈ Y(e)
⊢ ((↑bag-null(X es e)) ∧ v ∈ Y(e)) ∨ ((¬↑bag-null(X es e)) ∧ v ∈ X(e))
2
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. v : T
6. es : EO+(Info)
7. e : E
8. ¬((X es e) = {} ∈ bag(T))
9. v ∈ X(e)
⊢ ((↑bag-null(X es e)) ∧ v ∈ Y(e)) ∨ ((¬↑bag-null(X es e)) ∧ v ∈ X(e))
Latex:
Latex:
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. v : T
6. es : EO+(Info)
7. e : E
8. v \mmember{} X?Y(e)
\mvdash{} \mdownarrow{}((\muparrow{}bag-null(X es e)) \mwedge{} v \mmember{} Y(e)) \mvee{} ((\mneg{}\muparrow{}bag-null(X es e)) \mwedge{} v \mmember{} X(e))
By
Latex:
(RepUR ``class-opt-class classrel`` (-1)
THEN BagMemberD (-1)
THEN D 0
THEN Try (Fold `classrel` (-1)\mcdot{})\mcdot{})
Home
Index