---

Step * of Lemma int_term_ind-add

∀[C,V,A,S,M,MN,a,b:Top].
  (int-term-ind-fun(c.C[c];
                    v.V[v];
                    l,r,rl,rr.A[l;r;rl;rr];
                    l,r,rl,rr.S[l;r;rl;rr];
                    l,r,rl,rr.M[l;r;rl;rr];
                    x,rx.MN[x;rx]) 
   (a (+) b) ~ A[a;b;int-term-ind-fun(c.C[c];
                                      v.V[v];
                                      l,r,rl,rr.A[l;r;rl;rr];
                                      l,r,rl,rr.S[l;r;rl;rr];
                                      l,r,rl,rr.M[l;r;rl;rr];
                                      x,rx.MN[x;rx]) 
                     a;int-term-ind-fun(c.C[c];
                                        v.V[v];
                                        l,r,rl,rr.A[l;r;rl;rr];
                                        l,r,rl,rr.S[l;r;rl;rr];
                                        l,r,rl,rr.M[l;r;rl;rr];
                                        x,rx.MN[x;rx]) 
                       b])
BY
{ (RepUR ``int-term-ind-fun`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C,V,A,S,M,MN,a,b:Top].
    (int-term-ind-fun(c.C[c];
                                        v.V[v];
                                        l,r,rl,rr.A[l;r;rl;rr];
                                        l,r,rl,rr.S[l;r;rl;rr];
                                        l,r,rl,rr.M[l;r;rl;rr];
                                        x,rx.MN[x;rx]) 
      (a  (+)  b)  \msim{}  A[a;b;int-term-ind-fun(c.C[c];
                                                                            v.V[v];
                                                                            l,r,rl,rr.A[l;r;rl;rr];
                                                                            l,r,rl,rr.S[l;r;rl;rr];
                                                                            l,r,rl,rr.M[l;r;rl;rr];
                                                                            x,rx.MN[x;rx]) 
                                          a;int-term-ind-fun(c.C[c];
                                                                                v.V[v];
                                                                                l,r,rl,rr.A[l;r;rl;rr];
                                                                                l,r,rl,rr.S[l;r;rl;rr];
                                                                                l,r,rl,rr.M[l;r;rl;rr];
                                                                                x,rx.MN[x;rx]) 
                                              b])


By

---

Latex:
(RepUR  ``int-term-ind-fun``  0  THEN  Auto)

---

Home Index