Nuprl Definition : RankEx2_ind

RankEx2_ind(v;
            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 = 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; λ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 y ; λi.(RankEx2_ind y[i])]
                          else ⊥
                          fi )) 
  v


Definitions occuring in Statement :  select: L[n],  bottom: ⊥,  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>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  token: "$token",  axiom: Ax
FDL editor aliases :  RankEx2_ind
RankEx2\_ind(v;
                        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  )) 
    v


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

Home Index