Proof step 1 from proof toinfto-append-add (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (σ to∞ n∞) + σ0 to∞ ⌜n1⌝ + n∞ ≠ (σ to∞ n∞) + ⌜σ0 to n1⌝ , ¬ # σ0 < ⌜n1⌝ , ¬ # σ < n∞ ⊦

Rule argument

Additional information

Proof step 2 from proof toinfto-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (σ to∞ n∞) + σ0 to∞ ⌜n1⌝ + n∞ ≠ (σ to∞ n∞) + ⌜σ0 to n1⌝ , ¬ # σ0 < ⌜n1⌝ , ¬ # σ < n∞ ⊦

Rule argument

Additional information

Proof step 3 from proof toinfto-append-add (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: append-toinf-ls: ⊦ ¬ # σ < n∞ → σ + σ0 to∞ n∞ = σ to∞ n∞; toinf-inf: ⊦ σ to∞ ∞ = σ; appendend-equal: ⊦ σ + σ0 = σ ↔ σ0 = [] ∨ # σ = ∞; fin-empty: ⊦ ⌜x⌝ = [] ↔ x = []; to-empty2: ⊦ ¬ # σ < ⌜n⌝ → (σ to n = [] ↔ n = 0); append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; toinf-add: ⊦ σ to∞ ⌜n⌝ + ⌜m⌝ = ⌜σ to n + m⌝ ; to-append-add: ⊦ ¬ # σ < ⌜n⌝ ∧ ¬ # σ0 < ⌜n1⌝ → ⌜σ to n⌝ + σ0 to n1 + n = (σ to n) + (σ0 to n1); append-finfin: ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; toinf-fin: ⊦ σ to∞ ⌜n⌝ = ⌜σ to n⌝ ; append-split-fin: ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; natinf freely generated by ∞, ⌜ ⌝;; a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ ⌜m⌝ + ∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s)