Proof step 1 from proof infappend-frags (conclusion) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 2:

  ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# lf(n)) = lf(n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

• Proof step 3:

  ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∃ α, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Used terms: alf

Proof step 2 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 3 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Proof step 4 from proof infappend-frags (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  ∀ n. lf(n).last = lf(n + 1).head ∧ lf(n) ≠ [] ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# lf(n)) = lf(n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n) + 1⌝ ∧ (∀ m. n ≤ m → lf(m).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

• Proof step 6:

  ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n) ⊦ ∀ n. slf(n).last = slf(n + 1).head ∧ slf(n) ≠ [], ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

• Proof step 8:

  ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n) + 1⌝ ∧ (∀ m. n ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Used terms: slf

Proof step 5 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n)), slf(n0).last = slf(n0 + 1).head ∧ slf(n0) ≠ []

Rule argument

Additional information

Proof step 7 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: not-frag-empty: ⊦ ¬ frag(IOAut(start, step, ext))([], α); ⊦ ⌜[]⌝ = []; (s) Used terms: n0

Proof step 8 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ii(0) = 0, ii0(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 9 from proof infappend-frags (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  ii(0) = 0, ii0(0) = 0, ii0 = ii, (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n) ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

• Proof step 134:

  ii(0) = 0, ii0(0) = 0, ii0 ≠ ii, (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n) ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Used formulas: ii0 = ii

Proof step 10 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Proof step 11 from proof infappend-frags (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  ii(0) = 0, (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦ frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Used terms: σ, α, ii

Proof step 12 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ frag(IOAut(start, step, ext))(σ, α) ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ⌜ii(n2 + 1)⌝ < # σ ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2) ∧ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2)

Rule argument

Additional information

Proof step 13 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  ii(0) = 0, ¬ frag(IOAut(start, step, ext))(σ, α), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

• Proof step 105:

  ii(0) = 0, (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

• Proof step 112:

  ii(0) = 0, (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2) ∧ ⌜ii(n2 + 1)⌝ < # σ ∧ ii(n2 + 1) = ii(n2) + # alf(n2)

Rule argument

Additional information

Proof step 14 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 16:

  ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, # σ ≠ # α + ⌜1⌝ ∨ (∃ n. ¬(⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))) ⊦

Rule argument

Additional information

Used terms: ext, α, step, start, σ

Proof step 15 from proof infappend-frags (previous step) (back to tree)

Lemma frag

Proof step 16 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ii(0) = 0, (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), # σ ≠ # α + ⌜1⌝ ∨ ¬(⌜n1⌝ < # α → step(σ[n1], α[n1], σ[n1 + 1])) ⊦

Rule argument

Additional information

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

Proof step 17 from proof infappend-frags (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 18:

  ii(0) = 0, # σ ≠ # α + ⌜1⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, # σ ≠ # α + ⌜1⌝ ∨ ¬(⌜n1⌝ < # α → step(σ[n1], α[n1], σ[n1 + 1])) ⊦

• Proof step 36:

  # σ = # α + ⌜1⌝ , ii(0) = 0, (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, # σ ≠ # α + ⌜1⌝ ∨ ¬(⌜n1⌝ < # α → step(σ[n1], α[n1], σ[n1 + 1])) ⊦

Rule argument

Additional information

Used formulas: # σ ≠ # α + ⌜1⌝

Proof step 18 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ii(0) = 0, # σ ≠ # α + ⌜1⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Proof step 19 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  # α = ⌜ii(n)⌝ , ii(0) = 0, # σ ≠ # α + ⌜1⌝ , finp(α), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n) ⊦

• Proof step 30:

  ii(0) = 0, # σ ≠ # α + ⌜1⌝ , ¬ finp(α), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦

Rule argument

Additional information

Proof step 20 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # al = ii(n), ii(0) = 0, # σ ≠ ⌜ii(n)⌝ + ⌜1⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 21 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 22:

  # al = ii(n), # σ = ⌜ii(n0)⌝ + ⌜1⌝ , ii(0) = 0, # σ ≠ ⌜ii(n)⌝ + ⌜1⌝ , finp(σ), ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0) ⊦

• Proof step 26:

  # al = ii(n), ii(0) = 0, # σ ≠ ⌜ii(n)⌝ + ⌜1⌝ , ¬ finp(σ), ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦

Rule argument

Additional information

Proof step 22 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # al = ii(n), ii(n0) + 1 = # sl, ii(0) = 0, ii(n) + 1 ≠ # sl, ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0), ∀ n1. ii(n1 + 1) = ii(n1) + # slf(n1) - 1 ∧ ¬ ii(n0) < ii(n1 + 1) ∧ sl.drop(ii(n1)).take(# slf(n1)) = slf(n1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ n∞ = ⌜m⌝ + ⌜n0⌝ → (⌜n⌝ < n∞ ↔ n < m + n0); (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 23 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  # al = ii(n), ii(n0) + 1 = # sl, ii(0) = 0, ii(n) + 1 ≠ # sl, n ≤ n0 → alf(n0) = [] ∧ ii(n0) = ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # slf(n1) - 1 ∧ ¬ ii(n0) < ii(n1 + 1) ∧ sl.drop(ii(n1)).take(# slf(n1)) = slf(n1), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 24 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 25:

  # al = ii(n), ii(n0) + 1 = # sl, ii(0) = 0, ii(n) + 1 ≠ # sl, n ≤ n0 → alf(n0) = [] ∧ ii(n0) = ii(n), n0 ≤ n → slf(n).tail = [] ∧ ii(n) = ii(n0), ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0), ∀ n1. ii(n1 + 1) = ii(n1) + # slf(n1) - 1 ∧ ¬ ii(n0) < ii(n1 + 1) ∧ sl.drop(ii(n1)).take(# slf(n1)) = slf(n1) ⊦

Rule argument

Additional information

Used terms: n

Proof step 25 from proof infappend-frags (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n → m ≤ n; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) Used formulas: n ≤ n0

Proof step 26 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # al = ii(n), ii(0) = 0, ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n0. ii(n0 + 1) = ii(n0) + # slf(n0) - 1 ∧ sf.drop(ii(n0)).take(# slf(n0)) = slf(n0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss)

Proof step 27 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 28:

  # al = ii(n), ii(0) = 0, ∀ n0. ii(n0 + 1) = ii(n0) + # slf(n0) - 1 ∧ sf.drop(ii(n0)).take(# slf(n0)) = slf(n0), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1), ∃ m. ii(m) ≤ ii(n) ∧ ii(n) < ii(m + 1) ⊦

Rule argument

Additional information

Used terms: ii(n)

Proof step 28 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # al = ii(n), ii(0) = 0, ii(m) < ii(m + 1), ii(n) < ii(m + 1), ii(m) ≤ ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # slf(n0) - 1 ∧ sf.drop(ii(n0)).take(# slf(n0)) = slf(n0), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # alf(n1) ∧ ¬ ii(n) < ii(n1 + 1) ∧ al.drop(ii(n1)).take(# alf(n1)) = alf(n1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 29 from proof infappend-frags (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m

Proof step 30 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  ii(0) = 0, # σ ≠ ∞, finp(σ) → # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜m⌝ + ∞ = ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss)

Proof step 31 from proof infappend-frags (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 32:

  ii(0) = 0, σ = ⌜sl⌝ , # σ ≠ ∞, finp(σ) → # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0)), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 32 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  ii(n0) + 1 = # sl, ii(0) = 0, ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ii(n + 1) < # sl ∧ sl.drop(ii(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0) ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ finp(⌜x⌝ ); (s) ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 33 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 34:

  ii(n0) + 1 = # sl, ii(0) = 0, ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ii(n + 1) < # sl ∧ sl.drop(ii(n)).take(# slf(n)) = slf(n), ∃ m. ii(m) ≤ ii(n0) ∧ ii(n0) < ii(m + 1) ⊦

Rule argument

Additional information

Used terms: ii(n0)

Proof step 34 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  ii(n0) + 1 = # sl, ii(0) = 0, ii(m) < ii(m + 1), ii(n0) < ii(m + 1), # sl ≤ ii(m + 1), ii(m) ≤ ii(n0), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ii(n + 1) < # sl ∧ sl.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat

Proof step 35 from proof infappend-frags (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: m

Proof step 36 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # σ = # α + ⌜1⌝ , ii(0) = 0, ⌜n1⌝ < # α, ¬ step(σ[n1], α[n1], σ[n1 + 1]), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Proof step 37 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 38:

  # σ = # α + ⌜1⌝ , # α = ⌜ii(n)⌝ , ii(0) = 0, ⌜n1⌝ < # α, finp(α), ¬ step(σ[n1], α[n1], σ[n1 + 1]), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n) ⊦

• Proof step 77:

  # σ = # α + ⌜1⌝ , ii(0) = 0, ⌜n1⌝ < # α, ¬ finp(α), ¬ step(σ[n1], α[n1], σ[n1 + 1]), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦

Rule argument

Additional information

Proof step 38 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  # al = ii(n), # σ = ⌜ii(n)⌝ + ⌜1⌝ , ii(0) = 0, n1 < ii(n), ¬ step(σ[n1], al[n1], σ[n1 + 1]), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ n∞ = ⌜m⌝ + ⌜n0⌝ → (⌜n⌝ < n∞ ↔ n < m + n0); (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 39 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  # σ = ⌜ii(n)⌝ + ⌜1⌝ , # al = ii(n), # σ = ⌜ii(n0)⌝ + ⌜1⌝ , ii(0) = 0, n1 < ii(n), finp(σ), ¬ step(σ[n1], al[n1], σ[n1 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ ⌜n⌝ ≠ ∞; (s) 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

Proof step 40 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  # al = ii(n), ii(n) + 1 = # sl, ii(0) = 0, ii(n0) = ii(n), n1 < ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ sl.drop(ii(n2)).take(# slf(n2)) = slf(n2) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 41 from proof infappend-frags (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 42:

  ii(0) = 0, ∀ n. ii(n) ≤ ii(n + 1), m < ii(n0) ⊦ ∃ n1. n1 < n0 ∧ ii(n1) ≤ m ∧ m < ii(n1 + 1)

• Proof step 43:

  # al = ii(n), ii(n) + 1 = # sl, ii(n0) = ii(n), ii(0) = 0, n1 < ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦ ∀ n. ii(n) ≤ ii(n + 1)

• Proof step 45:

  # al = ii(n), ii(n) + 1 = # sl, ii(n0) = ii(n), ii(0) = 0, n1 < ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∃ n2. n2 < n ∧ ii(n2) ≤ n1 ∧ n1 < ii(n2 + 1) ⊦

Rule argument

Additional information

Used terms: ii, n1, n

Proof step 42 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  # al = ii(n), ii(n) + 1 = # sl, ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) < ii(n2), n1 < ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 44 from proof infappend-frags (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m + n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: n2, n2 + 1

Proof step 45 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  # al = ii(n), ii(n) + 1 = # sl, ii(0) = 0, ii(n0) = ii(n), n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ sl.drop(ii(n2)).take(# slf(n2)) = slf(n2) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat

Proof step 46 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 47:

  # al = ii(n), ii(n) + 1 = # sl, ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), al.drop(ii(n2)).take(# alf(n2)) = alf(n2), ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n1 < ii(n), n1 < ii(n2 + 1), n2 < n, ii(n2) ≤ n1, ¬ ii(n) < ii(n2 + 1), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used terms: n2

Proof step 47 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  # al = ii(n), ii(n) + 1 = # sl, ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), al.drop(ii(n2)).take(# alf(n2)) = alf(n2), alf(n2) ≠ [], ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n1 < ii(n), n1 < ii(n2 + 1), n2 < n, ii(n2 + 1) ≤ ii(n), ii(n2) ≤ n1, ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n2. ii(n2 + 1) = ii(n2) + # slf(n2) - 1 ∧ ¬ ii(n) < ii(n2 + 1) ∧ sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 48 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 49:

  # al = ii(n), ii(n) + 1 = # sl, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, al.drop(ii(n2)).take(# alf(n2)) = alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ii(n2 + 1) ≤ ii(n), ¬ ii(n) < ii(n2 + 1), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n) ⊦

Rule argument

Additional information

Used terms: n2

Proof step 49 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  # al = ii(n), ii(n) + 1 = # sl, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, al.drop(ii(n2)).take(# alf(n2)) = alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ii(n2 + 1) ≤ ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 50 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 51:

  # al = ii(n), ii(n) + 1 = # sl, slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # slf(n2) - 1, ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), al.drop(ii(n2)).take(# alf(n2)) = alf(n2), alf(n2) ≠ [], ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n1 < ii(n), n1 < ii(n2 + 1), n2 < n, frag*(IOAut(start, step, ext))(slf(n2), alf(n2)), ii(n2 + 1) ≤ ii(n), ii(n2) ≤ n1, ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used terms: n2

Proof step 51 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 53:

  # ⌜slf(n2)⌝ = # ⌜alf(n2)⌝ + ⌜1⌝ , # al = ii(n), ii(n) + 1 = # sl, slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, al.drop(ii(n2)).take(# alf(n2)) = alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ii(n2 + 1) ≤ ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n. ⌜n⌝ < # ⌜alf(n2)⌝ → step(⌜slf(n2)⌝ [n], ⌜alf(n2)⌝ [n], ⌜slf(n2)⌝ [n +1]) ⊦

Rule argument

Additional information

Used terms: ext, ⌜alf(n2)⌝ , step, start, ⌜slf(n2)⌝

Proof step 52 from proof infappend-frags (previous step) (back to tree)

Lemma frag

Proof step 53 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  # al = ii(n), ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # slf(n2) - 1, ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), al.drop(ii(n2)).take(# alf(n2)) = alf(n2), alf(n2) ≠ [], ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n1 < ii(n), n1 < ii(n2 + 1), n2 < n, ii(n2 + 1) ≤ ii(n), ii(n2) ≤ n1, ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s)

Proof step 54 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

• Proof step 56:

  # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ii(n2 + 1) ≤ ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n. n < # al.drop(ii(n2)).take(# alf(n2)) → al.drop(ii(n2)).take(# alf(n2))[n] = alf(n2)[n] ⊦

Rule argument

Additional information

Used terms: al.drop(ii(n2)).take(# alf(n2)), alf(n2)

Proof step 55 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  # al = ii(n), # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # slf(n2) - 1, ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n1 < ii(n), n1 < ii(n2 + 1), n2 < n, ii(n2 + 1) ≤ ii(n), ii(n2) ≤ n1, ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n. n < # alf(n2) → al.drop(ii(n2)).take(# alf(n2))[n] = alf(n2)[n], ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Proof step 57 from proof infappend-frags (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 58:

  # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = n4 + 1, slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), ii(n2 + 1) = n4, sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ii(n2 + 1) ≤ ii(n), 1 ≤ ii(n2) + # slf(n2), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n. n < # alf(n2) → al.drop(ii(n2)).take(# alf(n2))[n] = alf(n2)[n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ x.drop(0) = x; (s) ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: ii(n2) + # slf(n2), 1, n4

Proof step 58 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ii(n2 + 1) ≤ ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n. n < # alf(n2) → al.drop(ii(n2)).take(# alf(n2))[n] = alf(n2)[n] ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s) ⊦ m + 1 ≠ 0; (s) not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat

Proof step 59 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 60:

  # al = ii(n), # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), ii(n2) + # slf(n2) = ii(n2 + 1) + 1, ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n1 < ii(n), n1 < ii(n2 + 1), n2 < n, ii(n2 + 1) ≤ ii(n), ii(n2) ≤ n1, ¬ step(sl[n1], al[n1], sl[n1 + 1]), n1 - ii(n2) < # alf(n2) → al.drop(ii(n2)).take(# alf(n2))[n1 - ii(n2)] = alf(n2)[n1 - ii(n2)], ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Used terms: n1 - ii(n2)

Proof step 60 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  # al = ii(n), # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), ii(n2) + # slf(n2) = ii(n2 + 1) + 1, ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, al.drop(ii(n2)).take(# alf(n2))[n1 - ii(n2)] = alf(n2)[n1 - ii(n2)], ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n1 < ii(n), n1 < ii(n2 + 1), n2 < n, ii(n2 + 1) ≤ ii(n), ii(n2) ≤ n1, ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 61 from proof infappend-frags (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 62:

  # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, al.drop(ii(n2)).take(# alf(n2))[n4] = alf(n2)[n4], ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), n1 = n4 + ii(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n2 < n, n1 < ii(n2 + 1), n1 < ii(n), ii(n2) < ii(n2 + 1), ii(n2) < ii(n), ii(n2) ≤ n1, ii(n2 + 1) ≤ ii(n), ¬ step(sl[n1], al[n1], sl[n1 + 1]), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n1, ii(n2), n4

Proof step 62 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  # al = ii(n), # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), ii(n2) + # slf(n2) = ii(n2 + 1) + 1, ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, al.drop(ii(n2)).take(# alf(n2))[n4] = alf(n2)[n4], ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n4 < # alf(n2), ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n2 < n, n4 + ii(n2) < ii(n), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], al[n4 + ii(n2)], sl[(n4 + ii(n2)) + 1]), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m ≤ m + n; (s)

Proof step 63 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

  ¬ # x < n, m < n ⊦ x.take(n)[m] = x[m]

• Proof step 65:

  # al.drop(ii(n2)).take(# alf(n2)) = # alf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, al.drop(ii(n2))[n4] = alf(n2)[n4], ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n4 + ii(n2) < ii(n), n2 < n, ii(n2) < ii(n2 + 1), ii(n2) < ii(n), n4 < # alf(n2), ii(n2 + 1) ≤ ii(n), ¬ # al.drop(ii(n2)) < # alf(n2), ¬ step(sl[n4 + ii(n2)], al[n4 + ii(n2)], sl[(n4 + ii(n2)) + 1]), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → ¬ n < m; (s) ¬ # x < n ⊦ # x.drop(n) = # x - n; (s) ⊦ m < n → m ≤ n; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ ¬ n < n; (s) Used terms: al.drop(ii(n2)), # alf(n2), n4

Proof step 64 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 65 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  # al = ii(n), ii(n2) + # slf(n2) = ii(n2 + 1) + 1, ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, al[ii(n2) + n4] = alf(n2)[n4], ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n4 < # alf(n2), ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n2 < n, n4 + ii(n2) < ii(n), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: ¬ # x < n ⊦ # x.take(n) = n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n → m ≤ n; (s) ¬ # x < n ⊦ # x.drop(n) = # x - n; (s) ⊦ m < n → ¬ n < m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) m + m0 < # x ⊦ x.drop(m)[m0] = x[m + m0]; (s) ⊦ m < n → (n ≤ m ↔ false); (s) c: ⊦ m + n = n + m; from specification nat-basic

Proof step 66 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 67:

  # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, al[ii(n2) + n4] = alf(n2)[n4], ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n4 + ii(n2) < ii(n), n2 < n, ii(n2) < ii(n2 + 1), ii(n2) < ii(n), n4 < # alf(n2), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), n4 < # alf(n2) → step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n) ⊦

Rule argument

Additional information

Used terms: n4

Proof step 67 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  # al = ii(n), ii(n2) + # slf(n2) = ii(n2 + 1) + 1, ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, al[ii(n2) + n4] = alf(n2)[n4], ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), sl.drop(ii(n2)).take(# slf(n2)) = slf(n2), alf(n2) ≠ [], n4 < # alf(n2), ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n2 < n, n4 + ii(n2) < ii(n), step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 68 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

• Proof step 70:

  # sl.drop(ii(n2)).take(# slf(n2)) = # slf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, al[ii(n2) + n4] = alf(n2)[n4], ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), alf(n2) ≠ [], n4 + ii(n2) < ii(n), n2 < n, ii(n2) < ii(n2 + 1), ii(n2) < ii(n), n4 < # alf(n2), step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n. n < # sl.drop(ii(n2)).take(# slf(n2)) → sl.drop(ii(n2)).take(# slf(n2))[n] = slf(n2)[n] ⊦

Rule argument

Additional information

Used terms: sl.drop(ii(n2)).take(# slf(n2)), slf(n2)

Proof step 69 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  # al = ii(n), # sl.drop(ii(n2)).take(# slf(n2)) = # slf(n2), ii(n2) + # slf(n2) = ii(n2 + 1) + 1, ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, al[ii(n2) + n4] = alf(n2)[n4], ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), alf(n2) ≠ [], n4 < # alf(n2), ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n2 < n, n4 + ii(n2) < ii(n), step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), ∀ n. n < # slf(n2) → sl.drop(ii(n2)).take(# slf(n2))[n] = slf(n2)[n], ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 71 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 72:

  # sl.drop(ii(n2)).take(# slf(n2)) = # slf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, al[ii(n2) + n4] = alf(n2)[n4], ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), alf(n2) ≠ [], n4 + ii(n2) < ii(n), n2 < n, ii(n2) < ii(n2 + 1), ii(n2) < ii(n), n4 < # alf(n2), step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), n4 < # slf(n2) → sl.drop(ii(n2)).take(# slf(n2))[n4] = slf(n2)[n4], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n. n < # slf(n2) → sl.drop(ii(n2)).take(# slf(n2))[n] = slf(n2)[n] ⊦

Rule argument

Additional information

Used terms: n4

Proof step 72 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 73:

  # al = ii(n), # sl.drop(ii(n2)).take(# slf(n2)) = # slf(n2), ii(n2) + # slf(n2) = ii(n2 + 1) + 1, ii(n) + 1 = # sl, # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, al[ii(n2) + n4] = alf(n2)[n4], sl.drop(ii(n2)).take(# slf(n2))[n4] = slf(n2)[n4], ii(n0) = ii(n), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), alf(n2) ≠ [], n4 < # alf(n2), ii(n2) < ii(n), ii(n2) < ii(n2 + 1), n2 < n, n4 + ii(n2) < ii(n), step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ii(n2 + 1) ≤ ii(n), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), ∀ n. n < # slf(n2) → sl.drop(ii(n2)).take(# slf(n2))[n] = slf(n2)[n], ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 73 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ¬ # x < n, m < n ⊦ x.take(n)[m] = x[m]

• Proof step 75:

  # sl.drop(ii(n2)).take(# slf(n2)) = # slf(n2), # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, sl.drop(ii(n2))[n4] = slf(n2)[n4], al[ii(n2) + n4] = alf(n2)[n4], ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), alf(n2) ≠ [], n4 + ii(n2) < ii(n), n2 < n, ii(n2) < ii(n2 + 1), ii(n2) < ii(n), n4 < # alf(n2), n4 < # slf(n2), step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ii(n2 + 1) ≤ ii(n), ¬ # sl.drop(ii(n2)) < # slf(n2), ¬ step(sl[n4 + ii(n2)], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n), ∀ n. n < # slf(n2) → sl.drop(ii(n2)).take(# slf(n2))[n] = slf(n2)[n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + m0 < n → ¬ n + n0 < m; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m = n + 1 → ¬ m ≤ n; (s) ¬ # x < n ⊦ # x.take(n) = n; (s) ¬ # x < n ⊦ # x.drop(n) = # x - n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ¬ # x < n, m < n ⊦ x.take(n)[m] = x[m]; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < m0 ∧ n0 < n + m → n0 + 1 ≠ n + m0; (s) m + m0 < # x ⊦ x.drop(m)[m0] = x[m + m0]; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m +1 = m + 1; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n → ¬ n < m; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: sl.drop(ii(n2)), # slf(n2), n4

Proof step 74 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 75 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  # al = ii(n), # alf(n2) + 1 = # slf(n2), ii(n) + 1 = # sl, ii(n2) + # slf(n2) = ii(n2 + 1) + 1, slf(n2 + 1).head = slf(n2).last, sl[ii(n2) + n4] = slf(n2)[n4], al[ii(n2) + n4] = alf(n2)[n4], ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii(n0) = ii(n), alf(n2) ≠ [], sl ≠ [], slf(n2) ≠ [], n4 + ii(n2) < ii(n), n2 < n, ii(n2) < ii(n2 + 1), ii(n2) < ii(n), n4 < # alf(n2), n4 < # slf(n2), ii(n2) < # sl, ii(n2 + 1) < # sl, step(slf(n2)[n4], alf(n2)[n4], slf(n2)[n4 + 1]), ii(n2 + 1) ≤ ii(n), ¬ step(slf(n2)[n4], alf(n2)[n4], sl[(n4 + ii(n2)) + 1]), ∀ n1. n1 < # slf(n2) → sl[ii(n2) + n1] = slf(n2)[n1], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n → ¬ n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ # x = 0 ↔ x = []; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat m + m0 < # x ⊦ x.drop(m)[m0] = x[m + m0]; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ¬ # x < n, m < n ⊦ x.take(n)[m] = x[m]; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ¬ m + n < m; (s) ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m ≤ n ↔ ¬ n < m; (ss) ¬ # x < n ⊦ # x.drop(n) = # x - n; (s) ¬ # x < n ⊦ # x.take(n) = n; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s)

Proof step 76 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n4 + 1

Proof step 77 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  ii(0) = 0, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ ⌜m⌝ + ∞ = ∞; (s)

Proof step 78 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 79:

  ii(0) = 0, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1) ⊦

Rule argument

Additional information

Used terms: n1

Proof step 79 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  ii(0) = 0, ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 80 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 81:

  ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), af.drop(ii(m)).take(# alf(m)) = alf(m), n1 < ii(m + 1), ii(m) < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used terms: m

Proof step 81 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), af.drop(ii(m)).take(# alf(m)) = alf(m), alf(m) ≠ [], ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic

Proof step 82 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 83:

  slf(m + 1).head = slf(m).last, ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, af.drop(ii(m)).take(# alf(m)) = alf(m), alf(m) ≠ [], n1 < ii(m + 1), ii(m) < ii(m + 1), frag*(IOAut(start, step, ext))(slf(m), alf(m)), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used terms: m

Proof step 83 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 85:

  # ⌜slf(m)⌝ = # ⌜alf(m)⌝ + ⌜1⌝ , slf(m + 1).head = slf(m).last, ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), af.drop(ii(m)).take(# alf(m)) = alf(m), alf(m) ≠ [], ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ⌜n⌝ < # ⌜alf(m)⌝ → step(⌜slf(m)⌝ [n], ⌜alf(m)⌝ [n], ⌜slf(m)⌝ [n +1]) ⊦

Rule argument

Additional information

Used terms: ext, ⌜alf(m)⌝ , step, start, ⌜slf(m)⌝

Proof step 84 from proof infappend-frags (previous step) (back to tree)

Lemma frag

Proof step 85 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, af.drop(ii(m)).take(# alf(m)) = alf(m), alf(m) ≠ [], n1 < ii(m + 1), ii(m) < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s)

Proof step 86 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

• Proof step 88:

  # af.drop(ii(m)).take(# alf(m)) = # alf(m), # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. n < # af.drop(ii(m)).take(# alf(m)) → af.drop(ii(m)).take(# alf(m))[n] = alf(m)[n] ⊦

Rule argument

Additional information

Used terms: af.drop(ii(m)).take(# alf(m)), alf(m)

Proof step 87 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 88 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, alf(m) ≠ [], n1 < ii(m + 1), ii(m) < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ nf.drop(n)(m) = nf(m + n); (s) m < n ⊦ nf.take(n)[m] = nf(m); (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ # nf.take(n) = n; (s)

Proof step 89 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 90:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), n1 - ii(m) < # alf(m) → af((n1 - ii(m)) + ii(m)) = alf(m)[n1 - ii(m)], ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used terms: n1 - ii(m)

Proof step 90 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af((n1 - ii(m)) + ii(m)) = alf(m)[n1 - ii(m)], ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 91 from proof infappend-frags (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 92:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, n1 = n0 + ii(m), alf(m) ≠ [], n1 < ii(m + 1), ii(m) < ii(m + 1), ii(m) ≤ n1, ¬ step(sf(n1), af(n1), sf(n1 + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n] ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n1, ii(m), n0

Proof step 92 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], n0 < # alf(m), ii(m) < ii(m + 1), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 93 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 94:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, ii(m + 1) = ii(m) + # slf(m) - 1, sf.drop(ii(m)).take(# slf(m)) = slf(m), alf(m) ≠ [], ii(m) < ii(m + 1), n0 < # alf(m), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n] ⊦

Rule argument

Additional information

Used terms: m

Proof step 94 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 95:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

• Proof step 96:

  # sf.drop(ii(m)).take(# slf(m)) = # slf(m), # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = ii(m) + # slf(m) - 1, ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], n0 < # alf(m), ii(m) < ii(m + 1), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. n < # sf.drop(ii(m)).take(# slf(m)) → sf.drop(ii(m)).take(# slf(m))[n] = slf(m)[n] ⊦

Rule argument

Additional information

Used terms: sf.drop(ii(m)).take(# slf(m)), slf(m)

Proof step 95 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 96 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 97:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = ii(m) + # slf(m) - 1, ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], n0 < # alf(m), ii(m) < ii(m + 1), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n], ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ nf.drop(n)(m) = nf(m + n); (s) m < n ⊦ nf.take(n)[m] = nf(m); (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ # nf.take(n) = n; (s)

Proof step 97 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 98:

  # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, ii(m + 1) = ii(m) + # slf(m) - 1, alf(m) ≠ [], ii(m) < ii(m + 1), n0 < # alf(m), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), n0 < # slf(m) → sf(n0 + ii(m)) = slf(m)[n0], ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n] ⊦

Rule argument

Additional information

Used terms: n0

Proof step 98 from proof infappend-frags (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 99:

  # alf(m) + 1 = # slf(m), ii(m) + # slf(m) = n1 + 1, slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = n1, ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], n0 < # alf(m), ii(m) < ii(m + 1), 1 ≤ ii(m) + # slf(m), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), n0 < # slf(m) → sf(n0 + ii(m)) = slf(m)[n0], ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n], ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: ii(m) + # slf(m), 1, n1

Proof step 99 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

  # alf(m) + 1 = # slf(m), ii(m) + # slf(m) = ii(m + 1) + 1, slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), alf(m) ≠ [], n0 < # alf(m), ii(m) < ii(m + 1), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), n0 < # slf(m) → sf(n0 + ii(m)) = slf(m)[n0], ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n], ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s) ⊦ m + 1 ≠ 0; (s) not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat

Proof step 100 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 101:

  ii(m) + # slf(m) = ii(m + 1) + 1, # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, sf(n0 + ii(m)) = slf(m)[n0], alf(m) ≠ [], ii(m) < ii(m + 1), n0 < # alf(m), ¬ step(sf(n0 + ii(m)), alf(m)[n0], sf((n0 + ii(m)) + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 101 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

  # alf(m) + 1 = # slf(m), ii(m) + # slf(m) = ii(m + 1) + 1, slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), sf(n0 + ii(m)) = slf(m)[n0], alf(m) ≠ [], n0 < # alf(m), ii(m) < ii(m + 1), ¬ step(slf(m)[n0], alf(m)[n0], sf((n0 + ii(m)) + 1)), ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n], ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # alf(m) → step(slf(m)[n], alf(m)[n], slf(m)[n + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Proof step 102 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 103:

  ii(m) + # slf(m) = ii(m + 1) + 1, # alf(m) + 1 = # slf(m), slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(m + 1) = ii(m) + # alf(m), ii(0) = 0, sf(n0 + ii(m)) = slf(m)[n0], alf(m) ≠ [], ii(m) < ii(m + 1), n0 < # alf(m), ¬ step(slf(m)[n0], alf(m)[n0], sf((n0 + ii(m)) + 1)), n0 < # alf(m) → step(slf(m)[n0], alf(m)[n0], slf(m)[n0 + 1]), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n] ⊦

Rule argument

Additional information

Used terms: n0

Proof step 103 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 104:

  # alf(m) + 1 = # slf(m), ii(m) + # slf(m) = ii(m + 1) + 1, slf(m + 1).head = slf(m).last, af(n0 + ii(m)) = alf(m)[n0], ii(0) = 0, ii(m + 1) = ii(m) + # alf(m), sf(n0 + ii(m)) = slf(m)[n0], alf(m) ≠ [], n0 < # alf(m), ii(m) < ii(m + 1), step(slf(m)[n0], alf(m)[n0], slf(m)[n0 + 1]), ¬ step(slf(m)[n0], alf(m)[n0], sf((n0 + ii(m)) + 1)), ∀ n. n < # slf(m) → sf(n + ii(m)) = slf(m)[n], ∀ n. n < # alf(m) → af(n + ii(m)) = alf(m)[n], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ sf.drop(ii(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Proof step 104 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n0 + 1

Proof step 105 from proof infappend-frags (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 106:

  # α = ⌜ii(n)⌝ , ii(0) = 0, finp(α), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n) ⊦ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

• Proof step 108:

  ii(0) = 0, ¬ finp(α), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Proof step 106 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 107:

  # al = ii(n), ii(0) = 0, (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n), ∀ n2. ii(n2 + 1) = ii(n2) + # alf(n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ al.drop(ii(n2)).take(# alf(n2)) = alf(n2) ⊦ ∃ n1. ii(n) = ii(n1) ∧ (∀ m. n1 ≤ m → alf(m) = [] ∧ ii(m) = ii(n1))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ finp(⌜x⌝ ); (s) ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 107 from proof infappend-frags (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 108 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 109:

  ii(0) = 0, finp(σ) → # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ finp(⌜nf⌝ ); (s) ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss)

Proof step 109 from proof infappend-frags (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 110:

  ii(0) = 0, finp(σ) → # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0)), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

Used terms: n1

Proof step 110 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  ii(0) = 0, ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, finp(σ) → # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0)), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ af.drop(ii(n)).take(# alf(n)) = alf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 111 from proof infappend-frags (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: m

Proof step 112 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 113:

  ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2) ∧ ⌜ii(n2 + 1)⌝ < # σ ∧ ii(n2 + 1) = ii(n2) + # alf(n2)

Rule argument

Additional information

Used terms: n2

Proof step 113 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 114:

  ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # slf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# slf(n)) = slf(n) ⊦ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2) ∧ ⌜ii(n2 + 1)⌝ < # σ

Rule argument

Additional information

Proof step 114 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 115:

  ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2) ∧ ⌜ii(n2 + 1)⌝ < # σ

Rule argument

Additional information

Used terms: n2

Proof step 115 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 116:

  ii(n2 + 1) = ii(n2) + # slf(n2) - 1, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Proof step 116 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 117:

  ⊦ m ≤ n ∧ ¬ # σ < ⌜n⌝ → σ.take(n).drop(m) = σ.drop(m).take(n - m)

• Proof step 118:

  ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2), ii(n2) ≤ ii(n2 + 1) + 1 ∧ ¬ # σ < ⌜ii(n2 + 1) + 1⌝

• Proof step 120:

  ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ⌜ii(n2 + 1)⌝ < # σ, ii(n2) ≤ ii(n2 + 1) + 1, ¬ # σ < ⌜ii(n2 + 1) + 1⌝ , ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.drop(ii(n2)).take(ii(n2 + 1) + 1 - ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used terms: σ, ii(n2 + 1) + 1, ii(n2)

Proof step 117 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 118 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 119:

  ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ii(n2 + 1) + 1 < ii(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.take(ii(n2 + 1) + 1).drop(ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ # σ < ⌜n⌝ + ⌜1⌝ ↔ ¬ ⌜n⌝ < # σ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 119 from proof infappend-frags (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ m < n → n ≠ 0; (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: ii(n2) + # slf(n2), m0

Proof step 120 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 121:

  ii(n2 + 1) = ii(n2) + # slf(n2) - 1, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ⌜ii(n2 + 1)⌝ < # σ, ii(n2) ≤ ii(n2 + 1) + 1, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦ σ.drop(ii(n2)).take(ii(n2 + 1) + 1 - ii(n2)) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ # σ < ⌜n⌝ + ⌜1⌝ ↔ ¬ ⌜n⌝ < # σ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 121 from proof infappend-frags (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 122:

  ii(n2 + 1) + 1 = n1 + ii(n2), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ⌜ii(n2 + 1)⌝ < # σ, ii(n2) ≤ ii(n2 + 1) + 1, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.drop(ii(n2)).take(n1) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: ii(n2 + 1) + 1, ii(n2), n1

Proof step 122 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 123:

  ii(n2 + 1) + 1 = n1 + ii(n2), ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.drop(ii(n2)).take(n1) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 123 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 124:

  ii(n2 + 1) + 1 = n1 + ii(n2), slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # slf(n2) - 1, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ⌜ii(n2 + 1)⌝ < # σ, frag*(IOAut(start, step, ext))(slf(n2), alf(n2)), ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦ σ.drop(ii(n2)).take(n1) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used terms: n2

Proof step 124 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 125:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 126:

  # ⌜slf(n2)⌝ = # ⌜alf(n2)⌝ + ⌜1⌝ , ii(n2 + 1) + 1 = n1 + ii(n2), slf(n2 + 1).head = slf(n2).last, ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ n. ⌜n⌝ < # ⌜alf(n2)⌝ → step(⌜slf(n2)⌝ [n], ⌜alf(n2)⌝ [n], ⌜slf(n2)⌝ [n +1]) ⊦ σ.drop(ii(n2)).take(n1) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used terms: ext, ⌜alf(n2)⌝ , step, start, ⌜slf(n2)⌝

Proof step 125 from proof infappend-frags (previous step) (back to tree)

Lemma frag

Proof step 126 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 127:

  ii(n2 + 1) + 1 = n1 + ii(n2), # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # slf(n2) - 1, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦ σ.drop(ii(n2)).take(n1) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s)

Proof step 127 from proof infappend-frags (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 128:

  # alf(n2) + 1 = # slf(n2), ii(n2 + 1) + 1 = n1 + ii(n2), ii(n2) + # slf(n2) = m0 + 1, slf(n2 + 1).head = slf(n2).last, ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii(n2 + 1) = m0, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ii(n2) + # slf(n2) ≠ 0, ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ σ.drop(ii(n2)).take(n1) = slf(n2) ∧ α.take(ii(n2 + 1)).drop(ii(n2)) = alf(n2)

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: ii(n2) + # slf(n2), m0

Proof step 128 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 129:

  ii(n2 + 1) + 1 = # slf(n2) + ii(n2), # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), # slf(n2) + ii(n2) ≠ 0, α.take(ii(n2 + 1)).drop(ii(n2)) ≠ alf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: 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)

Proof step 129 from proof infappend-frags (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 130:

  ii(n2 + 1) + 1 = (# alf(n2) + 1) + ii(n2), slf(n2 + 1).head = slf(n2).last, ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# alf(n2) + 1) = slf(n2), (# alf(n2) + 1) + ii(n2) ≠ 0, α.take(ii(n2 + 1)).drop(ii(n2)) ≠ alf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦

Rule argument

Additional information

Proof step 130 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 131:

  slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = # alf(n2) + ii(n2), ii(0) = 0, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# alf(n2) + 1) = slf(n2), α.take(ii(n2 + 1)).drop(ii(n2)) ≠ alf(n2), ⌜ii(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 131 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 132:

  ⊦ m ≤ n ∧ ¬ # σ < ⌜n⌝ → σ.take(n).drop(m) = σ.drop(m).take(n - m)

• Proof step 133:

  slf(n2 + 1).head = slf(n2).last, ii(0) = 0, ii(n2 + 1) = # alf(n2) + ii(n2), σ.drop(ii(n2)).take(# alf(n2) + 1) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), α.drop(ii(n2)).take(ii(n2 + 1) - ii(n2)) ≠ alf(n2), ⌜ii(n2 + 1)⌝ < # σ, ii(n2) ≤ ii(n2 + 1), ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii(m) = ii(n0));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n3. n3 < # alf(n2) → step(slf(n2)[n3], alf(n2)[n3], slf(n2)[n3 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: α, ii(n2 + 1), ii(n2)

Proof step 132 from proof infappend-frags (previous step) (back to tree)

A spec-lemma

Proof step 133 from proof infappend-frags (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: ii(n2 + 1), ii(n2), n1

Proof step 134 from proof infappend-frags (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 135:

  ii(0) = 0, ii0(0) = 0, ii0(n1) ≠ ii(n1), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦ ∃ σ, α, ii. frag(IOAut(start, step, ext))(σ, α) ∧ ii(0) = 0 ∧ (finp(α) ⊃ ∃ n. # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ⌜ii(n + 1)⌝ < # σ ∧ α.take(ii(n + 1)).drop(ii(n)) = alf(n) ∧ σ.take(ii(n + 1) + 1).drop(ii(n)) = slf(n))

Rule argument

Additional information

Proof step 135 from proof infappend-frags (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 136:

  ii(0) = 0, ii0(0) = 0, ii0(n1) ≠ ii(n1), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Proof step 136 from proof infappend-frags (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 137:

  ii(0) = 0, ii0(0) = 0, ii0(n2 +1) ≠ ii(n2 +1), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ ii, ii0, σ, n0, slf, α, n, alf, start, step, ext. ¬ ( ii(0) = 0 ∧ ii0(0) = 0 ∧ ii0(n2) ≠ ii(n2) ∧ (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)) ∧ (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n)) ∧ (∀ m, n. m ≤ n → ii0(m) ≤ ii0(n)) ∧ (∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n))) ⊦

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

Proof step 137 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 138:

  ii(0) = 0, ii0(0) = 0, ii0(n2 + 1) ≠ ii(n2 + 1), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n), ∀ ii1, ii2, σ0, n1, slf0, α0, n3, alf0, start0, step0, ext0. ii1(0) ≠ 0 ∨ ii2(0) ≠ 0 ∨ ii2(n2) = ii1(n2) ∨ ¬ (finp(σ0) ⊃ # σ0 = ⌜ii2(n1)⌝ + ⌜1⌝ ∧ (∀ m. n1 ≤ m → slf0(m).tail = [] ∧ ii2(m) = ii2(n1));∀ n. ∃ m. ii2(m) ≤ n ∧ n < ii2(m + 1)) ∨ ¬ (finp(α0) ⊃ # α0 = ⌜ii1(n3)⌝ ∧ (∀ m. n3 ≤ m → alf0(m) = [] ∧ ii1(m) = ii1(n3));∀ n. ∃ m. ii1(m) ≤ n ∧ n < ii1(m + 1)) ∨ ¬(∀ n. frag*(IOAut(start0, step0, ext0))(slf0(n), alf0(n)) ∧ slf0(n + 1).head = slf0(n).last) ∨ ¬(∀ m, n. m ≤ n → ii1(m) ≤ ii1(n)) ∨ ¬(∀ n. ii1(n + 1) = ii1(n) + # alf0(n) ∧ ¬ # α0 < ⌜ii1(n + 1)⌝ ∧ α0.drop(ii1(n)).take(# alf0(n)) = alf0(n)) ∨ ¬(∀ m, n. m ≤ n → ii2(m) ≤ ii2(n)) ∨ ¬(∀ n. ii2(n + 1) = ii2(n) + # slf0(n) - 1 ∧ ⌜ii2(n + 1)⌝ < # σ0 ∧ σ0.drop(ii2(n)).take(# slf0(n)) = slf0(n)) ⊦

Rule argument

Additional information

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

Proof step 138 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 139:

  ii(0) = 0, ii0(0) = 0, ii0(n2 + 1) ≠ ii(n2 + 1), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ii(0) ≠ 0 ∨ ii0(0) ≠ 0 ∨ ii0(n2) = ii(n2) ∨ ¬ (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)) ∨ ¬ (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∨ ¬(∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last) ∨ ¬(∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∨ ¬(∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n)) ∨ ¬(∀ m, n. m ≤ n → ii0(m) ≤ ii0(n)) ∨ ¬(∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n)) ⊦

Rule argument

Additional information

Used terms: ii, ii0, σ, n0, slf, α, n, alf, start, step, ext

Proof step 139 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 140:

  ii(0) = 0, ii0(0) = 0, ii0(n2) = ii(n2), ii0(n2 + 1) ≠ ii(n2 + 1), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # alf(n) ∧ ¬ # α < ⌜ii(n + 1)⌝ ∧ α.drop(ii(n)).take(# alf(n)) = alf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n) ⊦

Rule argument

Additional information

Proof step 140 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 141:

  ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii0(n2) = ii(n2), ii0(0) = 0, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ii0(n2 + 1) ≠ ii(n2 + 1), ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), ∀ n. ii0(n + 1) = ii0(n) + # slf(n) - 1 ∧ ⌜ii0(n + 1)⌝ < # σ ∧ σ.drop(ii0(n)).take(# slf(n)) = slf(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦

Rule argument

Additional information

Used terms: n2

Proof step 141 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 142:

  ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii0(0) = 0, ii0(n2) = ii(n2), ii0(n2 + 1) = ii0(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii0(n2)).take(# slf(n2)) = slf(n2), ii0(n2 + 1) ≠ ii(n2 + 1), ⌜ii0(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n) ⊦

Rule argument

Additional information

Used terms: n2

Proof step 142 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 143:

  ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii0(n2 + 1) = ii(n2) + # slf(n2) - 1, ii0(n2) = ii(n2), ii0(0) = 0, σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ii0(n2 + 1) ≠ ii(n2 + 1), ⌜ii0(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. frag*(IOAut(start, step, ext))(slf(n), alf(n)) ∧ slf(n + 1).head = slf(n).last ⊦

Rule argument

Additional information

Proof step 143 from proof infappend-frags (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 144:

  slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii0(0) = 0, ii0(n2) = ii(n2), ii0(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ii0(n2 + 1) ≠ ii(n2 + 1), ⌜ii0(n2 + 1)⌝ < # σ, frag*(IOAut(start, step, ext))(slf(n2), alf(n2)), ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n) ⊦

Rule argument

Additional information

Used terms: n2

Proof step 144 from proof infappend-frags (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 145:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 146:

  # ⌜slf(n2)⌝ = # ⌜alf(n2)⌝ + ⌜1⌝ , slf(n2 + 1).head = slf(n2).last, ii(0) = 0, ii(n2 + 1) = ii(n2) + # alf(n2), ii0(n2 + 1) = ii(n2) + # slf(n2) - 1, ii0(n2) = ii(n2), ii0(0) = 0, σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), α.drop(ii(n2)).take(# alf(n2)) = alf(n2), ii0(n2 + 1) ≠ ii(n2 + 1), ⌜ii0(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ⌜n⌝ < # ⌜alf(n2)⌝ → step(⌜slf(n2)⌝ [n], ⌜alf(n2)⌝ [n], ⌜slf(n2)⌝ [n +1]) ⊦

Rule argument

Additional information

Used terms: ext, ⌜alf(n2)⌝ , step, start, ⌜slf(n2)⌝

Proof step 145 from proof infappend-frags (previous step) (back to tree)

Lemma frag

Proof step 146 from proof infappend-frags (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 147:

  # alf(n2) + 1 = # slf(n2), slf(n2 + 1).head = slf(n2).last, ii(n2 + 1) = ii(n2) + # alf(n2), ii(0) = 0, ii0(0) = 0, ii0(n2) = ii(n2), ii0(n2 + 1) = ii(n2) + # slf(n2) - 1, α.drop(ii(n2)).take(# alf(n2)) = alf(n2), σ.drop(ii(n2)).take(# slf(n2)) = slf(n2), ii0(n2 + 1) ≠ ii(n2 + 1), ⌜ii0(n2 + 1)⌝ < # σ, ¬ # α < ⌜ii(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii0(n0)⌝ + ⌜1⌝ ∧ (∀ m. n0 ≤ m → slf(m).tail = [] ∧ ii0(m) = ii0(n0));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)), (finp(α) ⊃ # α = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → alf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m, n. m ≤ n → ii0(m) ≤ ii0(n), ∀ n1. n1 < # alf(n2) → step(slf(n2)[n1], alf(n2)[n1], slf(n2)[n1 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s)

Proof step 147 from proof infappend-frags (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic