Proof step 1 from proof Sep-forall-prove-imp (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ nP0 ⊗_(n, m) ⊆ nP1 ⊗_(n, m), ∀ n0. n0 < m → nP0(n + n0) ⊆ nP1(n + n0) ⊦

Rule argument

Additional information

Proof step 2 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ¬ nP0 ⊗_(n, m0 +1) ⊆ nP1 ⊗_(n, m0 +1), ∀ n0. n0 < m0 +1 → nP0(n + n0) ⊆ nP1(n + n0), ∀ nP0, n, nP1. ¬(¬ nP0 ⊗_(n, m0) ⊆ nP1 ⊗_(n, m0) ∧ (∀ n0. n0 < m0 → nP0(n + n0) ⊆ nP1(n + n0))) ⊦

Rule argument

Additional information

Used simplifier rules: Sep-base: ⊦ nP ⊗_(n, 0) = emp; nat freely generated by 0, +1;; ⊦ hP ⊆ hP; (s)

Proof step 3 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ¬ nP0 ⊗_(n, m0 + 1) ⊆ nP1 ⊗_(n, m0 + 1), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0) ⊦

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 + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s)

Proof step 4 from proof Sep-forall-prove-imp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ nP ⊗_(n, m + 1) = nP(n) * nP ⊗_(n + 1, m)

• Proof step 6:

  ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n, m0 + 1), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)) ⊦

Rule argument

Additional information

Used terms: m0, n, nP0

Proof step 5 from proof Sep-forall-prove-imp (previous step) (back to tree)

Lemma Sep-rec

Proof step 6 from proof Sep-forall-prove-imp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ nP ⊗_(n, m + 1) = nP(n) * nP ⊗_(n + 1, m)

• Proof step 8:

  ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0) ⊦

Rule argument

Additional information

Used terms: m0, n, nP1

Proof step 7 from proof Sep-forall-prove-imp (previous step) (back to tree)

Lemma Sep-rec

Proof step 8 from proof Sep-forall-prove-imp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ hP0 ⊆ hP1 ∧ hP2 ⊆ hP3 → hP0 * hP2 ⊆ hP1 * hP3

• Proof step 10:

  ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)) ⊦ nP0(n) ⊆ nP1(n) ∧ nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n + 1, m0)

Rule argument

Additional information

Used terms: nP1 ⊗_(n + 1, m0), nP1(n), nP0 ⊗_(n + 1, m0), nP0(n)

Proof step 9 from proof Sep-forall-prove-imp (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 11:

  nP0(n) ⊆ nP1(n), ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0) ⊦ nP0(n) ⊆ nP1(n) ∧ nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n + 1, m0)

• Proof step 15:

  ¬ nP0(n) ⊆ nP1(n), ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0) ⊦ nP0(n) ⊆ nP1(n) ∧ nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n + 1, m0)

Rule argument

Additional information

Used formulas: nP0(n) ⊆ nP1(n)

Proof step 11 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  nP0(n) ⊆ nP1(n), ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ¬ nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n + 1, m0), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)) ⊦

Rule argument

Additional information

Proof step 12 from proof Sep-forall-prove-imp (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  nP0(n) ⊆ nP1(n), ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ¬ nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n + 1, m0), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0), nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n + 1, m0) ∨ ¬(∀ n1. n1 < m0 → nP0((n + 1) + n1) ⊆ nP1((n + 1) + n1)) ⊦

Rule argument

Additional information

Used terms: nP0, n + 1, nP1

Proof step 13 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  n1 < m0, nP0(n) ⊆ nP1(n), ¬ nP0((n + 1) + n1) ⊆ nP1((n + 1) + n1), ¬ nP0 ⊗_(n + 1, m0) ⊆ nP1 ⊗_(n + 1, m0), ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 14 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n1 + 1

Proof step 15 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ¬ nP0(n) ⊆ nP1(n), ¬ nP0(n) * nP0 ⊗_(n + 1, m0) ⊆ nP1(n) * nP1 ⊗_(n + 1, m0), ∀ n0. ¬ m0 < n0 → nP0(n + n0) ⊆ nP1(n + n0), ∀ nP, n0, nP2. nP ⊗_(n0, m0) ⊆ nP2 ⊗_(n0, m0) ∨ ¬(∀ n1. n1 < m0 → nP(n0 + n1) ⊆ nP2(n0 + n1)) ⊦

Rule argument

Additional information

Proof step 16 from proof Sep-forall-prove-imp (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: 0