---

Step * of Lemma normalize-constraint-eq

∀[k:ℕ]. ∀[A:ℕ ⟶ ℚ × ℤ].  (normalize-constraint(k;A) = A ∈ (ℕ ⟶ ℚ × ℤ))
BY
{ xxx(UnivCD THENA Auto)xxx }

1
1. k : ℕ
2. A : ℕ ⟶ ℚ × ℤ
⊢ normalize-constraint(k;A) = A ∈ (ℕ ⟶ ℚ × ℤ)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[A:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{}].    (normalize-constraint(k;A)  =  A)


By

---

Latex:
xxx(UnivCD  THENA  Auto)xxx

---

Home Index