Step * 1 of Lemma sbdecode_wf_gcd


1. : ℕList
2. v1 : ℕ+
3. v2 : ℕ+
4. sbdecode(L) = <v1, v2> ∈ (ℕ+ × ℕ+)
5. sbcode(v1;v2) ∈ (ℕList)
⊢ gcd(v1;v2) 1 ∈ ℤ
BY
xxx(HypSubst' (-1) (-2) THEN (RWO "sbdecode-code" (-2) THENA Auto) THEN EqHD (-2) THEN Auto THEN All Reduce)xxx }

1
1. : ℕList
2. v1 : ℕ+
3. v2 : ℕ+
4. (v1 ÷ gcd(v1;v2)) v1 ∈ ℕ+
5. (v2 ÷ gcd(v1;v2)) v2 ∈ ℕ+
6. sbcode(v1;v2) ∈ (ℕList)
⊢ gcd(v1;v2) 1 ∈ ℤ


Latex:


Latex:

1.  L  :  \mBbbN{}2  List
2.  v1  :  \mBbbN{}\msupplus{}
3.  v2  :  \mBbbN{}\msupplus{}
4.  sbdecode(L)  =  <v1,  v2>
5.  L  =  sbcode(v1;v2)
\mvdash{}  gcd(v1;v2)  =  1


By


Latex:
xxx(HypSubst'  (-1)  (-2)
        THEN  (RWO  "sbdecode-code"  (-2)  THENA  Auto)
        THEN  EqHD  (-2)
        THEN  Auto
        THEN  All  Reduce)xxx




Home Index