---

Step * 1 2 1 of Lemma rep_int_constraint_step_wf


1. f : IntConstraints ⟶ IntConstraints
2. p : IntConstraints
3. ∀p:IntConstraints
     (0 < dim(p) ⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))
4. n : ℤ
5. 0 < n
6. ∀p:IntConstraints. (dim(p) < n - 1 ⇒ (rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} ))
7. p1 : IntConstraints
8. dim(p1) < n
9. m : ℤ
10. 0 < m
11. ∀p:IntConstraints
      (dim(p) < n
      ⇒ num-eq-constraints(p) < m - 1
      ⇒ (rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} ))
12. p2 : IntConstraints
13. dim(p2) < n
14. num-eq-constraints(p2) < m
⊢ rep_int_constraint_step(f;p2) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} 
BY
{ (RecUnfold `rep_int_constraint_step` 0 THEN AutoSplit) }

1
1. f : IntConstraints ⟶ IntConstraints
2. p : IntConstraints
3. ∀p:IntConstraints
     (0 < dim(p) ⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))
4. n : ℤ
5. 0 < n
6. ∀p:IntConstraints. (dim(p) < n - 1 ⇒ (rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} ))
7. p1 : IntConstraints
8. dim(p1) < n
9. m : ℤ
10. 0 < m
11. ∀p:IntConstraints
      (dim(p) < n
      ⇒ num-eq-constraints(p) < m - 1
      ⇒ (rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} ))
12. p2 : IntConstraints
13. dim(p2) < n
14. num-eq-constraints(p2) < m
15. 0 < dim(p2)
⊢ let p' ⟵ f p2
  in rep_int_constraint_step(f;p') ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} 

2
1. f : IntConstraints ⟶ IntConstraints
2. p : IntConstraints
3. ∀p:IntConstraints
     (0 < dim(p) ⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))
4. n : ℤ
5. 0 < n
6. ∀p:IntConstraints. (dim(p) < n - 1 ⇒ (rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} ))
7. p1 : IntConstraints
8. dim(p1) < n
9. m : ℤ
10. 0 < m
11. ∀p:IntConstraints
      (dim(p) < n
      ⇒ num-eq-constraints(p) < m - 1
      ⇒ (rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} ))
12. p2 : IntConstraints
13. ¬0 < dim(p2)
14. dim(p2) < n
15. num-eq-constraints(p2) < m
⊢ p2 ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} 

---

Latex:

---

Latex:

1.  f  :  IntConstraints  {}\mrightarrow{}  IntConstraints
2.  p  :  IntConstraints
3.  \mforall{}p:IntConstraints
          (0  <  dim(p)
          {}\mRightarrow{}  (dim(f  p)  <  dim(p)
                \mvee{}  ((dim(f  p)  =  dim(p))  \mwedge{}  num-eq-constraints(f  p)  <  num-eq-constraints(p))))
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  \mforall{}p:IntConstraints
          (dim(p)  <  n  -  1  {}\mRightarrow{}  (rep\_int\_constraint\_step(f;p)  \mmember{}  \{p:IntConstraints|  dim(p)  =  0\}  ))
7.  p1  :  IntConstraints
8.  dim(p1)  <  n
9.  m  :  \mBbbZ{}
10.  0  <  m
11.  \mforall{}p:IntConstraints
            (dim(p)  <  n
            {}\mRightarrow{}  num-eq-constraints(p)  <  m  -  1
            {}\mRightarrow{}  (rep\_int\_constraint\_step(f;p)  \mmember{}  \{p:IntConstraints|  dim(p)  =  0\}  ))
12.  p2  :  IntConstraints
13.  dim(p2)  <  n
14.  num-eq-constraints(p2)  <  m
\mvdash{}  rep\_int\_constraint\_step(f;p2)  \mmember{}  \{p:IntConstraints|  dim(p)  =  0\} 


By

---

Latex:
(RecUnfold  `rep\_int\_constraint\_step`  0  THEN  AutoSplit)

---

Home Index