---

Step * of Lemma gcd-reduce-eq-constraints_wf

∀[LL,sat:ℤ List+ List].  (gcd-reduce-eq-constraints(sat;LL) ∈ ℤ List+ List?)
BY
{ (ProveWfLemma THEN RepeatFor 4 ((CallByValueReduce 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[LL,sat:\mBbbZ{}  List\msupplus{}  List].    (gcd-reduce-eq-constraints(sat;LL)  \mmember{}  \mBbbZ{}  List\msupplus{}  List?)


By

---

Latex:
(ProveWfLemma  THEN  RepeatFor  4  ((CallByValueReduce  0  THEN  Auto)))

---

Home Index