Step
*
1
of Lemma
normalize-constraints-eq
1. k : ℕ
2. A : (ℕ ⟶ ℚ × ℤ) 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. k : ℕ
2. A : (ℕ ⟶ ℚ × ℤ) 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