---

Step * of Lemma int_term_ind-minus

∀[C,V,A,S,M,MN,x: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]) 
   "-"x ~ MN[x;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]) 
               x])
BY
{ (RepUR ``int-term-ind-fun`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C,V,A,S,M,MN,x: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]) 
      "-"x  \msim{}  MN[x;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]) 
                              x])


By

---

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

---

Home Index