Nuprl Definition : extend-val

extend-val(v0;g;x) ==
  formula_ind(x;
              pvar(v)⇒ v0 pvar(v);
              pnot(a)⇒ r.¬b(g a);
              pand(a,b)⇒ r1,r2.(g a) ∧b (g b);
              por(a,b)⇒ r1,r2.(g a) ∨b(g b);
              pimp(a,b)⇒ r1,r2.(¬b(g a)) ∨b(g b)) 


Definitions occuring in Statement :  formula_ind: formula_ind,  pvar: pvar(name),  bor: p ∨bq,  band: p ∧b q,  bnot: ¬bb,  apply: f a
Definitions occuring in definition :  formula_ind: formula_ind,  pvar: pvar(name),  band: p ∧b q,  bor: p ∨bq,  bnot: ¬bb,  apply: f a
FDL editor aliases :  extend-val
Latex:
extend-val(v0;g;x)  ==
    formula\_ind(x;
                            pvar(v){}\mRightarrow{}  v0  pvar(v);
                            pnot(a){}\mRightarrow{}  r.\mneg{}\msubb{}(g  a);
                            pand(a,b){}\mRightarrow{}  r1,r2.(g  a)  \mwedge{}\msubb{}  (g  b);
                            por(a,b){}\mRightarrow{}  r1,r2.(g  a)  \mvee{}\msubb{}(g  b);
                            pimp(a,b){}\mRightarrow{}  r1,r2.(\mneg{}\msubb{}(g  a))  \mvee{}\msubb{}(g  b)) 


Date html generated: 2016_05_15-PM-07_15_07
Last ObjectModification: 2015_09_23-AM-08_13_26

Theory : general


Home Index