Proof step 1 from proof possize-notin (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(pos(a, x) = # x ↔ ¬ a ∈ x) ⊦

Rule argument

Additional information

Proof step 2 from proof possize-notin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  pos(a, x) = # x, a ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: notin-03: ⊦ ¬ a ∈ x → pos(a, x) = # x;

Proof step 3 from proof possize-notin (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  pos(a, a0 + x0) = #(a0 + x0), a ∈ a0 + x0, ∀ a. ¬(pos(a, x0) = # x0 ∧ a ∈ x0) ⊦

Rule argument

Additional information

Used simplifier rules: pos-e: ⊦ pos(a, []) = 0; list freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ ¬ a ∈ []; (s)

Proof step 4 from proof possize-notin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  pos(a, x0) = # x0, a ≠ a0, a ∈ x0, ∀ a1. pos(a1, x0) ≠ pos(a, x0) ∨ ¬ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: pos-y: ⊦ pos(a, a ' + x) = 0; pos-n: ⊦ a ≠ b → pos(a, b ' + x) = pos(a, x) + 1; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m + 1 ≠ 0; (s) ⊦ a ∈ b ' ↔ a = b; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a + x = a ' + x; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 5 from proof possize-notin (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a