Step
*
2
1
2
of Lemma
gcd-list-property
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]]
          ∈ ℤ))))
BY
{ ((D 0 THENA Auto)
   THEN RenameVar `a' (-1)
   THEN (InstHyp [⌜better-gcd(a;u)⌝] 3⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜accumulate (with value a and list item b):
                        better-gcd(a;b)
                       over list:
                         v
                       with starting value:
                        better-gcd(a;u))⌝⋅
         THENA Auto
         )
   THEN (Thin (-1) THEN RenameVar `x' (-1) THEN Thin 3)
   THEN (InstLemma `better-gcd-properties` [⌜a⌝;⌜u⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN Auto) }
1
1. u : ℤ
2. v : ℤ List
3. a : ℤ
4. x : ℤ
5. c : ℤ
6. (c * better-gcd(a;u)) = a ∈ ℤ
7. d : ℤ
8. (d * better-gcd(a;u)) = u ∈ ℤ
9. s : ℤ
10. t : ℤ
11. better-gcd(a;u) = ((s * a) + (t * u)) ∈ ℤ
12. R : ℤ List
13. [better-gcd(a;u) / v] = x * R ∈ (ℤ List)
14. S : ℤ List
15. ||S|| = (||v|| + 1) ∈ ℤ
16. x = S ⋅ [better-gcd(a;u) / v] ∈ ℤ
⊢ ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))
2
1. u : ℤ
2. v : ℤ List
3. a : ℤ
4. x : ℤ
5. c : ℤ
6. (c * better-gcd(a;u)) = a ∈ ℤ
7. d : ℤ
8. (d * better-gcd(a;u)) = u ∈ ℤ
9. s : ℤ
10. t : ℤ
11. better-gcd(a;u) = ((s * a) + (t * u)) ∈ ℤ
12. R : ℤ List
13. [better-gcd(a;u) / v] = x * R ∈ (ℤ List)
14. S : ℤ List
15. ||S|| = (||v|| + 1) ∈ ℤ
16. x = S ⋅ [better-gcd(a;u) / v] ∈ ℤ
17. ∃R:ℤ List. ([a; [u / v]] = x * R ∈ (ℤ List))
⊢ ∃S:ℤ List. ((||S|| = ((||v|| + 1) + 1) ∈ ℤ) ∧ (x = S ⋅ [a; [u / v]] ∈ ℤ))
Latex:
Latex:
1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}u:\mBbbZ{}
          ((\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]))))
\mvdash{}  \mforall{}u@0:\mBbbZ{}
        ((\mexists{}R:\mBbbZ{}  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))
        \mwedge{}  (\mexists{}S:\mBbbZ{}  List
                ((||S||  =  ((||v||  +  1)  +  1))
                \mwedge{}  (accumulate  (with  value  a  and  list  item  b):
                        better-gcd(a;b)
                      over  list:
                          v
                      with  starting  value:
                        better-gcd(u@0;u))
                    =  S  \mcdot{}  [u@0;  [u  /  v]]))))
By
Latex:
((D  0  THENA  Auto)
  THEN  RenameVar  `a'  (-1)
  THEN  (InstHyp  [\mkleeneopen{}better-gcd(a;u)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}accumulate  (with  value  a  and  list  item  b):
                                            better-gcd(a;b)
                                          over  list:
                                              v
                                          with  starting  value:
                                            better-gcd(a;u))\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  (Thin  (-1)  THEN  RenameVar  `x'  (-1)  THEN  Thin  3)
  THEN  (InstLemma  `better-gcd-properties`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  Auto)
Home
Index