Step
*
of Lemma
ndiff_ndiff
∀[a,b:ℤ]. ∀[c:ℕ]. (((a -- b) -- c) = (a -- (b + c)) ∈ ℤ)
BY
{ (RepUR ``ndiff imax`` 0
THEN (UnivCD THENA Auto)
THEN Repeat (CallByValueReduce 0)
THEN Auto
THEN Repeat (AutoSplit)
THEN Auto') }
Latex:
Latex:
\mforall{}[a,b:\mBbbZ{}]. \mforall{}[c:\mBbbN{}]. (((a -- b) -- c) = (a -- (b + c)))
By
Latex:
(RepUR ``ndiff imax`` 0
THEN (UnivCD THENA Auto)
THEN Repeat (CallByValueReduce 0)
THEN Auto
THEN Repeat (AutoSplit)
THEN Auto')
Home
Index