Step * 1 of Lemma normalize-constraints-eq


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

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


Latex:


Latex:

1.  k  :  \mBbbN{}
2.  A  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List
3.  map(\mlambda{}p.normalize-constraint(k;p);A)  =  A
\mvdash{}  normalize-constraints(k;A)  =  A


By


Latex:
(Assert  map(\mlambda{}p.normalize-constraint(k;p);A)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List  BY
              Auto)




Home Index