Step
*
of Lemma
classfun-res-disjoint-union-comb-right
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].
(X (+) Y@e = (inr Y@e ) ∈ (A + B)) supposing
(single-valued-classrel(es;Y;B) and
disjoint-classrel(es;A;X;B;Y) and
(↑e ∈b Y))
BY
{ ((UnivCD THENA Auto)
THEN RepUR ``disjoint-union-comb`` 0
THEN (InstLemma `classfun-res-parallel-class-right` [⌈Info⌉;⌈A + B⌉;⌈es⌉;⌈lifting-1(λx.(inl x))|X|⌉;
⌈lifting-1(λx.(inr x ))|Y|⌉;⌈e⌉]⋅
THENA Auto
)
THEN Try (Complete (DisjointClassRel))) }
1
.....antecedent.....
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. X : EClass(A)
6. Y : EClass(B)
7. e : E
8. ↑e ∈b Y
9. disjoint-classrel(es;A;X;B;Y)
10. single-valued-classrel(es;Y;B)
⊢ ↑e ∈b lifting-1(λx.(inr x ))|Y|
2
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. X : EClass(A)
6. Y : EClass(B)
7. e : E
8. ↑e ∈b Y
9. disjoint-classrel(es;A;X;B;Y)
10. single-valued-classrel(es;Y;B)
11. lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e ~ lifting-1(λx.(inr x ))|Y|@e
⊢ lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e = (inr Y@e ) ∈ (A + B)
Latex:
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. \mforall{}[e:E].
(X (+) Y@e = (inr Y@e )) supposing
(single-valued-classrel(es;Y;B) and
disjoint-classrel(es;A;X;B;Y) and
(\muparrow{}e \mmember{}\msubb{} Y))
By
Latex:
((UnivCD THENA Auto)
THEN RepUR ``disjoint-union-comb`` 0
THEN (InstLemma `classfun-res-parallel-class-right` [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A + B\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}lifting-1(\mlambda{}x.(inl x))|X|\mkleeneclose{}
;\mkleeneopen{}lifting-1(\mlambda{}x.(inr x ))|Y|\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN Try (Complete (DisjointClassRel)))
Home
Index