Step
*
2
1
1
of Lemma
assert-is-qrep
1. v1 : ℤ
2. v2 : ℕ+
⊢ (|gcd(v1;v2)| = 1 ∈ ℤ)
⇒ (↑eval g = better-gcd(v1;v2) in (g =z 1) ∨b(g =z -1))
BY
{ ((RWO "better-gcd-gcd" 0 THEN Auto) THEN (CallByValueReduce 0 THENA Auto) THEN RW assert_pushdownC 0 THEN Auto) }
1
1. v1 : ℤ
2. v2 : ℕ+
3. |gcd(v1;v2)| = 1 ∈ ℤ
⊢ (gcd(v1;v2) = 1 ∈ ℤ) ∨ (gcd(v1;v2) = (-1) ∈ ℤ)
Latex:
Latex:
1. v1 : \mBbbZ{}
2. v2 : \mBbbN{}\msupplus{}
\mvdash{} (|gcd(v1;v2)| = 1) {}\mRightarrow{} (\muparrow{}eval g = better-gcd(v1;v2) in (g =\msubz{} 1) \mvee{}\msubb{}(g =\msubz{} -1))
By
Latex:
((RWO "better-gcd-gcd" 0 THEN Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN RW assert\_pushdownC 0
THEN Auto)
Home
Index