---

Step * 1 of Lemma satisfies-int-constraint-problem_wf


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

---

Latex:

---

Latex:

1.  x  :  \mcup{}n:\mBbbN{}.(\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List  \mtimes{}  (\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List))
2.  xs  :  \mBbbZ{}  List
\mvdash{}  xs  |=  inl  x  \mmember{}  \mBbbP{}


By

---

Latex:
((D\_union  1  THEN  D  2)  THEN  ProveWfLemma)

---

Home Index