Proof step 1 from proof min-union (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (s ∪ s0).min ≠ (s.min < s0.min ⊃ s.min;s0.min), s ≠ ∅, s0 ≠ ∅ ⊦

Rule argument

Additional information

Proof step 2 from proof min-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # s0 ≠ 0, # s ≠ 0, (s ∪ s0).min ≠ (s.min < s0.min ⊃ s.min;s0.min), s ≠ ∅, s0 ≠ ∅ ⊦

Rule argument

Additional information

Used simplifier rules: Max-in: ⊦ s ≠ ∅ → s.max ∈ s; Min-in: ⊦ s ≠ ∅ → s.min ∈ s; max-in: ⊦ s ≠ ∅ → (s.max ∈ s ↔ true); min-inn: ⊦ s.min ∈ s ↔ s ≠ ∅; size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic

Proof step 3 from proof min-union (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  # s0 ≠ 0, #(s1 ++ a) ≠ 0, s1 ++ a ≠ ∅, ((s1 ++ a) ∪ s0).min ≠ ((s1 ++ a).min < s0.min ⊃ (s1 ++ a).min;s0.min), s0 ≠ ∅, ∀ s0. ¬(# s0 ≠ 0 ∧ # s1 ≠ 0 ∧ (s1 ∪ s0).min ≠ (s1.min < s0.min ⊃ s1.min;s0.min) ∧ s1 ≠ ∅ ∧ s0 ≠ ∅) ⊦

Rule argument

Additional information

Used simplifier rules: set('a) generated by ∅, ++;;

Proof step 4 from proof min-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  #(s1 ++ a) ≠ 0, # s0 ≠ 0, ((s1 ∪ s0) ++ a).min ≠ ((s1 ++ a).min < s0.min ⊃ (s1 ++ a).min;s0.min), s0 ≠ ∅, ∀ s. # s = 0 ∨ # s1 = 0 ∨ (s1 ∪ s).min = (s1.min < s.min ⊃ s1.min;s.min) ∨ s1 = ∅ ∨ s = ∅ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ∅ ≠ s ++ a; (s) size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union ⊦ (s ++ a) ∪ s0 = (s ∪ s0) ++ a; (s)

Proof step 5 from proof min-union (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ (s ++ a).min = (s = ∅ ∨ a < s.min ⊃ a;s.min)

• Proof step 7:

  #(s1 ++ a) ≠ 0, # s0 ≠ 0, ((s1 ∪ s0) ++ a).min ≠ ((s1 = ∅ ∨ a < s1.min ⊃ a;s1.min) < s0.min ⊃ (s1 = ∅ ∨ a < s1.min ⊃ a;s1.min);s0.min), s0 ≠ ∅, ∀ s. # s = 0 ∨ # s1 = 0 ∨ (s1 ∪ s).min = (s1.min < s.min ⊃ s1.min;s.min) ∨ s1 = ∅ ∨ s = ∅ ⊦

Rule argument

Additional information

Used terms: s1, a

Proof step 6 from proof min-union (previous step) (back to tree)

Lemma min-rec

Proof step 7 from proof min-union (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ (s ++ a).min = (s = ∅ ∨ a < s.min ⊃ a;s.min)

• Proof step 9:

  #(s1 ++ a) ≠ 0, # s0 ≠ 0, (s1 ∪ s0 = ∅ ∨ a < (s1 ∪ s0).min ⊃ a;(s1 ∪ s0).min) ≠ ((s1 = ∅ ∨ a < s1.min ⊃ a;s1.min) < s0.min ⊃ (s1 = ∅ ∨ a < s1.min ⊃ a;s1.min);s0.min), s0 ≠ ∅, ∀ s. # s = 0 ∨ # s1 = 0 ∨ (s1 ∪ s).min = (s1.min < s.min ⊃ s1.min;s.min) ∨ s1 = ∅ ∨ s = ∅ ⊦

Rule argument

Additional information

Used terms: s1 ∪ s0, a

Proof step 8 from proof min-union (previous step) (back to tree)

Lemma min-rec

Proof step 9 from proof min-union (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  #(s1 ++ a) ≠ 0, # s0 ≠ 0, (s1 ∪ s0 = ∅ ∨ a < (s1 ∪ s0).min ⊃ a;(s1 ∪ s0).min) ≠ ((s1 = ∅ ∨ a < s1.min ⊃ a;s1.min) < s0.min ⊃ (s1 = ∅ ∨ a < s1.min ⊃ a;s1.min);s0.min), s0 ≠ ∅, # s0 = 0 ∨ # s1 = 0 ∨ (s1 ∪ s0).min = (s1.min < s0.min ⊃ s1.min;s0.min) ∨ s1 = ∅ ∨ s0 = ∅ ⊦

Rule argument

Additional information

Used terms: s0

Proof step 10 from proof min-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (s1 ∪ s0).min = (s1.min < s0.min ⊃ s1.min;s0.min), # s1 ≠ 0, #(s1 ++ a) ≠ 0, # s0 ≠ 0, (a < (s1 ∪ s0).min ⊃ a;(s1 ∪ s0).min) ≠ ((a < s1.min ⊃ a;s1.min) < s0.min ⊃ (a < s1.min ⊃ a;s1.min);s0.min), s0 ≠ ∅, s1 ≠ ∅ ⊦

Rule argument

Additional information

Used simplifier rules: Max-in: ⊦ s ≠ ∅ → s.max ∈ s; Min-in: ⊦ s ≠ ∅ → s.min ∈ s; max-in: ⊦ s ≠ ∅ → (s.max ∈ s ↔ true); min-inn: ⊦ s.min ∈ s ↔ s ≠ ∅; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic size-zero-02: ⊦ # s = 0 → s = ∅; (forward) from specification set-basic unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union ⊦ s ∪ ∅ = s; (s) ⊦ #(∅ ++ a) = 1; (s) ⊦ s1 ∪ s2 = ∅ ↔ s1 = ∅ ∧ s2 = ∅; (s)

Proof step 11 from proof min-union (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 12:

  (s1 ∪ s0).min = s1.min, # s1 ≠ 0, #(s1 ++ a) ≠ 0, # s0 ≠ 0, (a < (s1 ∪ s0).min ⊃ a;(s1 ∪ s0).min) ≠ ((a < s1.min ⊃ a;s1.min) < s0.min ⊃ (a < s1.min ⊃ a;s1.min);s0.min), s0 ≠ ∅, s1 ≠ ∅, s1.min < s0.min ⊦

• Proof step 14:

  (s1 ∪ s0).min = s0.min, # s1 ≠ 0, #(s1 ++ a) ≠ 0, # s0 ≠ 0, (a < (s1 ∪ s0).min ⊃ a;(s1 ∪ s0).min) ≠ ((a < s1.min ⊃ a;s1.min) < s0.min ⊃ (a < s1.min ⊃ a;s1.min);s0.min), s0 ≠ ∅, s1 ≠ ∅, ¬ s1.min < s0.min ⊦

Rule argument

Additional information

Proof step 12 from proof min-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (s1 ∪ s0).min = s1.min, # s0 ≠ 0, #(s1 ++ a) ≠ 0, # s1 ≠ 0, (a < s1.min ⊃ a;s1.min) ≠ ((a < s1.min ⊃ a;s1.min) < s0.min ⊃ (a < s1.min ⊃ a;s1.min);s0.min), s0 ≠ ∅, s1 ≠ ∅, s1.min < s0.min ⊦

Rule argument

Additional information

Used simplifier rules: lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification weakord[tord]

Proof step 13 from proof min-union (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] Used formulas: a < s1.min

Proof step 14 from proof min-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (s1 ∪ s0).min = s0.min, # s0 ≠ 0, #(s1 ++ a) ≠ 0, # s1 ≠ 0, (a < s0.min ⊃ a;s0.min) ≠ ((a < s1.min ⊃ a;s1.min) < s0.min ⊃ a;s0.min), s0 ≠ ∅, s1 ≠ ∅, ¬ s1.min < s0.min ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a < a; (s) leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord[tord] nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification weakord[tord] nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord]

Proof step 15 from proof min-union (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  (s1 ∪ s0).min = s0.min, # s0 ≠ 0, #(s1 ++ a) ≠ 0, # s1 ≠ 0, (a < s0.min ⊃ a;s0.min) ≠ ((a < s1.min ⊃ a;s1.min) < s0.min ⊃ a;s0.min), s0 ≠ ∅, s1 ≠ ∅, ¬ a < s0.min, ¬ s1.min < s0.min ⊦

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord[tord] nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] Used formulas: a < s0.min

Proof step 16 from proof min-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  (s1 ∪ s0).min = s0.min, # s1 ≠ 0, #(s1 ++ a) ≠ 0, # s0 ≠ 0, s0.min ≠ ((a < s1.min ⊃ a;s1.min) < s0.min ⊃ a;s0.min), s0 ≠ ∅, s1 ≠ ∅, ¬ s1.min < s0.min, ¬ a < s0.min ⊦

Rule argument

Additional information

Used simplifier rules: nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification weakord[tord]

Proof step 17 from proof min-union (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss) lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification weakord[tord] transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) Used formulas: (a < s1.min ⊃ a;s1.min) < s0.min