---

Step * of Lemma gcd-reduce-ineq-constraints_wf

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

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))  THEN  Auto)

---

Home Index