---

Step * 2 1 of Lemma gcd-list-property


1. u : ℤ
2. v : ℤ List
⊢ (∃R:ℤ List
    ([u / v]
    = accumulate (with value a and list item b):
       better-gcd(a;b)
      over list:
        v
      with starting value:
       u) * R
    ∈ (ℤ List)))
∧ (∃S:ℤ List
    ((||S|| = (||v|| + 1) ∈ ℤ)
    ∧ (accumulate (with value a and list item b):
        better-gcd(a;b)
       over list:
         v
       with starting value:
        u)
      = S ⋅ [u / v]
      ∈ ℤ)))
BY
{ ((MoveToConcl 1 THEN ListInd 1) THEN Reduce 0) }

1
∀u:ℤ. ((∃R:ℤ List. ([u] = u * R ∈ (ℤ List))) ∧ (∃S:ℤ List. ((||S|| = 1 ∈ ℤ) ∧ (u = S ⋅ [u] ∈ ℤ))))

2
1. u : ℤ
2. v : ℤ List
3. ∀u:ℤ
     ((∃R:ℤ List
        ([u / v]
        = accumulate (with value a and list item b):
           better-gcd(a;b)
          over list:
            v
          with starting value:
           u) * R
        ∈ (ℤ List)))
     ∧ (∃S:ℤ List
         ((||S|| = (||v|| + 1) ∈ ℤ)
         ∧ (accumulate (with value a and list item b):
             better-gcd(a;b)
            over list:
              v
            with starting value:
             u)
           = S ⋅ [u / v]
           ∈ ℤ))))
⊢ ∀u@0:ℤ
    ((∃R:ℤ List
       ([u@0; [u / v]]
       = accumulate (with value a and list item b):
          better-gcd(a;b)
         over list:
           v
         with starting value:
          better-gcd(u@0;u)) * R
       ∈ (ℤ List)))
    ∧ (∃S:ℤ List
        ((||S|| = ((||v|| + 1) + 1) ∈ ℤ)
        ∧ (accumulate (with value a and list item b):
            better-gcd(a;b)
           over list:
             v
           with starting value:
            better-gcd(u@0;u))
          = S ⋅ [u@0; [u / v]]
          ∈ ℤ))))

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
\mvdash{}  (\mexists{}R:\mBbbZ{}  List
        ([u  /  v]
        =  accumulate  (with  value  a  and  list  item  b):
              better-gcd(a;b)
            over  list:
                v
            with  starting  value:
              u)  *  R))
\mwedge{}  (\mexists{}S:\mBbbZ{}  List
        ((||S||  =  (||v||  +  1))
        \mwedge{}  (accumulate  (with  value  a  and  list  item  b):
                better-gcd(a;b)
              over  list:
                  v
              with  starting  value:
                u)
            =  S  \mcdot{}  [u  /  v])))


By

---

Latex:
((MoveToConcl  1  THEN  ListInd  1)  THEN  Reduce  0)

---

Home Index