---

Step * of Lemma int_term_ind-var

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

---

Latex:

---

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


By

---

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

---

Home Index