Nuprl Definition : rng-pps

rng-pps(r;eq) ==
  mk-complete-pgeo(mk-pgeo(rng-pp-primitives(r);
                           λl,a,v,v. Ax;
                           λa,l,m. if eq (a . m) 0 then inr <a, λnp.(np Ax), λ%6.Ax>  else inl (λ%.Ax) fi ;
                           λl,a,b. if eq (b . l) 0 then inr <l, λnp.(np Ax), λ%6.Ax>  else inl (λ%.Ax) fi ;
                           λa,b,_. <(a x b), λ_.Ax, λ_.Ax>;
                           λa,b,_. <(a x b), λ_.Ax, λ_.Ax>;
                           λl.rng-pp-nontriv1(r;eq;l);
                           λa.rng-pp-nontriv2(r;eq;a));λi.1)


Definitions occuring in Statement :  rng-pp-nontriv2: rng-pp-nontriv2(r;eq;p),  rng-pp-nontriv1: rng-pp-nontriv1(r;eq;l),  rng-pp-primitives: rng-pp-primitives(r),  mk-complete-pgeo: mk-complete-pgeo(pg;p),  mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  inr: inr x ,  inl: inl x,  natural_number: $n,  axiom: Ax,  rng_one: 1,  rng_zero: 0,  scalar-product: (a . b),  cross-product: (a x b)
Definitions occuring in definition :  mk-complete-pgeo: mk-complete-pgeo(pg;p),  mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),  rng-pp-primitives: rng-pp-primitives(r),  ifthenelse: if b then t else f fi ,  scalar-product: (a . b),  natural_number: $n,  rng_zero: 0,  inr: inr x ,  apply: f a,  inl: inl x,  cross-product: (a x b),  pair: <a, b>,  axiom: Ax,  rng-pp-nontriv1: rng-pp-nontriv1(r;eq;l),  rng-pp-nontriv2: rng-pp-nontriv2(r;eq;p),  lambda: λx.A[x],  rng_one: 1
FDL editor aliases :  rng-pps
Latex:
rng-pps(r;eq)  ==
    mk-complete-pgeo(mk-pgeo(rng-pp-primitives(r);
                                                      \mlambda{}l,a,v,v.  Ax;
                                                      \mlambda{}a,l,m.  if  eq  (a  .  m)  0
                                                                    then  inr  <a,  \mlambda{}np.(np  Ax),  \mlambda{}\%6.Ax> 
                                                                    else  inl  (\mlambda{}\%.Ax)
                                                                    fi  ;
                                                      \mlambda{}l,a,b.  if  eq  (b  .  l)  0
                                                                    then  inr  <l,  \mlambda{}np.(np  Ax),  \mlambda{}\%6.Ax> 
                                                                    else  inl  (\mlambda{}\%.Ax)
                                                                    fi  ;
                                                      \mlambda{}a,b,$_{}$.  <(a  x  b),  \mlambda{}$_{}$.Ax,  \000C\mlambda{}$_{}$.Ax>
                                                      \mlambda{}a,b,$_{}$.  <(a  x  b),  \mlambda{}$_{}$.Ax,  \000C\mlambda{}$_{}$.Ax>
                                                      \mlambda{}l.rng-pp-nontriv1(r;eq;l);
                                                      \mlambda{}a.rng-pp-nontriv2(r;eq;a));\mlambda{}i.1)


Date html generated: 2018_05_22-PM-00_55_23
Last ObjectModification: 2017_12_22-PM-04_09_28

Theory : euclidean!plane!geometry


Home Index