Nuprl Definition : intlex-aux

intlex-aux(l1;l2)
==r if l1 is a pair then let a,as = l1
in let b,bs = l2

                            in if (a) < (b)  then inl Ax  else if a=b  then intlex-aux(as;bs)  else (inr Ax )

otherwise inl Ax

intlex-aux(l1;l2) ==
  fix((λintlex-aux,l1,l2. if l1 is a pair then let a,as = l1
                                               in let b,bs = l2
                                                  in if (a) < (b)

                                                        then inl Ax

                                                        else if a=b  then intlex-aux as bs  else (inr Ax )

                          otherwise inl Ax))
  l1
  l2

Definitions occuring in Statement : ispair: if z is a pair then a otherwise b, less: if (a) < (b) then c else d, int_eq: if a=b then c else d, apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, inr: inr x , inl: inl x, axiom: Ax
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], ispair: if z is a pair then a otherwise b, spread: spread def, less: if (a) < (b) then c else d, int_eq: if a=b then c else d, apply: f a, inr: inr x , inl: inl x, axiom: Ax
FDL editor aliases : intlex-aux

Latex:
intlex-aux(l1;l2) ==r if l1 is a pair then let a,as = l1 in let b,bs = l2 in if (a) < (b) then inl Ax else if a=b then intlex-aux(as;bs) else (inr Ax ) otherwise inl Ax

Latex:
intlex-aux(l1;l2) == fix((\mlambda{}intlex-aux,l1,l2. if l1 is a pair then let a,as = l1 in let b,bs = l2 in if (a) < (b) then inl Ax else if a=b then intlex-aux as bs else (inr Ax ) otherwise inl Ax)) l1 l2 Date html generated: 2017_09_29-PM-05_48_32 Last ObjectModification: 2017_05_31-AM-10_00_19 Theory : list_0 Home Index