Nuprl Definition : llex-le
llex-le(A;a,b.<[a; b]) == λL1,L2. ((L1 llex(A;a,b.<[a; b]) L2) ∨ (L1 = L2 ∈ (A List)))
Definitions occuring in Statement :
llex: llex(A;a,b.<[a; b]),
list: T List,
infix_ap: x f y,
or: P ∨ Q,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
or: P ∨ Q,
infix_ap: x f y,
llex: llex(A;a,b.<[a; b]),
equal: s = t ∈ T,
list: T List
FDL editor aliases :
llex-le
Latex:
llex-le(A;a,b.<[a; b]) == \mlambda{}L1,L2. ((L1 llex(A;a,b.<[a; b]) L2) \mvee{} (L1 = L2))
Date html generated:
2017_02_20-AM-10_55_25
Last ObjectModification:
2017_02_02-PM-09_24_19
Theory : general
Home
Index