[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,

Theorem base for Specification node-index-restrict

This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.

Name: Sequent: Type:
in-le ⊦ key0 ∈ ri |≤ key1 ↔ key0 ∈ ri ∧ ¬ key1 < key0 An Axiom
at-le ⊦ ¬ key1 < key0 ∧ key0 ∈ ri → (ri |≤ key1)[key0] = ri[key0] An Axiom
in-gt ⊦ key0 ∈ ri |> key1 ↔ key0 ∈ ri ∧ key1 < key0 An Axiom
at-gt ⊦ key1 < key0 ∧ key0 ∈ ri → (ri |> key1)[key0] = ri[key0] An Axiom
at-le-lt ⊦ key0 < key1 ∧ key0 ∈ ri → (ri |≤ key1)[key0] = ri[key0] A User Theorem
del-gt ⊦ key1 < key0 → (ri -- key0) |> key1 = (ri |> key1) -- key0 A User Theorem
del-le ⊦ ¬ key1 < key0 → (ri -- key0) |≤ key1 = (ri |≤ key1) -- key0 A User Theorem
deln-gt ⊦ ¬ key1 < key0 → (ri -- key0) |> key1 = ri |> key1 A User Theorem
deln-le ⊦ key1 < key0 → (ri -- key0) |≤ key1 = ri |≤ key1 A User Theorem
drop-gt ⊦ ¬ key1 < key0 → ri[key0, adr] |> key1 = ri |> key1 A User Theorem
drop-le ⊦ key1 < key0 → ri[key0, adr] |≤ key1 = ri |≤ key1 A User Theorem
gt-emp ⊦ ∅ |> key = ∅ A User Theorem
le-emp ⊦ ∅ |≤ key = ∅ A User Theorem
put-gt ⊦ key1 < key0 → ri[key0, adr] |> key1 = (ri |> key1)[key0, adr] A User Theorem
put-le ⊦ ¬ key1 < key0 → ri[key0, adr] |≤ key1 = (ri |≤ key1)[key0, adr] A User Theorem
restrict-gt1 ⊦ key0 < key1 → ri |> key0 |> key1 = ri |> key1 A User Theorem
restrict-gt2 ⊦ key1 < key0 → ri |> key0 |> key1 = ri |> key0 A User Theorem
restrict-gt3 ⊦ ¬ key0 < key1 → ri |> key0 |> key1 = ri |> key0 A User Theorem
restrict-gt4 ⊦ ¬ key1 < key0 → ri |> key0 |> key1 = ri |> key1 A User Theorem
restrict-le1 ⊦ key0 < key1 → ri |≤ key0 |≤ key1 = ri |≤ key0 A User Theorem
restrict-le2 ⊦ key1 < key0 → ri |≤ key0 |≤ key1 = ri |≤ key1 A User Theorem
restrict-le3 ⊦ ¬ key0 < key1 → ri |≤ key0 |≤ key1 = ri |≤ key1 A User Theorem
restrict-le4 ⊦ ¬ key1 < key0 → ri |≤ key0 |≤ key1 = ri |≤ key0 A User Theorem
restrict-norm ⊦ (ri |≤ key1) |> key0 = (ri |> key0) |≤ key1 A User Theorem