Nuprl Definition : decd-run-lt
decd-run-lt(r) ==
e1,e2.
case int_seg_decide(k.(I(k) where I(
) =
when _ = < 0, _ = I(+1). _.
when = 0.
_,x,y.
let a,x1 = x
in let a1,y1 = y
in if a=a1 then if x1=2 y1 then tt else (inr (_.) ) else (inr (_.) )
when zzj = > 0, %3 = I(-1).
_,x,y.
case list_accum(x@0,a.case x@0
of inl(i) =>
inl i
| inr(i) =>
case %3 (.) x a
of inl(%2) =>
let x,y1 = a
in let x1,y2 = y
in if y1=2 y2
then if (x) < (x1)
then inl <<x, y2>, <i, , >, %2, inl <, > >
else let info,_ = r x1
in case info
of inl(y) =>
let ev,_,_ = y in
let x1,y = ev
in if y2=2 y
then if x=x1
then inl <<x1, y>
, <i, , >
, %2
, ff>
else (inr (i + 1) )
else (inr (i + 1) )
| inr(_) =>
let ev,_,_ = "???" in
let x1,y = ev
in if y2=2 y
then if x=x1
then inl <<x1, y>
, <i, , >
, %2
, ff>
else (inr (i + 1) )
else (inr (i + 1) )
else let info,S = r x1
in (_.case info
of inl(y) =>
let ev,z,m = y in
let x2,y = ev
in if y1=2 y
then let info,_ = _
in case info
of inl(y1) =>
let ev,_,_ = y1 in
let x1,_ = ev
in if x=x1
then inl <<x1, y>
, <i, , >
, %2
, ff>
else (inr (i + 1) )
| inr(_) =>
let ev,_,_ = "???" in
let x1,_ = ev
in if x=x1
then inl <<x1, y>
, <i, , >
, %2
, ff>
else (inr (i + 1) )
else (inr (i + 1) )
| inr(z) =>
let ev,z,m = "???" in
let x2,y = ev
in if y1=2 y
then let info,_ = _
in case info
of inl(y1) =>
let ev,_,_ = y1 in
let x1,_ = ev
in if x=x1
then inl <<x1, y>
, <i, , >
, %2
, ff>
else (inr (i + 1) )
| inr(_) =>
if x=x2
then inl <<x2, y>
, <i, , >
, %2
, ff>
else (inr (i + 1) )
else (inr (i + 1) ))
<info, S>
| inr(_) =>
inr (i + 1) ;
inr 0 ;
prior-run-events(r;let x,_ = y
in x))
of inl(trp) =>
inl let _,%6 = I(zzj) where I() =
when _ = < 0, _ = I(+1). _.
when = 0.
_,_,_.
<_.(inr <, > )
, %.case %
of inl(%1) =>
let _,_,_,_ = %1
in
| inr(%2) =>
let _,_ = %2
in
>
when zzj = > 0, % = I(-1).
_.if zzj=0
then _,_.<_., _.>
else (x,y@0.
<%@0.let z,%7,%8 = %@0 in
inl let %10,_ = % (.) z y@0
in case %10 %8
of inl(%9) =>
let z@0,_,%13,%14 = %9
in <z@0
,
, if zzj - 1=0
then
else <z, %7, %13>
, %14>
| inr(%10) =>
let _,_ = %10
in <x, , , %7>
, %@0.case %@0
of inl(%6) =>
let z,_,%10,%11 = %6
in if zzj=1
then <y@0, %11, >
else if zzj - 1=0
then
else let z@0,%18,%19 = %10 in
<z@0
, %18
, let _,%22 = % (.) z@0
y@0
in %22
(inl <z
,
, %19
, %11> )>
| inr(%7) =>
let _,_ = %7
in any
>)
end where
(.)
x
y
in %6 (inl let z,%10 = trp in <z, let _,%13,%14 = %10 in <, %13, %14>> )
| inr(_) =>
inr (_.any )
end where
(.)
e1
e2);1;let x,_ = e2
in x + 1)
of inl(%2) =>
inl let k,%6 = %2
in <k, %6>
| inr(_) =>
inr (_.any )
Definitions occuring in Statement :
prior-run-events: prior-run-events(r;t),
int_seg_decide: int_seg_decide(d;i;j),
bfalse: ff,
btrue: tt,
it: ,
spreadn: spread4,
spreadn: spread3,
less: if (a) < (b) then c else d,
int_eq: if a=b then c else d,
apply: f a,
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 ,
ind: ind def,
subtract: n - m,
add: n + m,
natural_number: $n,
token: "$token",
list_accum: list_accum(x,a.f[x; a];y;l),
atom_eq: atomeqn def
FDL editor aliases :
decd-run-lt
decd-run-lt(r) ==
\mlambda{}e1,e2.
case int\_seg\_decide(\mlambda{}k.(I(k) where I(\malpha{}) =
when $_{}$ = \malpha{} < 0, $_{}$ = I(\000C\malpha{}+1). \mlambda{}$_{}$.\mcdot{}
when \malpha{} = 0.
\mlambda{}$_{}$,x,y.
let a,x1 = x
in let a1,y1 = y
in if a=a1
then if x1=2 y1
then tt
else (inr (\mlambda{}$_{}$.\mcdot{}) )
else (inr (\mlambda{}$_{}$.\mcdot{}) )
when zzj = \malpha{} > 0, \%3 = I(\malpha{}-1).
\mlambda{}$_{}$,x,y.
case list\_accum(x@0,a.case x@0
of inl(i) =>
inl i
| inr(i) =>
case \%3 (\mlambda{}.\mcdot{}) x a
of inl(\%2) =>
let x,y1 = a
in let x1,y2 = y
in if y1=2 y2
then if (x) < (x1)
then inl <<x, y2>
, <i, \mcdot{}, \mcdot{}>
, \%2
, inl <\mcdot{}, \mcdot{}> >
else let info,$_{\000C}$ = r x1
in case info
of inl(y) =>
let ev,$_\mbackslash{}ff\000C7b}$,$_{}$ = y in
let x1,y = ev
in if y2=2 y
then if x=x1
then ...
else ...
else (inr (i
+ 1) )
| inr($_\mbackslash{}ff7\000Cb}$) =>
let ev,$_\mbackslash{}ff\000C7b}$,$_{}$ = "???" in
let x1,y = ev
in if y2=2 y
then if x=x1
then ...
else ...
else (inr (i
+ 1) )
else let info,S = r x1
in (\mlambda{}$_{}$.c\000Case info
of inl(y) =>
let ev,z,m = y in
let x2,y = ev
in if y1=2 y
then let info,$\mbackslash{}f\000Cf5f{}$ = $_{}$
in case info
of inl(y1) =>
...
| inr($\mbackslash{}\000Cff5f{}$) =>
...
else (inr (i + 1) )
| inr(z) =>
let ev,z,m = "???" in
let x2,y = ev
in if y1=2 y
then let info,$\mbackslash{}f\000Cf5f{}$ = $_{}$
in case info
of inl(y1) =>
...
| inr($\mbackslash{}\000Cff5f{}$) =>
if x=x2
then ...
else ...
else (inr (i + 1) ))
<info, S>
| inr($_{}$) =>
inr (i + 1) ;
inr 0 ;
prior-run-events(r;let x,$_{}$ =\000C y
in x))
of inl(trp) =>
inl let $_{}$,\%6 =
I(zzj) where I(\malpha{}) =
when $_{}$ = \malpha{} < 0, $_{\mbackslash{}ff7\000Cd$ = I(\malpha{}+1). \mlambda{}$_{}$.\mcdot{}
when \malpha{} = 0.
\mlambda{}$_{}$,$_{}$,$\000C_{}$.
<\mlambda{}$_{}$.(inr <\mcdot{}, \mcdot{}> )
, \mlambda{}\%.case \%
of inl(\%1) =>
let $_{}$,$_{}\mbackslash{}\000Cff24,$_{}$,$_{}$ = \%1
in \mcdot{}
| inr(\%2) =>
let $_{}$,$_{}\mbackslash{}\000Cff24 = \%2
in \mcdot{}
>
when zzj = \malpha{} > 0, \% = I(\malpha{}-1).
\mlambda{}$_{}$.if zzj=0
then \mlambda{}$_{}$,$_{}\mbackslash{}\000Cff24.<\mlambda{}$_{}$.\mcdot{}, \mlambda{}$_{}$.\mcdot{}>
else (\mlambda{}x,y@0.
<\mlambda{}\%@0.let z,\%7,\%8 = \%@0 in
inl let \%10,$_{}$ = \000C\% (\mlambda{}.\mcdot{}) z y@0
in case \%10 \%8
of inl(\%9) =>
let z@0,$_{}\mbackslash{}ff2\000C4,\%13,\%14 = \%9
in <z@0
, \mcdot{}
, if zzj - 1=0
then \mcdot{}
else <z, \%7, \%13>
, \%14>
| inr(\%10) =>
let $_{}$,\mbackslash{}f\000Cf24_{}$ = \%10
in <x, \mcdot{}, \mcdot{}, \%7>
, \mlambda{}\%@0.case \%@0
of inl(\%6) =>
let z,$_{}$,\%10,\%1\000C1 = \%6
in if zzj=1
then <y@0, \%11, \mcdot{}>
else if zzj - 1=0
then \mcdot{}
else ...
| inr(\%7) =>
let $_{}$,$\mbackslash{}ff\000C5f{}$ = \%7
in any \mcdot{}
>)
end where
(\mlambda{}.\mcdot{})
x
y
in \%6
(inl let z,\%10 = trp
in <z, let $_{}$,\%13,\%14 = \%10 in <\000C\mcdot{}, \%13, \%14>> )
| inr($_{}$) =>
inr (\mlambda{}$_{}$.any \mcdot{})
end where
(\mlambda{}.\mcdot{})
e1
e2);1;let x,$_{}$ = e2
in x + 1)
of inl(\%2) =>
inl let k,\%6 = \%2
in <k, \%6>
| inr($_{}$) =>
inr (\mlambda{}$_{}$.any \mcdot{})
Date html generated:
2012_01_23-PM-12_43_47
Last ObjectModification:
2011_12_14-PM-12_00_22
Home
Index