Nuprl Definition : RankEx4_ind
RankEx4_ind(v;
            RankEx4_Foo(foo)
⇒ rec1.Foo[foo; rec1])  ==
  fix((λRankEx4_ind,v. let lbl,v1 = v 
                       in if lbl="Foo"
                          then case v1 of inl(x) => Foo[inl x; Ax] | inr(y) => Foo[inr y  RankEx4_ind y]
                          else Ax
                          fi )) 
  v
Definitions occuring in Statement : 
atom_eq: if a=b then c else d fi 
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
inr: inr x 
, 
inl: inl x
, 
token: "$token"
, 
axiom: Ax
Definitions occuring in definition : 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
atom_eq: if a=b then c else d fi 
, 
token: "$token"
, 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
inl: inl x
, 
inr: inr x 
, 
apply: f a
, 
axiom: Ax
FDL editor aliases : 
RankEx4_ind
Latex:
RankEx4\_ind(v;
                        RankEx4\_Foo(foo){}\mRightarrow{}  rec1.Foo[foo;  rec1])    ==
    fix((\mlambda{}RankEx4$_{ind}$,v.  let  lbl,v1  =  v 
                                            in  if  lbl="Foo"
                                                  then  case  v1
                                                              of  inl(x)  =>
                                                              Foo[inl  x;  Ax]
                                                              |  inr(y)  =>
                                                              Foo[inr  y  ;  RankEx4$_{ind}$  y]
                                                  else  Ax
                                                  fi  )) 
    v
Date html generated:
2016_05_16-AM-09_04_46
Last ObjectModification:
2015_12_14-PM-01_41_14
Theory : C-semantics
Home
Index