Nuprl Definition : intlex
l1 ≤_lex l2 == eval n1 = ||l1|| in eval n2 = ||l2|| in n1 <z n2 ∨b((n1 =z n2) ∧b intlex-aux(l1;l2))
Definitions occuring in Statement :
intlex-aux: intlex-aux(l1;l2),
length: ||as||,
bor: p ∨bq,
band: p ∧b q,
callbyvalue: callbyvalue,
lt_int: i <z j,
eq_int: (i =z j)
Definitions occuring in definition :
callbyvalue: callbyvalue,
length: ||as||,
bor: p ∨bq,
lt_int: i <z j,
band: p ∧b q,
eq_int: (i =z j),
intlex-aux: intlex-aux(l1;l2)
FDL editor aliases :
intlex
Latex:
l1 \mleq{}\_lex l2 ==
eval n1 = ||l1|| in
eval n2 = ||l2|| in
n1 <z n2 \mvee{}\msubb{}((n1 =\msubz{} n2) \mwedge{}\msubb{} intlex-aux(l1;l2))
Date html generated:
2017_09_29-PM-05_48_56
Last ObjectModification:
2017_05_31-AM-10_27_05
Theory : list_0
Home
Index