Proof step 1 from proof del1-01-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a ' + (x -1l a) ≠ x, ordered≤(a ' + (x -1l a)), ordered≤(x), a ∈ x ⊦

Rule argument

Additional information

Proof step 2 from proof del1-01-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  a ' + (x -1l a) ≠ x, ordered≤(a ' + (x -1l a)), ordered≤(x), a ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: cons-02: ⊦ ordered≤(a ' + x) → ordered≤(x); del1-01: ⊦ ordered≤(x) → ordered≤(x -1l a); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 3 from proof del1-01-01 (previous step) (back to tree)

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: cons-02: ⊦ ordered≤(a ' + x) → ordered≤(x); app-01: ⊦ ordered≤(x + y) → ordered≤(y); del1-01: ⊦ ordered≤(x) → ordered≤(x -1l a); le-r: ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x); orderedle-ls: ⊦ b < a ∧ b ∈ x → ¬ ordered≤(a ' + x); list freely generated by [], +;; ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x) -1l a = x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a); (s) ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] -1l a = []; (s) ⊦ x + [] = x; (s) ⊦ a ' ≠ []; (s) ⊦ ¬ a ∈ []; (s)