---

Step * 4 1 1 3 2 2 1 3 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
22. (v7 * v4) = (v3 * v8) ∈ ℤ
23. CoPrime(-v3,-v4)
24. CoPrime(-v7,-v8)
⊢ (if 0 ≤z v8 then v7 else -v7 fi  * if 0 ≤z v4 then v4 else -v4 fi )
= (if 0 ≤z v4 then v3 else -v3 fi  * if 0 ≤z v8 then v8 else -v8 fi )
∈ ℤ
BY
{ (RepeatFor 2 ((SplitOnConclITE THENA Auto)) THEN Auto) }

---

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{}
22.  (v7  *  v4)  =  (v3  *  v8)
23.  CoPrime(-v3,-v4)
24.  CoPrime(-v7,-v8)
\mvdash{}  (if  0  \mleq{}z  v8  then  v7  else  -v7  fi    *  if  0  \mleq{}z  v4  then  v4  else  -v4  fi  )
=  (if  0  \mleq{}z  v4  then  v3  else  -v3  fi    *  if  0  \mleq{}z  v8  then  v8  else  -v8  fi  )


By

---

Latex:
(RepeatFor  2  ((SplitOnConclITE  THENA  Auto))  THEN  Auto)

---

Home Index