Proof step 1 from proof subdel-02 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(x -1l a ⊆m y ↔ x -l a ⊆m y -l a ∧ #oc(a, x) ≤ #oc(a, y) + 1) ⊦

Rule argument

Additional information

Proof step 2 from proof subdel-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ #oc(a, x) ≤ #oc(a, y) → (x ⊆m y ↔ x -l a ⊆m y -l a)

Rule argument

Additional information

Used simplifier rules: oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; oc: ⊦ x ⊆m y → ¬ #oc(a, y) < #oc(a, x); del1: ⊦ a ∈ x → #oc(a, x -1l a) = #oc(a, x) -1; in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0; oc-zero: ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; del1: ⊦ a ∈ x → #oc(a, x -1l a) = #oc(a, x) -1; in-05: ⊦ a ∈ x → #oc(a, x) ≠ 0; ⊦ (x -1l a) -l a = x -l a; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n -1 = n - 1; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) le-one: ⊦ m ≤ n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat in-01-01: ⊦ a ∈ x -1l b → a ∈ x; (forward) from specification polylist-del n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s) ⊦ m + 1 ≤ n ↔ m < n; (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: a, x -1l a, y

Proof step 3 from proof subdel-02 (previous step) (back to tree)

Lemma sub-del