Step
*
of Lemma
itermAdd_functionality
∀[a,b,c,d:int_term()]. (a "+" c ≡ b "+" d) supposing (a ≡ b and c ≡ d)
BY
{ (Auto
THEN RepeatFor 2 (ParallelLast)
THEN (With ⌜f⌝ (D 5)⋅ THENA Auto)
THEN (RepUR ``int_term_value`` 0 THEN Fold `int_term_value` 0)
THEN Auto) }
Latex:
Latex:
\mforall{}[a,b,c,d:int\_term()]. (a "+" c \mequiv{} b "+" d) supposing (a \mequiv{} b and c \mequiv{} d)
By
Latex:
(Auto
THEN RepeatFor 2 (ParallelLast)
THEN (With \mkleeneopen{}f\mkleeneclose{} (D 5)\mcdot{} THENA Auto)
THEN (RepUR ``int\_term\_value`` 0 THEN Fold `int\_term\_value` 0)
THEN Auto)
Home
Index