Nuprl Definition : RankEx1_ind
RankEx1_ind(v;
            RankEx1_Leaf(leaf)
⇒ Leaf[leaf];
            RankEx1_Prod(prod)
⇒ rec1.Prod[prod; rec1];
            RankEx1_ProdL(prodl)
⇒ rec2.ProdL[prodl; rec2];
            RankEx1_ProdR(prodr)
⇒ rec3.ProdR[prodr; rec3];
            RankEx1_List(list)
⇒ rec4.List[list; rec4])  ==
  fix((λRankEx1_ind,v. let lbl,v1 = v 
                       in if lbl="Leaf" then Leaf[v1]
                          if lbl="Prod" then let v2,v3 = v1 in Prod[<v2, v3> <RankEx1_ind v2, RankEx1_ind v3>]
                          if lbl="ProdL" then let v2,v3 = v1 in ProdL[<v2, v3> RankEx1_ind v3]
                          if lbl="ProdR" then let v2,v3 = v1 in ProdR[<v2, v3> RankEx1_ind v2]
                          if lbl="List" then List[v1; λi.(RankEx1_ind v1[i])]
                          else Ax
                          fi )) 
  v
Definitions occuring in Statement : 
select: L[n]
, 
atom_eq: if a=b then c else d fi 
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
pair: <a, b>
, 
token: "$token"
, 
axiom: Ax
Definitions occuring in definition : 
fix: fix(F)
, 
spread: spread def, 
pair: <a, b>
, 
atom_eq: if a=b then c else d fi 
, 
token: "$token"
, 
lambda: λx.A[x]
, 
apply: f a
, 
select: L[n]
, 
axiom: Ax
FDL editor aliases : 
RankEx1_ind
Latex:
RankEx1\_ind(v;
                        RankEx1\_Leaf(leaf){}\mRightarrow{}  Leaf[leaf];
                        RankEx1\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;  rec1];
                        RankEx1\_ProdL(prodl){}\mRightarrow{}  rec2.ProdL[prodl;  rec2];
                        RankEx1\_ProdR(prodr){}\mRightarrow{}  rec3.ProdR[prodr;  rec3];
                        RankEx1\_List(list){}\mRightarrow{}  rec4.List[list;  rec4])    ==
    fix((\mlambda{}RankEx1$_{ind}$,v.  let  lbl,v1  =  v 
                                            in  if  lbl="Leaf"  then  Leaf[v1]
                                                  if  lbl="Prod"
                                                      then  let  v2,v3  =  v1 
                                                                in  Prod[<v2,  v3>  <RankEx1$_{ind}$  v2,  RankEx1\mbackslash{}f\000Cf24_{ind}$  v3>]
                                                  if  lbl="ProdL"  then  let  v2,v3  =  v1  in  ProdL[<v2,  v3>  RankEx1$_\mbackslash{}ff7\000Cbind}$  v3]
                                                  if  lbl="ProdR"  then  let  v2,v3  =  v1  in  ProdR[<v2,  v3>  RankEx1$_\mbackslash{}ff7\000Cbind}$  v2]
                                                  if  lbl="List"  then  List[v1;  \mlambda{}i.(RankEx1$_{ind}$  v1[i])]
                                                  else  Ax
                                                  fi  )) 
    v
Date html generated:
2016_05_16-AM-08_58_40
Last ObjectModification:
2015_12_14-PM-01_42_11
Theory : C-semantics
Home
Index