Nuprl Definition : total-run-lt-witness

total-run-lt-witness() ==

e1,e2.
   let x,y = e2
   in let x1,y1 = e1
      in if (x) < (x1)
            then if (x1) < (x)
                    then

else (inr inr <1, <x1, y1>, inl <

,

> ,

>  )
            else if (x1) < (x)
                    then inr (inl <1, <x, y>, inl <

,

> ,

> )
else tt

Definitions occuring in Statement : btrue: tt, it:

, less: if (a) < (b) then c else d, lambda:

x.A[x], spread: spread def, pair: <a, b>, inr: inr x , inl: inl x , natural_number: $n
Definitions : lambda:

x.A[x], spread: spread def, less: if (a) < (b) then c else d, inr: inr x , natural_number: $n, inl: inl x , pair: <a, b>, it:

, btrue: tt
FDL editor aliases : total-run-lt-witness

total-run-lt-witness() == \mlambda{}e1,e2. let x,y = e2 in let x1,y1 = e1 in if (x) < (x1) then if (x1) < (x) then \mcdot{} else (inr inr ə, <x1, y1>, inl <\mcdot{}, \mcdot{}> , \mcdot{}> ) else if (x1) < (x) then inr (inl ə, <x, y>, inl <\mcdot{}, \mcdot{}> , \mcdot{}> ) else tt Date html generated: 2011_08_17-PM-03_38_23 Last ObjectModification: 2010_11_30-AM-00_42_21 Home Index