---

Step * 4 1 1 of Lemma qrep_wf


1. z3 : ℤ
2. z4 : ℤ-o
3. z1 : ℤ
4. z2 : ℤ-o
5. v1 : ℕ
6. v3 : ℤ
7. v4 : ℤ
8. v5 : ℕ
9. v7 : ℤ
10. v8 : ℤ
11. z3 = (v7 * v5) ∈ ℤ
12. z4 = (v8 * v5) ∈ ℤ
13. CoPrime(v7,v8)
14. (z3 * v8) = (v7 * z4) ∈ ℤ
15. z1 = (v3 * v1) ∈ ℤ
16. z2 = (v4 * v1) ∈ ℤ
17. CoPrime(v3,v4)
18. (z1 * v4) = (v3 * z2) ∈ ℤ
19. (z3 * z2) = (z1 * z4) ∈ ℤ
20. v8 ∈ ℤ-o
21. v4 ∈ ℤ-o
⊢ if 0 ≤z v8 then <v7, v8> else <-v7, -v8> fi  = if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi  ∈ (ℤ × ℕ+)
BY
{ (Assert (v7 * v4) = (v3 * v8) ∈ ℤ BY
         (Auto THEN Decide z3 = 0 ∈ ℤ THEN Auto)) }

1
.....aux..... 
1. z3 : ℤ
2. z4 : ℤ-o
3. z1 : ℤ
4. z2 : ℤ-o
5. v1 : ℕ
6. v3 : ℤ
7. v4 : ℤ
8. v5 : ℕ
9. v7 : ℤ
10. v8 : ℤ
11. z3 = (v7 * v5) ∈ ℤ
12. z4 = (v8 * v5) ∈ ℤ
13. CoPrime(v7,v8)
14. (z3 * v8) = (v7 * z4) ∈ ℤ
15. z1 = (v3 * v1) ∈ ℤ
16. z2 = (v4 * v1) ∈ ℤ
17. CoPrime(v3,v4)
18. (z1 * v4) = (v3 * z2) ∈ ℤ
19. (z3 * z2) = (z1 * z4) ∈ ℤ
20. v8 ∈ ℤ-o
21. v4 ∈ ℤ-o
22. z3 = 0 ∈ ℤ
⊢ (v7 * v4) = (v3 * v8) ∈ ℤ

2
.....aux..... 
1. z3 : ℤ
2. z4 : ℤ-o
3. z1 : ℤ
4. z2 : ℤ-o
5. v1 : ℕ
6. v3 : ℤ
7. v4 : ℤ
8. v5 : ℕ
9. v7 : ℤ
10. v8 : ℤ
11. z3 = (v7 * v5) ∈ ℤ
12. z4 = (v8 * v5) ∈ ℤ
13. CoPrime(v7,v8)
14. (z3 * v8) = (v7 * z4) ∈ ℤ
15. z1 = (v3 * v1) ∈ ℤ
16. z2 = (v4 * v1) ∈ ℤ
17. CoPrime(v3,v4)
18. (z1 * v4) = (v3 * z2) ∈ ℤ
19. (z3 * z2) = (z1 * z4) ∈ ℤ
20. v8 ∈ ℤ-o
21. v4 ∈ ℤ-o
22. ¬(z3 = 0 ∈ ℤ)
⊢ (v7 * v4) = (v3 * v8) ∈ ℤ

3
1. z3 : ℤ
2. z4 : ℤ-o
3. z1 : ℤ
4. z2 : ℤ-o
5. v1 : ℕ
6. v3 : ℤ
7. v4 : ℤ
8. v5 : ℕ
9. v7 : ℤ
10. v8 : ℤ
11. z3 = (v7 * v5) ∈ ℤ
12. z4 = (v8 * v5) ∈ ℤ
13. CoPrime(v7,v8)
14. (z3 * v8) = (v7 * z4) ∈ ℤ
15. z1 = (v3 * v1) ∈ ℤ
16. z2 = (v4 * v1) ∈ ℤ
17. CoPrime(v3,v4)
18. (z1 * v4) = (v3 * z2) ∈ ℤ
19. (z3 * z2) = (z1 * z4) ∈ ℤ
20. v8 ∈ ℤ-o
21. v4 ∈ ℤ-o
22. (v7 * v4) = (v3 * v8) ∈ ℤ
⊢ if 0 ≤z v8 then <v7, v8> else <-v7, -v8> fi  = if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi  ∈ (ℤ × ℕ+)

---

Latex:

---

Latex:

1.  z3  :  \mBbbZ{}
2.  z4  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  z1  :  \mBbbZ{}
4.  z2  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  v1  :  \mBbbN{}
6.  v3  :  \mBbbZ{}
7.  v4  :  \mBbbZ{}
8.  v5  :  \mBbbN{}
9.  v7  :  \mBbbZ{}
10.  v8  :  \mBbbZ{}
11.  z3  =  (v7  *  v5)
12.  z4  =  (v8  *  v5)
13.  CoPrime(v7,v8)
14.  (z3  *  v8)  =  (v7  *  z4)
15.  z1  =  (v3  *  v1)
16.  z2  =  (v4  *  v1)
17.  CoPrime(v3,v4)
18.  (z1  *  v4)  =  (v3  *  z2)
19.  (z3  *  z2)  =  (z1  *  z4)
20.  v8  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}
21.  v4  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  if  0  \mleq{}z  v8  then  <v7,  v8>  else  <-v7,  -v8>  fi    =  if  0  \mleq{}z  v4  then  <v3,  v4>  else  <-v3,  -v4>  fi 


By

---

Latex:
(Assert  (v7  *  v4)  =  (v3  *  v8)  BY
              (Auto  THEN  Decide  z3  =  0  THEN  Auto))

---

Home Index