---

Step * of Lemma itermAdd_functionality_wrt_req

∀[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 ``real_term_value`` 0 THEN Fold `real_term_value` 0)
   THEN Auto
   THEN RWO "-1 -2" 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  ``real\_term\_value``  0  THEN  Fold  `real\_term\_value`  0)
  THEN  Auto
  THEN  RWO  "-1  -2"  0
  THEN  Auto)

---

Home Index