---

Step * 2 1 1 1 1 1 of Lemma imonomial-cons


1. u : ℤ
2. v : ℤ List
3. ∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u / v]>)) = int_term_value(f;imonomial-term(<a * (f u), v>)\000C) ∈ ℤ)
4. u@0 : ℤ
5. a : ℤ
6. f : ℤ ⟶ ℤ
7. int_term_value(f;imonomial-term(<a * (f u@0), [u / v]>)) = int_term_value(f;imonomial-term(<(a * (f u@0)) * (f u), v>\000C)) ∈ ℤ
8. v1 : ℤ List
9. [u / v] = v1 ∈ (ℤ List)
⊢ int_term_value(f;accumulate (with value t and list item v):
                    t (*) vv
                   over list:
                     v1
                   with starting value:
                    "a" (*) vu@0))
= int_term_value(f;accumulate (with value t and list item v):
                    t (*) vv
                   over list:
                     v1
                   with starting value:
                    "a * (f u@0)"))
∈ ℤ
BY
{ Assert ⌜∀t1,t2:int_term().
            ((int_term_value(f;t1) = int_term_value(f;t2) ∈ ℤ)
            ⇒ (int_term_value(f;accumulate (with value t and list item v):
                                  t (*) vv
                                 over list:
                                   v1
                                 with starting value:
                                  t1))
               = int_term_value(f;accumulate (with value t and list item v):
                                   t (*) vv
                                  over list:
                                    v1
                                  with starting value:
                                   t2))
               ∈ ℤ))⌝⋅ }

1
.....assertion..... 
1. u : ℤ
2. v : ℤ List
3. ∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u / v]>)) = int_term_value(f;imonomial-term(<a * (f u), v>)\000C) ∈ ℤ)
4. u@0 : ℤ
5. a : ℤ
6. f : ℤ ⟶ ℤ
7. int_term_value(f;imonomial-term(<a * (f u@0), [u / v]>)) = int_term_value(f;imonomial-term(<(a * (f u@0)) * (f u), v>\000C)) ∈ ℤ
8. v1 : ℤ List
9. [u / v] = v1 ∈ (ℤ List)
⊢ ∀t1,t2:int_term().
    ((int_term_value(f;t1) = int_term_value(f;t2) ∈ ℤ)
    ⇒ (int_term_value(f;accumulate (with value t and list item v):
                          t (*) vv
                         over list:
                           v1
                         with starting value:
                          t1))
       = int_term_value(f;accumulate (with value t and list item v):
                           t (*) vv
                          over list:
                            v1
                          with starting value:
                           t2))
       ∈ ℤ))

2
1. u : ℤ
2. v : ℤ List
3. ∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u / v]>)) = int_term_value(f;imonomial-term(<a * (f u), v>)\000C) ∈ ℤ)
4. u@0 : ℤ
5. a : ℤ
6. f : ℤ ⟶ ℤ
7. int_term_value(f;imonomial-term(<a * (f u@0), [u / v]>)) = int_term_value(f;imonomial-term(<(a * (f u@0)) * (f u), v>\000C)) ∈ ℤ
8. v1 : ℤ List
9. [u / v] = v1 ∈ (ℤ List)
10. ∀t1,t2:int_term().
      ((int_term_value(f;t1) = int_term_value(f;t2) ∈ ℤ)
      ⇒ (int_term_value(f;accumulate (with value t and list item v):
                            t (*) vv
                           over list:
                             v1
                           with starting value:
                            t1))
         = int_term_value(f;accumulate (with value t and list item v):
                             t (*) vv
                            over list:
                              v1
                            with starting value:
                             t2))
         ∈ ℤ))
⊢ int_term_value(f;accumulate (with value t and list item v):
                    t (*) vv
                   over list:
                     v1
                   with starting value:
                    "a" (*) vu@0))
= int_term_value(f;accumulate (with value t and list item v):
                    t (*) vv
                   over list:
                     v1
                   with starting value:
                    "a * (f u@0)"))
∈ ℤ

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}u,a:\mBbbZ{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.    (int\_term\_value(f;imonomial-term(<a,  [u  /  v]>))  =  int\_term\_value(f;imonomial-\000Cterm(<a  *  (f  u),  v>)))
4.  u@0  :  \mBbbZ{}
5.  a  :  \mBbbZ{}
6.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
7.  int\_term\_value(f;imonomial-term(<a  *  (f  u@0),  [u  /  v]>))  =  int\_term\_value(f;imonomial-term(<(a  *  \000C(f  u@0))  *  (f  u),  v>))
8.  v1  :  \mBbbZ{}  List
9.  [u  /  v]  =  v1
\mvdash{}  int\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                        t  (*)  vv
                                      over  list:
                                          v1
                                      with  starting  value:
                                        "a"  (*)  vu@0))
=  int\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                        t  (*)  vv
                                      over  list:
                                          v1
                                      with  starting  value:
                                        "a  *  (f  u@0)"))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}t1,t2:int\_term().
                    ((int\_term\_value(f;t1)  =  int\_term\_value(f;t2))
                    {}\mRightarrow{}  (int\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                                                t  (*)  vv
                                                              over  list:
                                                                  v1
                                                              with  starting  value:
                                                                t1))
                          =  int\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                                                  t  (*)  vv
                                                                over  list:
                                                                    v1
                                                                with  starting  value:
                                                                  t2))))\mkleeneclose{}\mcdot{}

---

Home Index