Nuprl Definition : rng-pp-nontriv1
rng-pp-nontriv1(r;eq;l) ==
eval x = non-zero-component(r;λx,y. (eq x y);3;l) in
if x=0
then <λx.if x=1 then l 0 else if x=0 then -r (l 1) else 0
, λx.if x=2 then l 0 else if x=0 then -r (l 2) else 0
, (λx.if x=1 then l 0 else if x=0 then -r (l 1) else 0 + λx.if x=2 then l 0 else if x=0 then -r (l 2) else 0)
, λ%.Ax
, λ%.Ax
, λ%.Ax
, <nonzero-cross-imp(r;λx,y. (eq x y);λx.if x=1 then l 0 else if x=0 then -r (l 1) else 0;λx.if x=2
then l 0
else if x=0
then -r (l 2)
else 0)
, λ%.Ax
, λ%.Ax>
, <nonzero-cross-imp(r;λx,y. (eq x y);λx.if x=2
then l 0
else if x=0 then -r (l 2) else 0;(λx.if x=1
then l 0
else if x=0
then -r (l 1)
else 0 + λx.if x=2
then l 0
else if x=0
then -r (l 2)
else 0))
, λ%.Ax
, λ%.Ax>
, nonzero-cross-imp(r;λx,y. (eq x y);(λx.if x=1
then l 0
else if x=0 then -r (l 1) else 0 + λx.if x=2
then l 0
else if x=0
then -r (l 2)
else 0);λx.if x=1
then l 0
else if x=0
then -r (l 1)
else 0)
, λ%.Ax
, λ%.Ax>
else if x=1
then <λx.if x=0 then l 1 else if x=1 then -r (l 0) else 0
, λx.if x=2 then l 1 else if x=1 then -r (l 2) else 0
, (λx.if x=0 then l 1 else if x=1 then -r (l 0) else 0 + λx.if x=2
then l 1
else if x=1 then -r (l 2) else 0)
, λ%.Ax
, λ%.Ax
, λ%.Ax
, <nonzero-cross-imp(r;λx,y. (eq x y);λx.if x=0 then l 1 else if x=1 then -r (l 0) else 0;λx.if x=2
then l 1
else if x=1
then -r (l 2)
else 0)
, λ%.Ax
, λ%.Ax>
, <nonzero-cross-imp(r;λx,y. (eq x y);λx.if x=2
then l 1
else if x=1 then -r (l 2) else 0;(λx.if x=0
then l 1
else if x=1
then -r (l 0)
else 0 + λx.if x=2
then l 1
else if x=1
then -r
(l 2)
else 0))
, λ%.Ax
, λ%.Ax>
, nonzero-cross-imp(r;λx,y. (eq x y);(λx.if x=0
then l 1
else if x=1 then -r (l 0) else 0 + λx.if x=2
then l 1
else if x=1
then -r (l 2)
else 0);λx.if x=0
then l 1
else if x=1
then -r
(l 0)
else 0)
, λ%.Ax
, λ%.Ax>
else if x=2
then <λx.if x=0 then l 2 else if x=2 then -r (l 0) else 0
, λx.if x=1 then l 2 else if x=2 then -r (l 1) else 0
, (λx.if x=0 then l 2 else if x=2 then -r (l 0) else 0 + λx.if x=1
then l 2
else if x=2 then -r (l 1) else 0)
, λ%.Ax
, λ%.Ax
, λ%.Ax
, <nonzero-cross-imp(r;λx,y. (eq x y);λx.if x=0 then l 2 else if x=2 then -r (l 0) else 0;λx.if x=1
then l 2
else if x=2
then -r
(l
1)
else 0)
, λ%.Ax
, λ%.Ax>
, <nonzero-cross-imp(r;λx,y. (eq x y);λx.if x=1
then l 2
else if x=2
then -r (l 1)
else 0;(λx.if x=0
then l 2
else if x=2
then -r (l 0)
else 0 + λx.if x=1
then l 2
else if x=2
then -r (l 1)
else 0))
, λ%.Ax
, λ%.Ax>
, nonzero-cross-imp(r;λx,y. (eq x y);(λx.if x=0 then l 2 else if x=2 then -r (l 0) else 0 + ...);...)
, ...>
else ...
Definitions occuring in Statement :
callbyvalue: callbyvalue,
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
natural_number: $n,
axiom: Ax,
rng_minus: -r,
rng_zero: 0,
nonzero-cross-imp: nonzero-cross-imp(r;eq;a;b),
non-zero-component: non-zero-component(r;eq;k;a),
vector-add: (a + b)
Definitions occuring in definition :
rng_zero: 0,
natural_number: $n,
apply: f a,
rng_minus: -r,
int_eq: if a=b then c else d,
lambda: λx.A[x],
nonzero-cross-imp: nonzero-cross-imp(r;eq;a;b),
pair: <a, b>,
axiom: Ax,
vector-add: (a + b),
non-zero-component: non-zero-component(r;eq;k;a),
callbyvalue: callbyvalue,
spread: spread def
FDL editor aliases :
rng-pp-nontriv1
Latex:
rng-pp-nontriv1(r;eq;l) ==
eval x = non-zero-component(r;\mlambda{}x,y. (eq x y);3;l) in
if x=0
then <\mlambda{}x.if x=1 then l 0 else if x=0 then -r (l 1) else 0
, \mlambda{}x.if x=2 then l 0 else if x=0 then -r (l 2) else 0
, (\mlambda{}x.if x=1 then l 0 else if x=0 then -r (l 1) else 0 + \mlambda{}x.if x=2
then l 0
else if x=0 then -r (l 2) else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax
, <nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);\mlambda{}x.if x=1
then l 0
else if x=0 then -r (l 1) else 0;\mlambda{}x.if x=2
then l 0
else if x=0
then -r (l 2)
else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
, <nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);\mlambda{}x.if x=2
then l 0
else if x=0
then -r (l 2)
else 0;(\mlambda{}x.if x=1
then l 0
else if x=0
then -r (l 1)
else 0 + \mlambda{}x.if x=2
then l 0
else if x=0
then -r (l 2)
else 0))
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
, nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);(\mlambda{}x.if x=1
then l 0
else if x=0
then -r (l 1)
else 0 + \mlambda{}x.if x=2
then l 0
else if x=0
then -r (l 2)
else 0);\mlambda{}x.if x=1
then l 0
else if x=0
then -r (l 1)
else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
else if x=1
then <\mlambda{}x.if x=0 then l 1 else if x=1 then -r (l 0) else 0
, \mlambda{}x.if x=2 then l 1 else if x=1 then -r (l 2) else 0
, (\mlambda{}x.if x=0 then l 1 else if x=1 then -r (l 0) else 0 + \mlambda{}x.if x=2
then l 1
else if x=1
then -r (l 2)
else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax
, <nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);\mlambda{}x.if x=0
then l 1
else if x=1 then -r (l 0) else 0;\mlambda{}x.if x=2
then l 1
else if x=1
then -r
(l 2)
else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
, <nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);\mlambda{}x.if x=2
then l 1
else if x=1
then -r (l 2)
else 0;(\mlambda{}x.if x=0
then l 1
else if x=1
then -r (l 0)
else 0 + \mlambda{}x.if x=2
then l 1
else if x=1
then -r (l 2)
else 0))
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
, nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);(\mlambda{}x.if x=0
then l 1
else if x=1
then -r (l 0)
else 0 + \mlambda{}x.if x=2
then l 1
else if x=1
then -r (l 2)
else 0);\mlambda{}x.if x=0
then l 1
else if x=1
then -r (l 0)
else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
else if x=2
then <\mlambda{}x.if x=0 then l 2 else if x=2 then -r (l 0) else 0
, \mlambda{}x.if x=1 then l 2 else if x=2 then -r (l 1) else 0
, (\mlambda{}x.if x=0 then l 2 else if x=2 then -r (l 0) else 0 + \mlambda{}x.if x=1
then l 2
else if x=2
then -r (l 1)
else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax
, <nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);\mlambda{}x.if x=0
then l 2
else if x=2
then -r (l 0)
else 0;\mlambda{}x.if x=1
then l 2
else if x=2
then -r (l 1)
else 0)
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
, <nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);\mlambda{}x.if x=1
then l 2
else if x=2
then -r (l 1)
else 0;(\mlambda{}x.if x=0
then l 2
else if x=2
then -r (l 0)
else 0 + \mlambda{}x.if x=1
then l 2
else if x=2
then -r
(l
1)
else 0))
, \mlambda{}\%.Ax
, \mlambda{}\%.Ax>
, nonzero-cross-imp(r;\mlambda{}x,y. (eq x y);(\mlambda{}x.if x=0
then l 2
else if x=2 then -r (l 0) else 0 + ...);...)
, ...>
else ...
Date html generated:
2018_05_22-PM-00_54_08
Last ObjectModification:
2018_01_14-PM-03_48_51
Theory : euclidean!plane!geometry
Home
Index