---

Step * of Lemma satisfies-int-constraint-problem_wf

∀[p:IntConstraints]. ∀[xs:ℤ List].  (xs |= p ∈ ℙ)
BY
{ (Auto THEN D 1) }

1
1. x : ⋃n:ℕ.({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List × ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List))
2. xs : ℤ List
⊢ xs |= inl x ∈ ℙ

2
1. y : Unit
2. xs : ℤ List
⊢ xs |= inr y  ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[p:IntConstraints].  \mforall{}[xs:\mBbbZ{}  List].    (xs  |=  p  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  D  1)

---

Home Index