Proof step 1 from proof readFOsOk-add-FO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  notMember(t, writers), readFOsOk(rfo, writers), ¬ readFOsOk(rfo(t := rfo(t) + FO(l) '), writers) ⊦

Rule argument

Additional information

Proof step 2 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  notMember(t, writers), ∀ t. rfo(t).forall(.FO?), ∀ t, l. t ∈ writers(l) → rfo(t) = [] ⊦ (t = t0 ⊃ rfo(t0) + FO(l) ';rfo(t0)).forall(.FO?) ∧ (t1 ∈ writers(l0) → (t = t1 ⊃ rfo(t1) + FO(l) ';rfo(t1)) = [])

Rule argument

Additional information

Used simplifier rules: readFOsOk: ⊦ readFOsOk(rfo, writers) ↔ rfo.FOs? ∧ (∀ t, l. t ∈ writers(l) → rfo(t) = []); FOs: ⊦ rfo.FOs? ↔ (∀ t. rfo(t).forall(.FO?));

Proof step 3 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

  notMember(t, writers), ¬ (t = t0 ⊃ rfo(t0) + FO(l) ';rfo(t0)).forall(.FO?), ∀ t, l. t ∈ writers(l) → rfo(t) = [], ∀ t. rfo(t).forall(.FO?) ⊦

• Proof step 8:

  (t = t1 ⊃ rfo(t1) + FO(l) ';rfo(t1)) ≠ [], notMember(t, writers), t1 ∈ writers(l0), ∀ t, l. t ∈ writers(l) → rfo(t) = [], ∀ t. rfo(t).forall(.FO?) ⊦

Rule argument

Additional information

Proof step 4 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 5:

  t = t0, notMember(t, writers), ¬ (rfo(t0) + FO(l) ').forall(.FO?), ∀ t. rfo(t).forall(.FO?), ∀ t, l. t ∈ writers(l) → rfo(t) = [] ⊦

• Proof step 7:

  t ≠ t0, notMember(t, writers), ¬ rfo(t0).forall(.FO?), ∀ t. rfo(t).forall(.FO?), ∀ t, l. t ∈ writers(l) → rfo(t) = [] ⊦

Rule argument

Additional information

Proof step 5 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  notMember(t0, writers), ¬ (rfo(t0) + FO(l) ').forall(.FO?), ∀ t, l. t ∈ writers(l) → rfo(t) = [], ∀ t. rfo(t).forall(.FO?) ⊦

Rule argument

Additional information

Proof step 6 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (x + y).forall(p) ↔ x.forall(p) ∧ y.forall(p); (ws) ⊦ a '.forall(p) ↔ p(a); (s) ⊦ FO(l).FO?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: t0

Proof step 7 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0

Proof step 8 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # writers(l0) ≠ 0, (t = t1 ⊃ rfo(t1) + FO(l) ';rfo(t1)) ≠ [], writers(l0) ≠ ∅, notMember(t, writers), t1 ∈ writers(l0), ∀ t, l. t ∈ writers(l) → rfo(t) = [], ∀ t. rfo(t).forall(.FO?) ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 9 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  # writers(l0) ≠ 0, (t = t1 ⊃ rfo(t1) + FO(l) ';rfo(t1)) ≠ [], t ≠ t1, writers(l0) ≠ ∅, notMember(t, writers), t1 ∈ writers(l0), ∀ t. rfo(t).forall(.FO?), ∀ t, l. t ∈ writers(l) → rfo(t) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ notMember(t, tsf) → ¬ t ∈ tsf(l); (as) Used formulas: t = t1

Proof step 10 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # writers(l0) ≠ 0, rfo(t1) ≠ [], t ≠ t1, writers(l0) ≠ ∅, notMember(t, writers), t1 ∈ writers(l0), ∀ t, l. t ∈ writers(l) → rfo(t) = [], ∀ t. rfo(t).forall(.FO?) ⊦

Rule argument

Additional information

Proof step 11 from proof readFOsOk-add-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t1, l0