Step
*
of Lemma
testxxx_lemma
∀b:Top. (tt ∨bb ~ tt)
BY
{ ((UnivCD THENA Auto)
THEN RW (AddrC [1] (RepeatC (UnfoldsC ``bor btrue ifthenelse``) ANDTHENC ReduceC⋅)) 0⋅
THEN RW (AddrC [2] (UnfoldC `btrue`⋅⋅)) 0⋅
THEN SqEqCD) }
Latex:
Latex:
\mforall{}b:Top. (tt \mvee{}\msubb{}b \msim{} tt)
By
Latex:
((UnivCD THENA Auto)
THEN RW (AddrC [1] (RepeatC (UnfoldsC ``bor btrue ifthenelse``) ANDTHENC ReduceC\mcdot{})) 0\mcdot{}
THEN RW (AddrC [2] (UnfoldC `btrue`\mcdot{}\mcdot{})) 0\mcdot{}
THEN SqEqCD)
Home
Index