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
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: 2015_07_17-AM-07_48_42
Last ObjectModification: 2013_02_24-PM-11_10_54

Home Index