[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
# .	list-data	f	List('a) → Nat
# .	set-basic	f	Set('a) → Nat
#oc	list-perm	f	'a × List('a) → Nat
. '	list	f	'a → List('a)
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	'a × List('a) → List('a)
. + .	list	f	List('a) × List('a) → List('a)
. + .	list	f	List('a) × 'a → List('a)
. ++ .	list-dup	f	List('a) × 'a → List('a)
. ++ .	set-basic	f	Set('a) × 'a → Set('a)
. +1	nat-basic	f	Nat → Nat
. +2 .	list	f	'a × 'a → List('a)
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -- .	set-union	f	Set('a) × 'a → Set('a)
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	list-del	f	List('a) × 'a → List('a)
. -l .	list-del	f	List('a) × 'a → List('a)
. -p .	list-del	f	List('a) × Nat → List('a)
. .FO?	FOW	p	FOW
. .FO?	Bevent	p	Bevent
. .FOWs ( . )	FLIT-preds	f	List(Bevent) × T × L → List(FOW)
. .FOs?	FLIT-preds	p	(T → Type(List(Bevent)))
. .W?	FOW	p	FOW
. .W?	Bevent	p	Bevent
. .butlast	list-last	pf	List('a) → List('a) with λ x. x ≠ []
. .count ( . )	filter-count	f	List('a) × ('a → Bool) → Nat
. .count ( . )	filter-count	pf	List('a) × Nat × Nat × ('a → Bool) → Nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x
. .distinct	list-dup	f	List('a) → List('a)
. .drop ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .dropRight ( . )	list-last	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .exists ( . )	forall-indexWhere	p	List('a) × ('a → Type(Bool))
. .filter ( . )	filter-count	f	List('a) × ('a → Bool) → List('a)
. .filter ( . )	set-union	f	Set('a) × ('a → Bool) → Set('a)
. .foldLeft ( . )	list	f	List('a) × 'b × ('b × 'a → 'b) → 'b
. .forall ( . )	forall-indexWhere	p	List('a) × ('a → Type(Bool))
. .head	list-data	pf	List('a) → 'a with λ x. x ≠ []
. .indexOf ( . )	list-del	f	List('a) × 'a → Nat
. .indexWhere ( . )	forall-indexWhere	f	List('a) × ('a → Bool) → Nat
. .l	Bevent	pf	Bevent → L with λ be. be.FO? ∨ be.W?
. .last	list-last	pf	List('a) → 'a with λ x. x ≠ []
. .map ( . )	list	f	List('a) × ('a → 'b) → List('b)
. .map ( . )	set-union	f	Set('a) × ('a → 'b) → Set('b)
. .sublist ( . )	list-del	pf	List('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x
. .tail	list-data	pf	List('a) → List('a) with λ x. x ≠ []
. .take ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .takeRight ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .tid	FOW	f	FOW → T
. .v	Bevent	pf	Bevent → V with λ be. be.W?
. .val	FOW	pf	FOW → V with λ fow. fow.W?
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List('a) × List('a)
. > .	nat	p	Nat × Nat
. [ . := . ]	list-getput	pf	List('a) × Nat × 'a → List('a) with λ x, n, a. n < # x
. [ . ]	list-getput	pf	List('a) × Nat → 'a with λ x, n. n < # x
. \ .	list-set	f	List('a) × List('a) → List('a)
. \ .	set-union	f	Set('a) × Set('a) → Set('a)
. \| .	FLITPSC-preds	f	List(FOW) × T → List(FOW)
. \|FO	FLITPSC-preds	f	List(FOW) → List(FOW)
. \|SF .	FLIT-preds	f	List(Bevent) × L → List(Bevent)
. \|W	FLITPSC-preds	f	List(FOW) → List(FOW)
. \|WL .	FLIT-preds	f	List(Bevent) × L → List(Bevent)
. ∈ .	list	p	'a × List('a)
. ∈ .	set-basic	p	'a × Set('a)
. ∩ .	set-union	f	Set('a) × Set('a) → Set('a)
. ∪ .	list-set	f	List('a) × List('a) → List('a)
. ∪ .	set-union	f	Set('a) × Set('a) → Set('a)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	list-set	p	List('a) × List('a)
. ⊆ .	set-basic	p	Set('a) × Set('a)
. ⊆m .	list-perm	p	List('a) × List('a)
. ⊑ .	list-last	p	List('a) × List('a)
. ⊒ .	list-last	p	List('a) × List('a)
. ⊒w .	FLIT-preds	p	List(Bevent) × List(Bevent)
. ⊕ .	FLITPSC-preds	f	V × List(FOW) → V
. ⊕ .	FLITPSC-preds	f	(L → V) × (L → List(FOW)) → L → V
. ⊕ .	FLIT-preds	f	V × List(Bevent) → V
. ⊕ .	FLIT-preds	f	(L → V) × List(Bevent) → L → V
. intersect .	list-set	f	List('a) × List('a) → List('a)
. zip .	filter-count	f	List('a) × List('b) → List(('a, 'b))
[]	list-data	c	List('a)
{ . }	set-union	f	'a → Set('a)
∅	set-basic	c	Set('a)
∅	memory	f	L → V
Bevent	Bevent	s
FO	FOW	f	T → FOW
FO	Bevent	f	L → Bevent
FOFollowsW	FLITPSC-preds	p	T × List(FOW)
FOFollowsW	FLIT-preds	p	T × List(Bevent) × (L → Type(List(FOW))) × L
FOFollowsW	FLIT-preds	p	T × List(Bevent) × List(FOW) × L
FOW	FOW	s
L	memory	s
List	list-data	s
Nat	nat-basic	s
O	memory	c	V
SF	Bevent	c	Bevent
SFTrailing	FLIT-preds	p	(T → Type(List(Bevent)))
Set	set-basic	s
T	memory	s
V	memory	s
W	FOW	f	V × T → FOW
W	Bevent	f	L × V → Bevent
be	FLIT-preds	v	Bevent
bel	FLIT-preds	v	List(Bevent)
bq	FLIT-preds	v	T → List(Bevent)
ctrok	FLITPSC-preds	p	(L → Type(Nat)) × (L → Type(Set(T)))
disj	list-dup	p	List('a) × List('a)
disjoint	set-union	p	Set('a) × Set('a)
dups	list-dup	p	List('a)
fillfirst	list-last	f	Nat × 'a × List('a) → List('a)
fow	FLIT-preds	v	FOW
fowl	FLIT-preds	v	List(FOW)
frome	list-del	f	List('a) × 'a → List('a)
isPropFO	FLIT-preds	p	Nat × L × List(Bevent)
l	FLIT-preds	v	L
m	FLIT-preds	v	Nat
mem	FLIT-preds	v	L → V
mklist	list-last	f	'a × Nat → List('a)
n	FLIT-preds	v	Nat
noPending	FLITPSC-preds	p	T × (L → Type(List(FOW)))
noPending	FLIT-preds	p	T × (T → Type(List(Bevent))) × (L → Type(List(FOW)))
noPendingW	FLITPSC-preds	p	T × (L → Type(List(FOW)))
noPendingW	FLIT-preds	p	T × (T → Type(List(Bevent))) × (L → Type(List(FOW)))
notMember	FLITPSC-preds	p	T × (L → Type(Set(T)))
oneMember	FLITPSC-preds	p	T × L × (L → Type(Set(T)))
onePendingW	FLITPSC-preds	p	T × L × (L → Type(List(FOW)))
p	FLIT-preds	v	L → List(FOW)
pendingOk	FLITPSC-preds	p	(L → Type(List(FOW)))
pendingOk	FLIT-preds	p	(T → Type(List(Bevent))) × (L → Type(List(FOW)))
perm	list-perm	p	List('a) × List('a)
pq	FLIT-preds	v	L → List(FOW)
readFOsOk	FLIT-preds	p	(T → Type(List(Bevent))) × (L → Type(Set(T)))
rely	FLIT-preds	p	T × (L → Type(List(FOW))) × (T → Type(List(Bevent))) × (L → Type(List(FOW))) × (T → Type(List(Bevent)))
rely	FLIT-preds	p	T × L × List(FOW) × List(Bevent) × List(FOW) × List(Bevent)
relyp	FLITPSC-preds	p	T × List(FOW) × List(FOW)
relyp	FLITPSC-preds	p	T × (L → Type(List(FOW))) × (L → Type(List(FOW)))
relyws	FLITPSC-preds	p	T × (L → Type(Set(T))) × (L → Type(Set(T)))
relyws	FLITPSC-preds	p	T × Set(T) × Set(T)
rev	list-last	f	List('a) → List('a)
rfo	FLIT-preds	v	T → List(Bevent)
t	FLIT-preds	v	T
v	FLIT-preds	v	V
writers	FLIT-preds	v	L → Set(T)
writersOk	FLITPSC-preds	p	(L → Type(List(FOW))) × (L → Type(Set(T)))
writersOk	FLIT-preds	p	(T → Type(List(Bevent))) × (L → Type(List(FOW))) × (L → Type(Set(T)))