Proof step 1 from proof not-always-decrease (conclusion) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 2:

  □ ⟨a := A⟩ (◇ A ≪ a), ∃ a. a = A ⊦

• Proof step 34:

  □ ⟨a := A⟩ (◇ A ≪ a) ⊦ ∃ a. a = A

Rule argument

Additional information

Used formulas: ∃ a. a = A

Proof step 2 from proof not-always-decrease (previous step) (back to tree)

User applied rule exists left

And obtained the following new goals

• Proof step 3:

  □ ⟨a := A⟩ (◇ A ≪ a), a0 = A ⊦

Rule argument

Additional information

Proof step 3 from proof not-always-decrease (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 4:

  ∀ a. (∀ a0. a0 ≪ a → iHP(a0)) → iHP(a) ⊦ iHP(a)

• Proof step 5:

  ∀ a1. a1 ≪ a0 → \A ∀ A, a0. ¬(a1 = a0 ∧ □ ⟨a := A⟩ (◇ A ≪ a) ∧ a0 = A) ⊦ \A ∀ A, a2. ¬(a0 = a2 ∧ □ ⟨a := A⟩ (◇ A ≪ a) ∧ a2 = A)

Rule argument

Additional information

Used terms: λ a1. \A ∀ A, a0. ¬(a1 = a0 ∧ □ ⟨a := A⟩ (◇ A ≪ a) ∧ a0 = A), a0

Proof step 4 from proof not-always-decrease (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ∀ a1. a1 ≪ a0 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A ⊦ \A ∀ A, a2. a0 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A

Rule argument

Additional information

Proof step 6 from proof not-always-decrease (previous step) (back to tree)

User applied rule pall focus right

And obtained the following new goals

• Proof step 7:

  ∀ a1. a1 ≪ a0 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A ⊦ ∀ A, a2. a0 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A

Rule argument

Additional information

Proof step 7 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), a2 = A ⊦

Rule argument

Additional information

Proof step 8 from proof not-always-decrease (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  ∃ a. ◇ (a = A ∧ a ≪ a2), ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), a2 = A ⊦

• Proof step 18:

  ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), a2 = A ⊦ ∃ a. ◇ (a = A ∧ a ≪ a2)

Rule argument

Additional information

Used formulas: ∃ a. ◇ (a = A ∧ a ≪ a2)

Proof step 9 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), ◇ (a0 = A ∧ A ≪ a2), a2 = A ⊦

Rule argument

Additional information

Proof step 10 from proof not-always-decrease (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  a0 ≪ a2 → \A ∀ A, a2. a0 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), ◇ (a0 = A ∧ A ≪ a2), a2 = A ⊦

Rule argument

Additional information

Used terms: a0

Proof step 11 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  a0 ≪ A → \A ∀ A, a2. a0 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), ◇ (a0 = A ∧ A ≪ a2), a2 = A ⊦

Rule argument

Additional information

Proof step 12 from proof not-always-decrease (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  □ ⟨a := A⟩ (◇ A ≪ a), ◇ (a0 = A ∧ A ≪ a2), a2 = A, ¬ a0 ≪ A ⊦

• Proof step 16:

  \A ∀ A, a2. a0 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), ◇ (a0 = A ∧ A ≪ a2), a2 = A ⊦

Rule argument

Additional information

Proof step 13 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  □ ⟨a := A⟩ (◇ A ≪ a), ◇ (a0 = A ∧ A ≪ a2), a2 = A, ¬ a0 ≪ A ⊦

Rule argument

Additional information

Proof step 14 from proof not-always-decrease (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 15:

  □ ⟨a := A⟩ (◇ A ≪ a), ◇ (a0 = A ∧ A ≪ a2), a2 = A, ¬ a0 ≪ a2 ⊦

Rule argument

Additional information

Proof step 15 from proof not-always-decrease (previous step) (back to tree)

User applied rule execute eventually

And closed the goal!

Rule argument

Additional information

Proof step 16 from proof not-always-decrease (previous step) (back to tree)

User applied rule execute eventually

And obtained the following new goals

• Proof step 17:

  \A ∀ A, a2. a0 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), ⟨a := A⟩ (◇ A ≪ a), a0 = A, A ≪ a2 ⊦

Rule argument

Additional information

Proof step 17 from proof not-always-decrease (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: A, a0

Proof step 18 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, □ ⟨a := A⟩ (◇ A ≪ a), a2 = A ⊦ ∃ a0. ◇ (a0 = A ∧ A ≪ a2)

Rule argument

Additional information

Proof step 19 from proof not-always-decrease (previous step) (back to tree)

User applied rule always left

And obtained the following new goals

• Proof step 20:

  ● □ ⟨a := A⟩ (◇ A ≪ a), ⟨a := A⟩ (◇ A ≪ a), ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, a2 = A ⊦ ∃ a0. ◇ (a0 = A ∧ A ≪ a2)

Rule argument

Additional information

Proof step 20 from proof not-always-decrease (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 21:

  ⟨a := A⟩ (◇ A ≪ a), ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a := A⟩ (◇ A ≪ a) ∨ a2 ≠ A, a2 = A ⊦ ∃ a0. ◇ (a0 = A ∧ A ≪ a2)

Rule argument

Additional information

Proof step 21 from proof not-always-decrease (previous step) (back to tree)

User applied rule assign left

And obtained the following new goals

• Proof step 22:

  ◇ A ≪ a, ∀ a1. a1 ≪ a2 → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a0 := A⟩ (◇ A ≪ a0) ∨ a2 ≠ A, a = A, a2 = A ⊦ ∃ a0. ◇ (a0 = A ∧ A ≪ a2)

Rule argument

Additional information

Proof step 22 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ◇ A ≪ a, ∀ a1. a1 ≪ a → \A ∀ A, a2. a1 ≠ A ∨ ¬ □ ⟨a0 := A⟩ (◇ A ≪ a0) ∨ a2 ≠ A, a = A ⊦ ∃ a0. ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Proof step 23 from proof not-always-decrease (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 24:

  ◇ A ≪ a ⊦ ∃ a0. ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Proof step 24 from proof not-always-decrease (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 25:

  N = N'' +1 until A ≪ a, n = N, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: ◇ A ≪ a

Proof step 25 from proof not-always-decrease (previous step) (back to tree)

User applied rule step

And obtained the following new goals

• Proof step 26:

  a1 ≪ a ∨ n = N +1 ∧ N = N'' +1 until A ≪ a, boolvar → a1 = a2 ∧ n = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∧ a1 ≪ a ∨ ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Proof step 26 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  a1 ≪ a ∨ n = N + 1 ∧ N = N'' + 1 until A ≪ a, boolvar → a1 = a2 ∧ n = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∧ a1 ≪ a ∨ ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

Proof step 27 from proof not-always-decrease (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 28:

  a1 ≪ a, boolvar → a1 = a2 ∧ n = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∧ a1 ≪ a ∨ ◇ (a0 = A ∧ A ≪ a)

• Proof step 30:

  N = N'' + 1 until A ≪ a, n = N + 1, boolvar → a1 = a2 ∧ n = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∧ a1 ≪ a ∨ ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Proof step 28 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  a1 ≪ a, boolvar → a1 = a2 ∧ n = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∨ ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Proof step 29 from proof not-always-decrease (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a1

Proof step 30 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  N = N'' + 1 until A ≪ a, n = N + 1, boolvar → a1 = a2 ∧ N + 1 = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∧ a1 ≪ a ∨ ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Proof step 31 from proof not-always-decrease (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 32:

  ∃ a0. ◇ (a0 = A ∧ A ≪ a), N = N'' + 1 until A ≪ a, n = N + 1, boolvar → a1 = a2 ∧ N + 1 = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∧ a1 ≪ a ∨ ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

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

Proof step 32 from proof not-always-decrease (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  ◇ (a0 = A ∧ A ≪ a), N = N'' + 1 until A ≪ a, n = N + 1, boolvar → a1 = a2 ∧ N + 1 = n0, \A ∀ N, A, a. N < n → N = N'' +1 until A ≪ a → (∃ a0. ◇ (a0 = A ∧ A ≪ a)) ⊦ ∃ a0. a0 = a1 ∧ a1 ≪ a ∨ ◇ (a0 = A ∧ A ≪ a)

Rule argument

Additional information

Proof step 33 from proof not-always-decrease (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0

Proof step 34 from proof not-always-decrease (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: A