Step
*
4
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) ∈ ℤ
⊢ if 0 ≤z v8 then <v7, v8> else <-v7, -v8> fi = if 0 ≤z v4 then <v3, v4> else <-v3, -v4> fi ∈ (ℤ × ℕ+)
BY
{ ((Assert v8 ∈ ℤ-o BY
(Decide v8 = 0 ∈ ℤ THEN Auto THEN TACTIC:(HypSubst' -1 12 THEN Auto)))
THEN (Assert v4 ∈ ℤ-o BY
(Decide v4 = 0 ∈ ℤ THEN Auto THEN HypSubst' -1 16 THEN Auto))
) }
1
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 ∈ (ℤ × ℕ+)
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)
\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 v8 \mmember{} \mBbbZ{}\msupminus{}\msupzero{} BY
(Decide v8 = 0 THEN Auto THEN TACTIC:(HypSubst' -1 12 THEN Auto)))
THEN (Assert v4 \mmember{} \mBbbZ{}\msupminus{}\msupzero{} BY
(Decide v4 = 0 THEN Auto THEN HypSubst' -1 16 THEN Auto))
)
Home
Index