---

Step * of Lemma normalize-constraints-eq

∀[k:ℕ]. ∀[A:(ℕ ⟶ ℚ × ℤ) List].  (normalize-constraints(k;A) = A ∈ ((ℕ ⟶ ℚ × ℤ) List))
BY
{ (Auto
   THEN (Assert map(λp.normalize-constraint(k;p);A) = A ∈ ((ℕ ⟶ ℚ × ℤ) List) BY
               (BLemma `trivial_map` THEN Auto THEN Reduce 0 THEN BLemma `normalize-constraint-eq` THEN Auto))
   ) }

1
1. k : ℕ
2. A : (ℕ ⟶ ℚ × ℤ) List
3. map(λp.normalize-constraint(k;p);A) = A ∈ ((ℕ ⟶ ℚ × ℤ) List)
⊢ normalize-constraints(k;A) = A ∈ ((ℕ ⟶ ℚ × ℤ) List)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  map(\mlambda{}p.normalize-constraint(k;p);A)  =  A  BY
                          (BLemma  `trivial\_map`
                            THEN  Auto
                            THEN  Reduce  0
                            THEN  BLemma  `normalize-constraint-eq`
                            THEN  Auto))
  )

---

Home Index