[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol Specification Kind Type
# .lp-arrayflp-array → nat
# .nat-list-setfnat-set → nat
# .nat-list-setfnat-list → nat
. 'nat-list-setfnat → nat-list
. + .nat-basicfnat × nat → nat
. + .nat-list-setfnat × nat-list → nat-list
. + .nat-list-setfnat-list × nat → nat-list
. + .nat-list-setfnat-list × nat-list → nat-list
. ++ .nat-list-setfnat-set × nat → nat-set
. ++ .nat-list-setfnat-list × nat → nat-list
. +1nat-basicfnat → nat
. +2 .nat-list-setfnat × nat → nat-list
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -- .nat-list-setfnat-set × nat → nat-set
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. -1l .nat-list-setfnat-list × nat → nat-list
. -l .nat-list-setfnat-list × nat → nat-list
. -p .nat-list-setfnat-list × nat → nat-list
. .butlastnat-list-setpfnat-list → nat-list with λ nx. nx ≠ []
. .filter ( . )array-indicesfnat-set × (nat → bool) → nat-set
. .flagslpropsflprops → lpropflags
. .flags:= .lpropsflprops × lpropflags → lprops
. .gcheapidxlpropsflprops → nat
. .gcheapidx:= .lpropsflprops × nat → lprops
. .headnat-list-setpfnat-list → nat with λ nx. nx ≠ []
. .indicesWhere ( . )lp-arrayflp-array × (lprops → bool) → nat-list
. .indicesWhere ( . )lp-arrayflp-array × (lprops → bool) × nat → nat-list
. .lastnat-list-setpfnat-list → nat with λ nx. nx ≠ []
. .map ( . )lp-arrayflp-array × (lprops → lprops) → lp-array
. .map ( . )array-indicesfnat-set × (nat → nat) → nat-set
. .mapIf ( . )lp-arrayflp-array × (lprops → bool) × (lprops → lprops) → lp-array
. .mapIf ( . )lp-arrayflp-array × (lprops → bool) × (lprops → lprops) × nat → lp-array
. .mapIndices ( . )lp-arrayflp-array × nat-list × (lprops → lprops) → lp-array
. .mapIndices ( . )lp-arrayflp-array × nat-set × (lprops → lprops) → lp-array
. .ref-sizelpropsflprops → nat
. .ref-size:= .lpropsflprops × nat → lprops
. .sizelpropsflprops → nat
. .size:= .lpropsflprops × nat → lprops
. .tailnat-list-setpfnat-list → nat-list with λ nx. nx ≠ []
. .toSetnat-list-setfnat-list → nat-set
. < .nat-list-lesspnat-list × nat
. < .nat-basicpnat × nat
. < .nat-list-setpnat-list × nat-list
. > .natpnat × nat
. [ . ]lp-arraypflp-array × nat × lprops → lp-array with λ lpt, n, lp. n < # lpt
. [ . ]lp-arraypflp-array × nat → lprops with λ lpt, n. n < # lpt
. [ . ]nat-list-setpfnat-list × nat × nat → nat-list with λ nx, n, n0. n < # nx
. [ . ]nat-list-setpfnat-list × nat → nat with λ nx, n. n < # nx
. \ .nat-list-setfnat-set × nat-set → nat-set
. ∈ .lp-arrayplprops × lp-array
. ∈ .nat-list-setpnat × nat-list
. ∈ .nat-list-setpnat × nat-set
. ∩ .nat-list-setfnat-set × nat-set → nat-set
. ∪ .nat-list-setfnat-set × nat-set → nat-set
. ≤ .natpnat × nat
. ≥ .natpnat × nat
. ⊆ .nat-list-setpnat-set × nat-set
. ⊑ .nat-list-setpnat-list × nat-list
. ⊒ .nat-list-setpnat-list × nat-list
[]nat-list-setcnat-list
{ . }nat-list-setfnat → nat-set
φlp-arrayvlprops → bool
φnarray-indicesvnat → bool
∅nat-list-setcnat-set
LP_FREElpropsclpropflags
LP_GROUP_NODESlpropsclpropflags
LP_INDEX_NODESlpropsclpropflags
butlastnnat-list-setpfnat × nat-list → nat-list with λ n, nx. n ≤ # nx
cmplp-arraypplp-array × lprops × nat × nat with λ lpt, lp, m, n. m + n ≤ # lpt
cmplp-arraypplp-array × nat × lp-array × nat × nat with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0
copylp-arraypflp-array × nat × lp-array × nat × nat → lp-array with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0
disjnat-list-setpnat-list × nat-list
dropnnat-list-setfnat × nat-list → nat-list
dupsnat-list-setpnat-list
filllp-arraypflp-array × lprops × nat × nat → lp-array with λ lpt, lp, n, m. n + m ≤ # lpt
filllp-arrayflp-array × lprops → lp-array
fillfirstnat-list-setfnat × nat × nat-list → nat-list
firstnnat-list-setpfnat × nat-list → nat-list with λ n, nx. n ≤ # nx
fnarray-indicesvnat → nat
fromenat-list-setfnat-list × nat → nat-list
id○lp-arrayplp-array × lp-array × nat
idrangelp-arraypplp-array × nat × nat with λ lpt, m, n. m + n ≤ # lpt
lastnnat-list-setpfnat × nat-list → nat-list with λ n, nx. n ≤ # nx
lplpropsvlprops
lp-arraylp-arrays
lp0lpropsvlprops
lp1lp-arrayvlprops
lpflpropsvlpropflags
lpf0lpropsvlpropflags
lpropflagslpropss
lpropslpropss
lptlp-arrayvlp-array
lpt0lp-arrayvlp-array
lpt1lp-arrayvlp-array
lpt2lp-arrayvlp-array
lptfunlp-arrayvlprops → lprops
mnat-basicvnat
m0lpropsvnat
m1lpropsvnat
m2lpropsvnat
m3lpropsvnat
m4lpropsvnat
mklistnat-list-setfnat × nat → nat-list
mklplpropsfnat × nat × lpropflags × nat → lprops
mklparraylp-arrayfnat → lp-array
nnat-basicvnat
n0nat-basicvnat
n1nat-basicvnat
n2nat-list-setvnat
n3nat-list-setvnat
n4nat-list-setvnat
n5nat-list-setvnat
natnat-basics
nat-listnat-list-sets
nat-setnat-list-sets
nsnat-list-setvnat-set
ns0nat-list-setvnat-set
ns1nat-list-setvnat-set
ns2nat-list-setvnat-set
nxnat-list-setvnat-list
nx0nat-list-setvnat-list
nx1nat-list-setvnat-list
nynat-list-setvnat-list
nznat-list-setvnat-list
posnat-list-setfnat × nat-list → nat
prefixnnat-list-setfnat × nat-list → nat-list
restnnat-list-setpfnat × nat-list → nat-list with λ n, nx. n ≤ # nx
revlp-arraypflp-array × nat → lp-array with λ lpt, n. n ≤ # lpt
revlp-arrayflp-array → lp-array
revnat-list-setfnat-list → nat-list
rmdupnat-list-setfnat-list → nat-list
slicenat-list-setfnat × nat × nat-list → nat-list
subarraylp-arraypflp-array × nat × nat → lp-array with λ lpt, m, n. m + n ≤ # lpt
sublistnat-list-setpfnat × nat × nat-list → nat-list with λ n, m, nx. n + m ≤ # nx
valid-indiceslp-arrayplp-array × nat-list