Proof step 1 from proof del-size-le (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # s < #(s -- a) ⊦

Rule argument

Additional information

Proof step 2 from proof del-size-le (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: del-size: ⊦ a ∈ s → #(s -- a) = # s - 1; del-in: ⊦ ¬ a ∈ s → s -- a = s; ⊦ ¬ n < n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) size-zero-02: ⊦ # s = 0 → s = ∅; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: a ∈ s