Nuprl Definition : RankEx2_ind

            RankEx2_LeafT(leaft) LeafT[leaft];
            RankEx2_LeafS(leafs) LeafS[leafs];
            RankEx2_Prod(prod) rec1.Prod[prod; rec1];
            RankEx2_Union(union) rec2.Union[union; rec2];
            RankEx2_ListProd(listprod) rec3.ListProd[listprod; rec3];
            RankEx2_UnionList(unionlist) rec4.UnionList[unionlist; rec4])  ==
  fix((λRankEx2_ind,v. let lbl,v1 
                       in if lbl="LeafT" then LeafT[v1]
                          if lbl="LeafS" then LeafS[v1]
                          if lbl="Prod" then let v2,v3 v1 in let v4,v5 v2 in Prod[<<v4, v5>v3>RankEx2_ind v4]
                          if lbl="Union"
                            then case v1
                                  of inl(x) =>
                                  let x1,x2 
                                  in Union[inl <x1, x2>RankEx2_ind x2]
                                  inr(y) =>
                                  Union[inr RankEx2_ind y]
                          if lbl="ListProd" then ListProd[v1; λi.let v2,v3 v1[i] in RankEx2_ind v3]
                          if lbl="UnionList"
                            then case v1
                                  of inl(x) =>
                                  UnionList[inl x; Ax]
                                  inr(y) =>
                                  UnionList[inr ; λi.(RankEx2_ind y[i])]
                          else ⊥
                          fi )) 

Definitions occuring in Statement :  select: L[n] bottom: atom_eq: if a=b then else fi  apply: a fix: fix(F) lambda: λx.A[x] spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x token: "$token" axiom: Ax
FDL editor aliases :  RankEx2_ind
                        RankEx2\_LeafT(leaft){}\mRightarrow{}  LeafT[leaft];
                        RankEx2\_LeafS(leafs){}\mRightarrow{}  LeafS[leafs];
                        RankEx2\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;  rec1];
                        RankEx2\_Union(union){}\mRightarrow{}  rec2.Union[union;  rec2];
                        RankEx2\_ListProd(listprod){}\mRightarrow{}  rec3.ListProd[listprod;  rec3];
                        RankEx2\_UnionList(unionlist){}\mRightarrow{}  rec4.UnionList[unionlist;  rec4])    ==
    fix((\mlambda{}RankEx2$_{ind}$,v.  let  lbl,v1  =  v 
                                            in  if  lbl="LeafT"  then  LeafT[v1]
                                                  if  lbl="LeafS"  then  LeafS[v1]
                                                  if  lbl="Prod"
                                                      then  let  v2,v3  =  v1 
                                                                in  let  v4,v5  =  v2 
                                                                      in  Prod[<<v4,  v5>,  v3>  RankEx2$_{ind}$  v4]
                                                  if  lbl="Union"
                                                      then  case  v1
                                                                  of  inl(x)  =>
                                                                  let  x1,x2  =  x 
                                                                  in  Union[inl  <x1,  x2>  RankEx2$_{ind}$  x2]
                                                                  |  inr(y)  =>
                                                                  Union[inr  y  ;  RankEx2$_{ind}$  y]
                                                  if  lbl="ListProd"  then  ListProd[v1;  \mlambda{}i.let  v2,v3  =  v1[i]  in  RankEx2$\mbackslash{}ff\000C5f{ind}$  v3]
                                                  if  lbl="UnionList"
                                                      then  case  v1
                                                                  of  inl(x)  =>
                                                                  UnionList[inl  x;  Ax]
                                                                  |  inr(y)  =>
                                                                  UnionList[inr  y  ;  \mlambda{}i.(RankEx2$_{ind}$  y[i])]
                                                  else  \mbot{}
                                                  fi  )) 

Date html generated: 2015_07_17-AM-07_50_19
Last ObjectModification: 2014_05_06-PM-01_45_55

Home Index