Step
*
of Lemma
bor_mon_wf
<𝔹,∨b> ∈ AbMon
BY
{ (Unfold `bor_mon` 0
THEN ((BLemma `mk_abmonoid`) THENA Auto)
THEN D 0
THEN Reduce 0
THEN Auto
THEN AutoBoolCase ⌜x⌝⋅
THEN AutoBoolCase ⌜y⌝⋅) }
Latex:
Latex:
<\mBbbB{},\mvee{}\msubb{}> \mmember{} AbMon
By
Latex:
(Unfold `bor\_mon` 0
THEN ((BLemma `mk\_abmonoid`) THENA Auto)
THEN D 0
THEN Reduce 0
THEN Auto
THEN AutoBoolCase \mkleeneopen{}x\mkleeneclose{}\mcdot{}
THEN AutoBoolCase \mkleeneopen{}y\mkleeneclose{}\mcdot{})
Home
Index