Nuprl Definition : int-term-ind-fun

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]) ==
  λt.int_term_ind(t;
                  itermConstant(c)⇒ C[c];
                  itermVar(v)⇒ V[v];
                  itermAdd(l,r)⇒ rl,rr.A[l; r; rl; rr];
                  itermSubtract(l,r)⇒ rl,rr.S[l; r; rl; rr];
                  itermMultiply(l,r)⇒ rl,rr.M[l; r; rl; rr];
                  itermMinus(x)⇒ rx.MN[x; rx]) 


Definitions occuring in Statement :  int_term_ind: int_term_ind,  lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x],  int_term_ind: int_term_ind
FDL editor aliases :  int-term-ind-fun
Latex:
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])  ==
    \mlambda{}t.int\_term\_ind(t;
                                    itermConstant(c){}\mRightarrow{}  C[c];
                                    itermVar(v){}\mRightarrow{}  V[v];
                                    itermAdd(l,r){}\mRightarrow{}  rl,rr.A[l;  r;  rl;  rr];
                                    itermSubtract(l,r){}\mRightarrow{}  rl,rr.S[l;  r;  rl;  rr];
                                    itermMultiply(l,r){}\mRightarrow{}  rl,rr.M[l;  r;  rl;  rr];
                                    itermMinus(x){}\mRightarrow{}  rx.MN[x;  rx]) 


Date html generated: 2017_09_29-PM-05_51_53
Last ObjectModification: 2017_05_12-AM-11_46_12

Theory : omega


Home Index