Step
*
of Lemma
eclass0-disjoint-classrel
∀[Info,A,B,C:Type]. ∀[Y:EClass(A)]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ bag(C)]. ∀[es:EO+(Info)].
(disjoint-classrel(es;B;X;A;Y)
⇒ disjoint-classrel(es;C;(f o X);A;Y))
BY
{ ((At ⌈𝕌'⌉ Intros⋅ THEN Auto)
THEN All(Unfold `disjoint-classrel`)
THEN Auto
THEN (InstHyp [⌈e⌉] (-2)⋅ THENA Auto)
THEN D (-1)
THEN Try (Complete ((OrRight THEN Auto)))
THEN OrLeft
THEN Auto
THEN (D 0 THENA Auto)
THEN MaUseClassRel (-1)⋅
THEN (Assert ¬b ∈ X(e) BY
Auto)
THEN Auto) }
Latex:
\mforall{}[Info,A,B,C:Type]. \mforall{}[Y:EClass(A)]. \mforall{}[X:EClass(B)]. \mforall{}[f:Id {}\mrightarrow{} B {}\mrightarrow{} bag(C)]. \mforall{}[es:EO+(Info)].
(disjoint-classrel(es;B;X;A;Y) {}\mRightarrow{} disjoint-classrel(es;C;(f o X);A;Y))
By
((At \mkleeneopen{}\mBbbU{}'\mkleeneclose{} Intros\mcdot{} THEN Auto)
THEN All(Unfold `disjoint-classrel`)
THEN Auto
THEN (InstHyp [\mkleeneopen{}e\mkleeneclose{}] (-2)\mcdot{} THENA Auto)
THEN D (-1)
THEN Try (Complete ((OrRight THEN Auto)))
THEN OrLeft
THEN Auto
THEN (D 0 THENA Auto)
THEN MaUseClassRel (-1)\mcdot{}
THEN (Assert \mneg{}b \mmember{} X(e) BY
Auto)
THEN Auto)
Home
Index