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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(#(σ from n) < ⌜n0⌝ ↔ # σ < ⌜n + n0⌝ ), ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(#(σ from n) < ⌜n0⌝ ↔ # σ < ⌜n⌝ + ⌜n0⌝ ), ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 3 from proof size-from-less (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; size-inf: ⊦ # ⌜nf⌝ = ∞; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ¬ ∞ < n∞; (s) ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; (s) c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)