This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| Min-in | ⊦ s ≠ ∅ → s.min ∈ s | An Axiom |
| Min-min | ⊦ a ∈ s → ¬ a < s.min | An Axiom |
| Butmin | ⊦ s ≠ ∅ → s.butmin = s -- s.min | An Axiom |
| Max-in | ⊦ s ≠ ∅ → s.max ∈ s | An Axiom |
| Max-max | ⊦ a ∈ s → ¬ s.max < a | An Axiom |
| Butmax | ⊦ s ≠ ∅ → s.butmax = s -- s.max | An Axiom |
| Less | ⊦ a < s ↔ (∀ b. b ∈ s → a < b) | An Axiom |
| Greater | ⊦ s < a ↔ (∀ b. b ∈ s → b < a) | An Axiom |
| bm-shift | 1 < # s ⊦ s.butmin.butmax = s.butmax.butmin | A User Theorem |
| bmax-def | ⊦ s ≠ ∅ → s -- s.max = s.butmax | A User Theorem |
| bmax-empty | ⊦ s.butmax = ∅ ∧ s ≠ ∅ → # s = 1 | A User Theorem |
| bmax-in | ⊦ b ∈ s → (b ∈ s.butmax ↔ b ≠ s.max) | A User Theorem |
| bmax-in-01 | ⊦ s ≠ ∅ → ¬ s.max ∈ s.butmax | A User Theorem |
| bmax-in-02 | ⊦ a ∈ s.butmax ∧ s ≠ ∅ → a ∈ s | A User Theorem |
| bmax-max | ⊦ 1 < # s → ¬ s.max < s.butmax.max | A User Theorem |
| bmax-min | ⊦ 1 < # s → s.butmax.min = s.min | A User Theorem |
| bmax-one | ⊦ (∅ ++ a).butmax = ∅ | A User Theorem |
| bmax-one-01 | ⊦ # s = 1 → s.butmax = ∅ | A User Theorem |
| bmax-shift | s -- a ≠ ∅, a ≠ s.max ⊦ (s -- a).butmax = s.butmax -- a | A User Theorem |
| bmin-bin | ⊦ s ≠ ∅ ∧ # s ≠ 1 → s.butmin.min ∈ s | A User Theorem |
| bmin-bls | ⊦ s ≠ ∅ ∧ s.butmin ≠ ∅ → s.min < s.butmin.min | A User Theorem |
| bmin-bneq | ⊦ s ≠ ∅ ∧ # s ≠ 1 → s.min ≠ s.butmin.min | A User Theorem |
| bmin-del | ⊦ s ≠ ∅ → s.butmin -- s.min = s.butmin | A User Theorem |
| bmin-del-01 | ⊦ s ≠ ∅ → s.butmin -- a -- s.min = s.butmin -- a | A User Theorem |
| bmin-del-02 | ⊦ s ≠ ∅ → s -- a -- s.min = s.butmin -- a | A User Theorem |
| bmin-del-03 | ⊦ s -- a ≠ ∅ ∧ a ≠ s.min → (s -- a).butmin = s.butmin -- a | A User Theorem |
| bmin-del-04 | ⊦ s ≠ ∅ ∧ a ≠ s.min → (s -- a).butmin = s.butmin -- a | A User Theorem |
| bmin-del-05 | ⊦ s ≠ ∅ → s -- s.min = s.butmin | A User Theorem |
| bmin-eq | ⊦ s = s.butmin ++ s.min ↔ s ≠ ∅ | A User Theorem |
| bmin-eq-01 | ⊦ s.butmin = s0.butmin ∧ s ≠ s0 ∧ s ≠ ∅ ∧ s0 ≠ ∅ → s.min ≠ s0.min | A User Theorem |
| bmin-f | ⊦ s.min ∈ s.butmin → s = ∅ | A User Theorem |
| bmin-in | ⊦ ¬ a ∈ s.butmin → (a ∈ s ↔ ¬ ¬(a = s.min ∧ s ≠ ∅)) | A User Theorem |
| bmin-in-01 | ⊦ a ∈ s ∧ a ≠ s.min → a ∈ s.butmin | A User Theorem |
| bmin-in-02 | ⊦ ¬ a ∈ s.butmin → (a ∈ s ↔ a = s.min ∧ s ≠ ∅) | A User Theorem |
| bmin-in-03 | ⊦ a ∈ s.butmin ∧ s ≠ ∅ ↔ a ∈ s ∧ a ≠ s.min | A User Theorem |
| bmin-in-04 | s.butmin ≠ ∅ ⊦ s ⊆ s0 ∧ s ≠ ∅ → s.butmin.min ∈ s0 | A User Theorem |
| bmin-intempty | ⊦ s ∩ s0 = ∅ ∧ s ≠ ∅ → s.butmin ∩ s0 = ∅ | A User Theorem |
| bmin-min | ⊦ s.butmin.min < s.min ∧ s ≠ ∅ → s.butmin = ∅ | A User Theorem |
| bmin-nin | ⊦ ¬ a ∈ s ∧ s ≠ ∅ → ¬ a ∈ s.butmin | A User Theorem |
| bmin-nin-01 | ⊦ s ≠ ∅ → ¬ s.min ∈ s.butmin | A User Theorem |
| bmin-nin-02 | ⊦ ¬ a ∈ s.butmin ∧ a ≠ s.min → ¬ a ∈ s | A User Theorem |
| bmin-one | ⊦ (∅ ++ a).butmin = ∅ | A User Theorem |
| bmin-one-01 | ⊦ s ≠ ∅ ∧ s.butmin = ∅ → # s = 1 | A User Theorem |
| bmin-one-02 | ⊦ s.butmin = ∅ → (a ∈ s ↔ a = s.min ∧ s ≠ ∅) | A User Theorem |
| bmin-one-03 | ⊦ # s = 1 → s.butmin = ∅ | A User Theorem |
| bmin-size | ⊦ # s.butmin < # s ↔ s ≠ ∅ | A User Theorem |
| bmin-size-01 | ⊦ s ≠ ∅ → # s.butmin = # s - 1 | A User Theorem |
| bmin-size-02 | ⊦ s ≠ ∅ → # s.butmin + 1 = # s | A User Theorem |
| bmin-sub | ⊦ s ⊆ s0 ∧ s ≠ ∅ → s.butmin ⊆ s0 | A User Theorem |
| bmin-sub-01 | ⊦ # s = 2 ∧ s ⊆ s0 → s.butmin.min ∈ s0 | A User Theorem |
| bmin-sub-02 | ⊦ # s = 2 ∧ s.butmin.min ∈ s0 ∧ s.min ∈ s0 → s ⊆ s0 | A User Theorem |
| bmin-sub-03 | ⊦ s ≠ ∅ → s.butmin ⊆ s | A User Theorem |
| bmin-sub-04 | ⊦ s ⊆ s0 ∧ s0 ≠ ∅ → (s ⊆ s0.butmin ↔ ¬ s0.min ∈ s) | A User Theorem |
| bmin-sub-05 | ⊦ s ⊆ s0 ∧ s ≠ ∅ → s.butmin ⊆ s0.butmin | A User Theorem |
| bmin-two | ⊦ # s = 2 → s.butmin.min ∈ s | A User Theorem |
| bmin-two-01 | ⊦ a < b → (∅ ++ a ++ b).butmin = ∅ ++ b | A User Theorem |
| bmin-two-02 | ⊦ a < b → (∅ ++ b ++ a).butmin = ∅ ++ b | A User Theorem |
| bmin-two-03 | ⊦ a < b → (∅ ++ a ++ b).butmin = ∅ ++ b ∧ (∅ ++ a ++ b).min = a | A User Theorem |
| bmin-two-04 | ⊦ # s = 2 → ∅ ++ s.min ++ s.butmin.min = s | A User Theorem |
| bmin-two-05 | ⊦ # s = 2 → s.min ≠ s.butmin.min | A User Theorem |
| bmin-two-06 | ⊦ # s = 2 → s.butmin.min ∈ s.butmin | A User Theorem |
| bmin-two-07 | ⊦ # s = 2 → s.butmin ≠ ∅ | A User Theorem |
| bmin-two-08 | ⊦ # s = 2 → ∅ ++ s.butmin.min ++ s.min = s | A User Theorem |
| bminmin | ⊦ s ≠ ∅ → s.butmin ++ s.min = s | A User Theorem |
| butmin-in | ⊦ a ∈ s.butmin ∧ s ≠ ∅ → a ∈ s | A User Theorem |
| butmin-ins | ⊦ s.min < a ∧ s ≠ ∅ → (s ++ a).butmin = s.butmin ++ a | A User Theorem |
| butmin-ins-01 | ⊦ a < s.min ∧ s ≠ ∅ → (s ++ a).butmin = s | A User Theorem |
| butminempty-sizeone | ⊦ s.butmin = ∅ ∧ s ≠ ∅ → # s = 1 | A User Theorem |
| diff-min | ⊦ s1 \ s0 ≠ ∅ ∧ s ⊆ s0 → ¬ (s1 \ s0).min ∈ s | A User Theorem |
| emptyset-ls | ⊦ a < ∅ | A User Theorem |
| ins-inbutmins | ⊦ a ∈ s → (a ∈ s.butmin ↔ a ≠ s.min) | A User Theorem |
| ls-add | ⊦ s < b → (¬ s ++ a < b ↔ ¬ a < b) | A User Theorem |
| ls-emptyset | ⊦ ∅ < a | A User Theorem |
| ls-rm | ⊦ s < b → s -- a < b | A User Theorem |
| max-bmin | ⊦ 1 < # s → s.butmin.max = s.max | A User Theorem |
| max-del | ⊦ s.max < (s -- a).max → s = ∅ ++ a | A User Theorem |
| max-del-01 | ⊦ a ≠ s.max ∧ s ≠ ∅ → (s -- a).max = s.max | A User Theorem |
| max-gr | ⊦ s.max < a ∧ s ≠ ∅ → ¬ a ∈ s | A User Theorem |
| max-ifins | ⊦ (s ++ a).max = (s = ∅ ⊃ a;(a < s.max ⊃ s.max;a)) | A User Theorem |
| max-in | ⊦ s ≠ ∅ → (¬ s.max ∈ s ↔ false) | A User Theorem |
| max-ins | ⊦ a < s.max ∧ s ≠ ∅ → (s ++ a).max = s.max | A User Theorem |
| max-ins-01 | ⊦ ¬ a < s.max ∧ s ≠ ∅ → (s ++ a).max = a | A User Theorem |
| max-one | ⊦ (∅ ++ a).max = a | A User Theorem |
| max-one-01 | ⊦ # s = 1 → (s = ∅ ++ s.max ↔ true) | A User Theorem |
| max-q | a ∈ s, ∀ b. b ∈ s → ¬ a < b ⊦ s.max = a | A User Theorem |
| max-subset | ⊦ s ≠ ∅ ∧ s ⊆ s0 → ¬ s0.max < s.max | A User Theorem |
| max-subset-01 | ⊦ s ≠ ∅ ∧ s ⊆ s0 → s.max ∈ s0 | A User Theorem |
| maxunion | ⊦ s ≠ ∅ → ¬ (s ∪ s0).max < s.max | A User Theorem |
| min-del | ⊦ s ≠ ∅ ∧ a ≠ s.min → (s -- a).min = s.min | A User Theorem |
| min-del-01 | ⊦ s -- a ≠ ∅ ∧ a ≠ s.min → (s -- a).min = s.min | A User Theorem |
| min-delmin | ⊦ 1 < # s → s.min < (s -- s.min).min | A User Theorem |
| min-delmin-01 | ⊦ s ≠ ∅ ∧ s ≠ ∅ ++ s.min → (s -- s.min).min ∈ s | A User Theorem |
| min-inc | s ≠ ∅ ⊦ s.min ∈ s | A User Theorem |
| min-inn | ⊦ ¬ s.min ∈ s ↔ s = ∅ | A User Theorem |
| min-ins | ⊦ s.min ∈ s ↔ s ≠ ∅ | A User Theorem |
| min-ins-01 | ⊦ a ∈ s ∧ ¬ b < a → (s ++ b).min = s.min | A User Theorem |
| min-ins-02 | ⊦ s ≠ ∅ → ¬ s.min < (s ++ a).min | A User Theorem |
| min-ins-03 | ⊦ s.min < a ∧ s ≠ ∅ → (s ++ a).min = s.min | A User Theorem |
| min-ins-04 | ⊦ ¬ s.min < a ∧ s ≠ ∅ → (s ++ a).min = a | A User Theorem |
| min-ins-05 | ⊦ s ≠ ∅ → s ++ s.min = s | A User Theorem |
| min-insert | ⊦ a < s.min ∧ s ≠ ∅ → (s ++ a).min = a | A User Theorem |
| min-intempty | ⊦ s ∩ s0 = ∅ ∧ s ≠ ∅ → (¬ ¬ s.min ∈ s0 ↔ false) | A User Theorem |
| min-less | ⊦ a ≠ s.min ∧ a ∈ s → s.min < a | A User Theorem |
| min-ls | ⊦ #(s -- s.min) < # s ↔ s ≠ ∅ | A User Theorem |
| min-one | ⊦ (∅ ++ a).min = a | A User Theorem |
| min-one-01 | ⊦ # s = 1 → ∅ ++ s.min = s | A User Theorem |
| min-q | a ∈ s, ∀ b. b ∈ s → ¬ b < a ⊦ a = s.min | A User Theorem |
| min-sub | ⊦ ¬ s.min ∈ s0 → (s ⊆ s0 ↔ s = ∅) | A User Theorem |
| min-sub-01 | ⊦ s ⊆ s0 ∧ s ≠ ∅ ∧ s0.min ∈ s → (s.min ≠ s0.min ↔ false) | A User Theorem |
| min-subset | ⊦ s ≠ ∅ ∧ s ⊆ s0 → s.min ∈ s0 | A User Theorem |
| min-two | ⊦ a < b → (∅ ++ a ++ b).min = a | A User Theorem |
| min-two-01 | ⊦ a < b → (∅ ++ b ++ a).min = a | A User Theorem |
| min-two-02 | ⊦ # s = 2 ∧ a ∈ s ∧ a ≠ s.min → ∅ ++ a ++ s.min = s | A User Theorem |
| minmax | ⊦ s.butmin = ∅ ∧ s ≠ ∅ → s.butmax = ∅ | A User Theorem |
| minmax-01 | ⊦ s.butmin = ∅ ∧ s ≠ ∅ → s.max = s.min | A User Theorem |
| minmax-02 | ⊦ s.min = s.max ∧ s ≠ ∅ → # s = 1 | A User Theorem |
| minmax-03 | ⊦ 1 < # s → s.min < s.max | A User Theorem |
| minmax-04 | ⊦ s ≠ ∅ → ¬ s.max < s.min | A User Theorem |
| one-min | ⊦ s = ∅ ++ s.min → s -- s.min = ∅ | A User Theorem |
| size-two | ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b) | A User Theorem |