---

Step * 1 1 of Lemma gcd_subtract


1. a : ℕ
2. b : ℕ
3. b ≤ a
4. y : ℤ
5. GCD(a - b;b;y)
6. gcd(a - b;b) = y ∈ ℤ
7. ∀y1,y2:ℤ.  (GCD(a;b;y1) ⇒ GCD(a;b;y2) ⇒ (y1 ~ y2))
⊢ GCD(a;b;y)
BY
{ TACTIC:((FLemma `gcd_p_sym` [-3] THENA Auto)
          THEN (InstLemma `gcd_p_shift` [⌜b⌝;⌜a - b⌝;⌜y⌝;⌜1⌝]⋅ THENA Auto)
          THEN FLemma `gcd_p_sym` [-1]
          THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  b  \mleq{}  a
4.  y  :  \mBbbZ{}
5.  GCD(a  -  b;b;y)
6.  gcd(a  -  b;b)  =  y
7.  \mforall{}y1,y2:\mBbbZ{}.    (GCD(a;b;y1)  {}\mRightarrow{}  GCD(a;b;y2)  {}\mRightarrow{}  (y1  \msim{}  y2))
\mvdash{}  GCD(a;b;y)


By

---

Latex:
TACTIC:((FLemma  `gcd\_p\_sym`  [-3]  THENA  Auto)
                THEN  (InstLemma  `gcd\_p\_shift`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a  -  b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  FLemma  `gcd\_p\_sym`  [-1]
                THEN  Auto)

---

Home Index