Nuprl Definition : rank-Ex1
rank-Ex1(t) ==
fix((λrank-Ex1,t. if RankEx1_Leaf?(t) then 1
if RankEx1_Prod?(t)
then imax(rank-Ex1 (fst(RankEx1_Prod-prod(t)));rank-Ex1 (snd(RankEx1_Prod-prod(t)))) + 1
if RankEx1_ProdL?(t) then (rank-Ex1 (snd(RankEx1_ProdL-prodl(t)))) + 1
if RankEx1_ProdR?(t) then (rank-Ex1 (fst(RankEx1_ProdR-prodr(t)))) + 1
else imax-list([0 / map(λu.(rank-Ex1 u);RankEx1_List-list(t))]) + 1
fi ))
t
Definitions occuring in Statement :
RankEx1_List-list: RankEx1_List-list(v),
RankEx1_ProdR-prodr: RankEx1_ProdR-prodr(v),
RankEx1_ProdR?: RankEx1_ProdR?(v),
RankEx1_ProdL-prodl: RankEx1_ProdL-prodl(v),
RankEx1_ProdL?: RankEx1_ProdL?(v),
RankEx1_Prod-prod: RankEx1_Prod-prod(v),
RankEx1_Prod?: RankEx1_Prod?(v),
RankEx1_Leaf?: RankEx1_Leaf?(v),
imax-list: imax-list(L),
map: map(f;as),
cons: [a / b],
imax: imax(a;b),
ifthenelse: if b then t else f fi ,
pi1: fst(t),
pi2: snd(t),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
FDL editor aliases :
rank-Ex1
Latex:
rank-Ex1(t) ==
fix((\mlambda{}rank-Ex1,t. if RankEx1\_Leaf?(t) then 1
if RankEx1\_Prod?(t)
then imax(rank-Ex1 (fst(RankEx1\_Prod-prod(t)));rank-Ex1
(snd(RankEx1\_Prod-prod(t))))
+ 1
if RankEx1\_ProdL?(t) then (rank-Ex1 (snd(RankEx1\_ProdL-prodl(t)))) + 1
if RankEx1\_ProdR?(t) then (rank-Ex1 (fst(RankEx1\_ProdR-prodr(t)))) + 1
else imax-list([0 / map(\mlambda{}u.(rank-Ex1 u);RankEx1\_List-list(t))]) + 1
fi ))
t
Date html generated:
2016_05_16-AM-08_58_52
Last ObjectModification:
2013_02_24-PM-11_10_54
Theory : C-semantics
Home
Index