Proof step 1 from proof pfxclosed-lift-tr (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pfxclosed(trlp), ¬ pfxclosed(lift(trlp)) ⊦

Rule argument

Additional information

Proof step 2 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ pfxclosed(trlp) ↔ (∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1))

• Proof step 4:

  ¬ pfxclosed(lift(trlp)), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used terms: trlp

Proof step 3 from proof pfxclosed-lift-tr (previous step) (back to tree)

Lemma pdfclosedtrl-def

Proof step 4 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ pfxclosed(trp) ↔ (∀ σ1, σ2, α1, α2. trp(σ2, α2) ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 ∧ # σ1 = # α1 + ⌜1⌝ ∧ # σ2 = # α2 + ⌜1⌝ → trp(σ1, α1))

• Proof step 6:

  ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1), ∃ σ1, σ2, α1, α2. ¬(lift(trlp)(σ2, α2) ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 ∧ # σ1 = # α1 + ⌜1⌝ ∧ # σ2 = # α2 + ⌜1⌝ → lift(trlp)(σ1, α1)) ⊦

Rule argument

Additional information

Used terms: lift(trlp)

Proof step 5 from proof pfxclosed-lift-tr (previous step) (back to tree)

Lemma pdfclosedtr-def

Proof step 6 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # σ1 = # α1 + ⌜1⌝ , # σ2 = # α2 + ⌜1⌝ , lift(trlp)(σ2, α2), σ1 ⊑ σ2, α1 ⊑ α2, ¬ lift(trlp)(σ1, α1), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Proof step 7 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  # σ2 = # α2 + ⌜1⌝ , # σ1 = # α1 + ⌜1⌝ , α1 = ⌜al⌝ , lift(trlp)(σ2, α2), α1 ⊑ α2, σ1 ⊑ σ2, ¬ lift(trlp)(σ1, α1), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

• Proof step 30:

  # σ2 = # α2 + ⌜1⌝ , # σ1 = # α1 + ⌜1⌝ , α1 = ⌜af⌝ , lift(trlp)(σ2, α2), α1 ⊑ α2, σ1 ⊑ σ2, ¬ lift(trlp)(σ1, α1), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝;

Proof step 8 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # σ2 = # α2 + ⌜1⌝ , # σ1 = ⌜# al⌝ + ⌜1⌝ , lift(trlp)(σ2, α2), σ1 ⊑ σ2, ⌜al⌝ ⊑ α2, ¬ lift(trlp)(σ1, ⌜al⌝ ), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 9 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  # σ1 = ⌜# al⌝ + ⌜1⌝ , # σ2 = # α2 + ⌜1⌝ , σ1 = ⌜sl⌝ , lift(trlp)(σ2, α2), ⌜al⌝ ⊑ α2, σ1 ⊑ σ2, ¬ lift(trlp)(σ1, ⌜al⌝ ), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝; ⊦ # ⌜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 10 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # σ2 = # α2 + ⌜1⌝ , # al + 1 = # sl, lift(trlp)(σ2, α2), ⌜sl⌝ ⊑ σ2, ⌜al⌝ ⊑ α2, ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: lift-trp-fin: ⊦ lift(trlp)(⌜sl⌝ , ⌜al⌝ ) ↔ trlp(sl, al); 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)

Proof step 11 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  # σ2 = # α2 + ⌜1⌝ , # al + 1 = # sl, σ2 = ⌜sl0⌝ , lift(trlp)(σ2, α2), ⌜al⌝ ⊑ α2, ⌜sl⌝ ⊑ σ2, ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

• Proof step 16:

  # σ2 = # α2 + ⌜1⌝ , # al + 1 = # sl, σ2 = ⌜sf⌝ , lift(trlp)(σ2, α2), ⌜al⌝ ⊑ α2, ⌜sl⌝ ⊑ σ2, ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝;

Proof step 12 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # al + 1 = # sl, ⌜# sl0⌝ = # α2 + ⌜1⌝ , lift(trlp)(⌜sl0⌝ , α2), ⌜al⌝ ⊑ α2, sl ⊑ sl0, ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 13 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 14:

  # al + 1 = # sl, α2 = ⌜al0⌝ , ⌜# sl0⌝ = # α2 + ⌜1⌝ , lift(trlp)(⌜sl0⌝ , α2), sl ⊑ sl0, ⌜al⌝ ⊑ α2, ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜m⌝ + ∞ = ∞; (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 ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 14 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # al + 1 = # sl, # al0 + 1 = # sl0, trlp(sl0, al0), al ⊑ al0, sl ⊑ sl0, ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: lift-trp-fin: ⊦ lift(trlp)(⌜sl⌝ , ⌜al⌝ ) ↔ trlp(sl, al); ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (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)

Proof step 15 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: sl, sl0, al, al0

Proof step 16 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # α2 = ∞, # al + 1 = # sl, lift(trlp)(⌜sf⌝ , α2), ⌜sl⌝ ⊑ ⌜sf⌝ , ⌜al⌝ ⊑ α2, ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

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 ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 17 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 18:

  # α2 = ∞, # al + 1 = # sl, α2 = ⌜af⌝ , lift(trlp)(⌜sf⌝ , α2), ⌜al⌝ ⊑ α2, ⌜sl⌝ ⊑ ⌜sf⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝; ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 18 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # al + 1 = # sl, ⌜sl⌝ ⊑ ⌜sf⌝ , ⌜al⌝ ⊑ ⌜af⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1), ∀ n. trlp(sf.take(n + 1), af.take(n)) ⊦

Rule argument

Additional information

Used simplifier rules: lift-trp-inf: ⊦ lift(trlp)(⌜sf⌝ , ⌜af⌝ ) ↔ (∀ n. trlp(sf.take(n + 1), af.take(n))); ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 19 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  # al + 1 = # sl, trlp(sf.take(# al + 1), af.take(# al)), ⌜al⌝ ⊑ ⌜af⌝ , ⌜sl⌝ ⊑ ⌜sf⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used terms: # al

Proof step 20 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # al + 1 = # sl, trlp(sf.take(# sl), af.take(# al)), ⌜sl⌝ ⊑ ⌜sf⌝ , ⌜al⌝ ⊑ ⌜af⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Proof step 21 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 22:

  # al0 = # al, # al + 1 = # sl, af = (⌜al0⌝ + ⌜nf0⌝ ).f, trlp(sf.take(# sl), al0), ⌜al⌝ ⊑ ⌜af⌝ , ⌜sl⌝ ⊑ ⌜sf⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x0 = nf.take(n) ∧ nf0 = nf.drop(n) ↔ nf = (⌜x0⌝ + ⌜nf0⌝ ).f ∧ # x0 = n; (elim) Used terms: af, # al, al0, nf0

Proof step 22 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # al0 = # al, # al + 1 = # sl, trlp(sf.take(# sl), al0), ⌜sl⌝ ⊑ ⌜sf⌝ , ⌜al⌝ ⊑ ⌜al0⌝ + ⌜nf0⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x + nf⌝ = ⌜x⌝ + ⌜nf⌝ ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜nf⌝ ).f = x + nf; (s)

Proof step 23 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  # al0 = # al, # sl0 = # sl, # al + 1 = # sl, sf = (⌜sl0⌝ + ⌜sf0⌝ ).f, trlp(sl0, al0), ⌜al⌝ ⊑ ⌜al0⌝ + ⌜nf0⌝ , ⌜sl⌝ ⊑ ⌜sf⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x0 = nf.take(n) ∧ nf0 = nf.drop(n) ↔ nf = (⌜x0⌝ + ⌜nf0⌝ ).f ∧ # x0 = n; (elim) Used terms: sf, # sl, sl0, sf0

Proof step 24 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  # sl0 = # sl, # al0 = # al, # al + 1 = # sl, trlp(sl0, al0), ⌜al⌝ ⊑ ⌜al0⌝ + ⌜nf0⌝ , ⌜sl⌝ ⊑ ⌜sl0⌝ + ⌜sf0⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x + nf⌝ = ⌜x⌝ + ⌜nf⌝ ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜nf⌝ ).f = x + nf; (s)

Proof step 25 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

• Proof step 27:

  # al0 = # al, # sl0 = # sl, # al + 1 = # sl, trlp(sl0, al0), ⌜al⌝ ⊑ ⌜al0⌝ + ⌜nf0⌝ , ¬ trlp(sl, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1), ∃ σ1. ⌜sl⌝ + σ1 = ⌜sl0⌝ + ⌜sf0⌝ ⊦

Rule argument

Additional information

Used terms: ⌜sl⌝ , ⌜sl0⌝ + ⌜sf0⌝

Proof step 26 from proof pfxclosed-lift-tr (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  # al0 = # al, # al + 1 = # sl0, trlp(sl0, al0), ⌜al⌝ ⊑ ⌜al0⌝ + ⌜nf0⌝ , ¬ trlp(sl0, al), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s)

Proof step 28 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

Rule argument

Additional information

Used simplifier rules: ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: ⌜al⌝ , ⌜al0⌝ + ⌜nf0⌝

Proof step 29 from proof pfxclosed-lift-tr (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # σ2 = # α2 + ⌜1⌝ , # σ1 = ∞, lift(trlp)(σ2, α2), σ1 ⊑ σ2, ⌜af⌝ ⊑ α2, ¬ lift(trlp)(σ1, ⌜af⌝ ), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

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 ⊦ ⌜m⌝ + ∞ = ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 31 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 32:

  # σ1 = ∞, # σ2 = # α2 + ⌜1⌝ , α2 = ⌜af0⌝ , lift(trlp)(σ2, α2), ⌜af⌝ ⊑ α2, σ1 ⊑ σ2, ¬ lift(trlp)(σ1, ⌜af⌝ ), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝; ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ¬ ⌜nf⌝ ⊑ ⌜x⌝ ; (s)

Proof step 32 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # σ2 = ∞, # σ1 = ∞, lift(trlp)(σ2, ⌜af0⌝ ), σ1 ⊑ σ2, ¬ lift(trlp)(σ1, ⌜af0⌝ ), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ ⊑ ⌜nf0⌝ ↔ nf = nf0; (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) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 33 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 34:

  # σ1 = ∞, # σ2 = ∞, σ2 = ⌜sf⌝ , lift(trlp)(σ2, ⌜af0⌝ ), σ1 ⊑ σ2, ¬ lift(trlp)(σ1, ⌜af0⌝ ), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝; ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 34 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # σ1 = ∞, σ1 ⊑ ⌜sf⌝ , ¬ lift(trlp)(σ1, ⌜af0⌝ ), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1), ∀ n. trlp(sf.take(n + 1), af0.take(n)) ⊦

Rule argument

Additional information

Used simplifier rules: lift-trp-inf: ⊦ lift(trlp)(⌜sf⌝ , ⌜af⌝ ) ↔ (∀ n. trlp(sf.take(n + 1), af.take(n))); ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 35 from proof pfxclosed-lift-tr (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 36:

  # σ1 = ∞, σ1 = ⌜sf0⌝ , σ1 ⊑ ⌜sf⌝ , ¬ lift(trlp)(σ1, ⌜af0⌝ ), ∀ n. trlp(sf.take(n + 1), af0.take(n)), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝; ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 36 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  ¬ trlp(sf.take(n + 1), af0.take(n)), ∀ n. trlp(sf.take(n + 1), af0.take(n)), ∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1) ⊦

Rule argument

Additional information

Used simplifier rules: lift-trp-inf: ⊦ lift(trlp)(⌜sf⌝ , ⌜af⌝ ) ↔ (∀ n. trlp(sf.take(n + 1), af.take(n))); ⊦ ⌜nf⌝ ⊑ ⌜nf0⌝ ↔ nf = nf0; (s) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 37 from proof pfxclosed-lift-tr (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n