Step * 2 1 2 of Lemma gcd-list-property


1. : ℤ
2. : ℤ List
3. ∀u:ℤ
     ((∃R:ℤ List
        ([u v]
        accumulate (with value 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 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 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 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 THENA Auto)
   THEN RenameVar `a' (-1)
   THEN (InstHyp [⌜better-gcd(a;u)⌝3⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜accumulate (with value 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. : ℤ
2. : ℤ List
3. : ℤ
4. : ℤ
5. : ℤ
6. (c better-gcd(a;u)) a ∈ ℤ
7. : ℤ
8. (d better-gcd(a;u)) u ∈ ℤ
9. : ℤ
10. : ℤ
11. better-gcd(a;u) ((s a) (t u)) ∈ ℤ
12. : ℤ List
13. [better-gcd(a;u) v] R ∈ (ℤ List)
14. : ℤ List
15. ||S|| (||v|| 1) ∈ ℤ
16. S ⋅ [better-gcd(a;u) v] ∈ ℤ
⊢ ∃R:ℤ List. ([a; [u v]] R ∈ (ℤ List))

2
1. : ℤ
2. : ℤ List
3. : ℤ
4. : ℤ
5. : ℤ
6. (c better-gcd(a;u)) a ∈ ℤ
7. : ℤ
8. (d better-gcd(a;u)) u ∈ ℤ
9. : ℤ
10. : ℤ
11. better-gcd(a;u) ((s a) (t u)) ∈ ℤ
12. : ℤ List
13. [better-gcd(a;u) v] R ∈ (ℤ List)
14. : ℤ List
15. ||S|| (||v|| 1) ∈ ℤ
16. S ⋅ [better-gcd(a;u) v] ∈ ℤ
17. ∃R:ℤ List. ([a; [u v]] 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