Proof step 1 from proof int-le-floor (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i ≤ ⌊r⌋ ↔ i.r ≤ r) ⊦

Rule argument

Additional information

Proof step 2 from proof int-le-floor (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(i ≤ ⌊r⌋ ↔ i.r ≤ r) ⊦

Rule argument

Additional information

Proof step 3 from proof int-le-floor (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  i ≤ ⌊r⌋ , ¬ i.r ≤ r ⊦

• Proof step 9:

  i.r ≤ r, ¬ i ≤ ⌊r⌋ ⊦

Rule argument

Additional information

Proof step 4 from proof int-le-floor (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  i ≤ ⌊r⌋ , r < i.r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 5 from proof int-le-floor (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ⌊r⌋ .r ≤ r

• Proof step 7:

  i ≤ ⌊r⌋ , r < i.r, ⌊r⌋ .r ≤ r ⊦

Rule argument

Additional information

Used terms: r

Proof step 6 from proof int-le-floor (previous step) (back to tree)

Lemma floor-le

Proof step 7 from proof int-le-floor (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  ⊦ r ≤ r0 ∧ r0 ≤ r1 → r ≤ r1

Rule argument

Additional information

Used simplifier rules: floor-le: ⊦ ⌊r⌋ .r ≤ r; ⊦ i.r ≤ j.r ↔ i ≤ j; (s) ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: i.r, ⌊r⌋ .r, r

Proof step 8 from proof int-le-floor (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof int-le-floor (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  ⊦ r < ⌊r⌋ .r + 1.r

• Proof step 11:

  i.r ≤ r, r < ⌊r⌋ .r + 1.r, ¬ i ≤ ⌊r⌋ ⊦

Rule argument

Additional information

Used terms: r

Proof step 10 from proof int-le-floor (previous step) (back to tree)

Lemma floor-gr-subone

Proof step 11 from proof int-le-floor (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  ⊦ r ≤ r0 ∧ r0 < r1 → r < r1

• Proof step 13:

  i.r ≤ r, r < ⌊r⌋ .r + 1.r, ¬ i ≤ ⌊r⌋ , i.r ≤ r ∧ r < ⌊r⌋ .r + 1.r → i.r < ⌊r⌋ .r + 1.r ⊦

Rule argument

Additional information

Used terms: i.r, r, ⌊r⌋ .r + 1.r

Proof step 12 from proof int-le-floor (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof int-le-floor (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  i.r ≤ r, i.r < ⌊r⌋ .r + 1.r, r < ⌊r⌋ .r + 1.r, ¬ i ≤ ⌊r⌋ ⊦

Rule argument

Additional information

Used simplifier rules: floor-gr-subone: ⊦ r < ⌊r⌋ .r + 1.r; ⊦ i ≤ j ↔ ¬ j < i; (ss) add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic

Proof step 14 from proof int-le-floor (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ (* i).r + (* j).r = (i + j).r

Rule argument

Additional information

Used simplifier rules: ⊦ i.r < j.r ↔ i < j; (s) ⊦ i < j + 1 ↔ i ≤ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i ≤ j → ¬ j < i; (s) Used terms: ⌊r⌋ , 1

Proof step 15 from proof int-le-floor (previous step) (back to tree)

A spec-lemma