| Symbol | Specification | Kind | Type |
|---|
| # . | set-basic | f | Set('a) → Nat |
| . + . | nat-basic | f | Nat × Nat → Nat |
| . ++ . | set-basic | f | Set('a) × 'a → Set('a) |
| . +1 | nat-basic | f | Nat → Nat |
| . - . | nat | pf | Nat × Nat → Nat with λ n, m. n ≥ m |
| . -1 | nat-basic | pf | Nat → Nat with λ n. n ≠ 0 |
| . .b | Set | pp | SetAction with λ a.
(∃ tid, b. a = ARetMember(tid, b)) ∨ (∃ tid, b. a = ARetInsert(tid, b))
∨ (∃ tid, b. a = ADoInsert(tid, b)) |
| . .e | Set | pf | SetAction → Elem with λ a. (∃ tid, e. a = AInvMember(tid, e)) ∨ (∃ tid, e. a = AInvInsert(tid, e)) |
| . .gstate | Set | f | SetState → SetGState |
| . .gstate:= . | Set | f | SetState × SetGState → SetState |
| . .lb | Set | p | SetLState |
| . .lb:= . | Set | f | SetLState × Bool → SetLState |
| . .le | Set | f | SetLState → Elem |
| . .le:= . | Set | f | SetLState × Elem → SetLState |
| . .lsf | Set | f | SetState → Tid → SetLState |
| . .lsf:= . | Set | f | SetState × (Tid → SetLState) → SetState |
| . .pcf | Set | f | SetState → Tid → SetPC |
| . .pcf:= . | Set | f | SetState × (Tid → SetPC) → SetState |
| . .set | Set | f | SetGState → Set(Elem) |
| . .set:= . | Set | f | SetGState × Set(Elem) → SetGState |
| . .tid | Set | f | SetLState → Tid |
| . .tid | Set | pf | SetAction → Tid with λ a. a ≠ τ |
| . .tid:= . | Set | f | SetLState × Tid → SetLState |
| . < . | nat-basic | p | Nat × Nat |
| . > . | nat | p | Nat × Nat |
| . ∈ . | set-basic | p | 'a × Set('a) |
| . ≤ . | nat | p | Nat × Nat |
| . ≥ . | nat | p | Nat × Nat |
| . ⊆ . | set-basic | p | Set('a) × Set('a) |
| τ | Set | c | SetAction |
| ∅ | set-basic | c | Set('a) |
| ⊥ | Set | c | Elem |
| ADoInsert | Set | f | Tid × Bool → SetAction |
| ADoMember | Set | f | Tid → SetAction |
| AInvInsert | Set | f | Tid × Elem → SetAction |
| AInvMember | Set | f | Tid × Elem → SetAction |
| ARetInsert | Set | f | Tid × Bool → SetAction |
| ARetMember | Set | f | Tid × Bool → SetAction |
| DOINSERT | Set | pr | Bool × Elem : Bool × Set(Elem) |
| DOMEMBER | Set | pr | Elem × Set(Elem) : Bool |
| Elem | Set | s | |
| INVINSERT | Set | pr | Elem : Elem |
| INVMEMBER | Set | pr | Elem : Elem |
| Nat | nat-basic | s | |
| RETINSERT | Set | pr | Bool : : Bool |
| RETMEMBER | Set | pr | Bool : : Bool |
| Set | set-basic | s | |
| SetAction | Set | s | |
| SetGInv | Set | p | SetGState |
| SetGState | Set | s | |
| SetInv | Set | p | SetGState × (Tid → Type(SetLState)) × (Tid → Type(SetPC)) |
| SetLInv | Set | p | SetGState × SetLState × SetPC |
| SetLState | Set | s | |
| SetPC | Set | s | |
| SetRely | Set | p | SetGState × Tid × SetGState |
| SetState | Set | s | |
| Tid | tid | s | |
| a | Set-proofs | v | SetAction |
| b | Set-proofs | v | Bool |
| dummytid | tid | c | Tid |
| e | Set-proofs | v | Elem |
| gs | Set-proofs | v | SetGState |
| gstate | Set-proofs | v | SetGState |
| gstepf | Set | f | SetGState × SetLState × SetPC × SetAction → SetGState |
| idle | Set | c | SetPC |
| invInsert | Set | c | SetPC |
| invMember | Set | c | SetPC |
| lb | Set-proofs | v | Bool |
| le | Set-proofs | v | Elem |
| ls | Set-proofs | v | SetLState |
| lsf | Set-proofs | v | Tid → SetLState |
| lstep | Set | p | SetGState × SetLState × SetPC × SetAction × SetGState × SetLState × SetPC |
| lstepf | Set | f | SetGState × SetLState × SetPC × SetAction → SetLState |
| mkgs | Set | f | Set(Elem) → SetGState |
| mkls | Set | f | Tid × Elem × Bool → SetLState |
| mkstate | Set | f | SetGState × (Tid → SetLState) × (Tid → SetPC) → SetState |
| pc | Set-proofs | v | SetPC |
| pcf | Set-proofs | v | Tid → SetPC |
| pcstepf | Set | f | SetGState × SetLState × SetPC × SetAction → SetPC |
| pre | Set | p | SetGState × SetLState × SetPC × SetAction |
| retInsert | Set | c | SetPC |
| retMember | Set | c | SetPC |
| s | Set-proofs | v | SetState |
| set | Set-proofs | v | Set(Elem) |
| setInit | Set | p | SetState |
| setStep | Set | p | SetState × SetAction × SetState |
| tid | Set-proofs | v | Tid |