Information

Trace generated on 26.1.2026 at 12:55
Trace length: 48
Specification file (xtl): GetPositiveElements/GetPositiveElements.pl
Git revision of file: 100644 9a8cb7b5c62e23f9d739d9e7753a0415cd9479a6 0 GetPositiveElements.pl
Git revision of repository HEAD: a129bd4b378f4883186191b9f02623d1059a2525
ProB version: 1.16.0-nightly
ProB revision: 25fadf907101913f4f3f41a98fdcdc96920fbb46 (Mon Jan 26 07:56:17 2026 +0100)

1. step_neg/inv3/INV (true)

(start_xtl_system)

`e ≤ 0 ∧ e ∈ elements`
`elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`---------------------`
`elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

2. reselect_hyp (pos ⊆ ELEMENTS)

(reselect_hyp(subset($(pos),$('ELEMENTS'))))

`e ≤ 0 ∧ e ∈ elements`
`elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`pos ⊆ ELEMENTS`
`---------------------`
`elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

3. reselect_hyp (elements ⊆ ELEMENTS)

(reselect_hyp(subset($(elements),$('ELEMENTS'))))

`e ≤ 0 ∧ e ∈ elements`
`elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`---------------------`
`elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

4. reselect_hyp (ELEMENTS ⊂ ℤ)

(reselect_hyp(subset_strict($('ELEMENTS'),'INTEGER')))

`e ≤ 0 ∧ e ∈ elements`
`elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`---------------------`
`elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

5. reselect_hyp (pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})

(reselect_hyp(equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))))

`e ≤ 0 ∧ e ∈ elements`
`elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`---------------------`
`elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

6. reselect_hyp (finite(ELEMENTS))

(reselect_hyp(finite($('ELEMENTS'))))

`e ≤ 0 ∧ e ∈ elements`
`elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`finite(ELEMENTS)`
`---------------------`
`elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

7. imp_r

`e ≤ 0 ∧ e ∈ elements`
`elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`---------------------`
`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

8. imp_case (elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x})

(imp_case(implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))))))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`pos ⊆ ELEMENTS`	`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`	`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`---------------------`	`---------------------`
`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`	`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

9. skip_to_cont

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`pos ⊆ ELEMENTS`	`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`	`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`	`¬(elements = ∅)`
`---------------------`	`---------------------`
`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`	`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

10. hyp

`e ≤ 0 ∧ e ∈ elements`
`pos ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`---------------------`
`pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

11. eq (lr,pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})

(eq(lr,$(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`---------------------`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} = {x·0 < x ∧ x ∈ ELEMENTS∣x}`

12. DERIV_EQUAL ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} = {x·0 < x ∧ x ∈ ELEMENTS∣x})

(simplify_goal('DERIV_EQUAL'))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`---------------------`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x} ∧ {x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

13. and_r

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`---------------------`	`---------------------`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x}`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

14. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS)

(simplify_hyp('DEF_SUBSETEQ',subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS'))))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`---------------------`	`---------------------`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x}`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

15. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x})

(simplify_goal('DEF_SUBSETEQ'))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`---------------------`	`---------------------`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}))`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

16. all_r

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`---------------------`	`---------------------`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

17. imp_r

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`	`---------------------`
`---------------------`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}`

18. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})

(simplify_goal('SIMP_IN_COMPSET_ONEPOINT'))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`	`---------------------`
`---------------------`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`0 < y ∧ y ∈ ELEMENTS`

19. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})

(simplify_hyp('SIMP_IN_COMPSET_ONEPOINT',member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y ∧ y ∈ ELEMENTS ∖ elements`	`---------------------`
`---------------------`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`0 < y ∧ y ∈ ELEMENTS`

20. and_l (0 < y ∧ y ∈ ELEMENTS ∖ elements)

(and_l(conjunct(less(0,$(y)),member($(y),set_subtraction($('ELEMENTS'),$(elements))))))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`---------------------`
`y ∈ ELEMENTS ∖ elements`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`---------------------`
`0 < y ∧ y ∈ ELEMENTS`

21. and_r

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`0 < y`	`---------------------`
`y ∈ ELEMENTS ∖ elements`	`y ∈ ELEMENTS ∖ elements`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`---------------------`	`---------------------`
`0 < y`	`y ∈ ELEMENTS`

22. hyp

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`---------------------`
`y ∈ ELEMENTS ∖ elements`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`---------------------`
`y ∈ ELEMENTS`

23. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)

(simplify_hyp('DEF_IN_SETMINUS',member($(y),set_subtraction($('ELEMENTS'),$(elements)))))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`---------------------`
`y ∈ ELEMENTS ∧ ¬(y ∈ elements)`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`---------------------`
`y ∈ ELEMENTS`

24. and_l (y ∈ ELEMENTS ∧ ¬(y ∈ elements))

(and_l(conjunct(member($(y),$('ELEMENTS')),negation(member($(y),$(elements))))))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`---------------------`
`y ∈ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`
`¬(y ∈ elements)`
`---------------------`
`y ∈ ELEMENTS`

25. hyp

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`---------------------`
`{x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

26. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})

(simplify_goal('DEF_SUBSETEQ'))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`---------------------`
`(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x} ⇒ y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}))`

27. all_r

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`---------------------`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x} ⇒ y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

28. imp_r

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`---------------------`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}`

29. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})

(simplify_goal('SIMP_IN_COMPSET_ONEPOINT'))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}`
`---------------------`
`0 < y ∧ y ∈ ELEMENTS ∖ elements`

30. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})

(simplify_hyp('SIMP_IN_COMPSET_ONEPOINT',member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`0 < y ∧ y ∈ ELEMENTS`
`---------------------`
`0 < y ∧ y ∈ ELEMENTS ∖ elements`

31. and_l (0 < y ∧ y ∈ ELEMENTS)

(and_l(conjunct(less(0,$(y)),member($(y),$('ELEMENTS')))))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`---------------------`
`0 < y ∧ y ∈ ELEMENTS ∖ elements`

32. and_r

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`elements ∖ {e} = ∅`	`elements ∖ {e} = ∅`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`0 < y`
`y ∈ ELEMENTS`	`y ∈ ELEMENTS`
`---------------------`	`---------------------`
`0 < y`	`y ∈ ELEMENTS ∖ elements`

33. hyp

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ∖ {e} = ∅`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`---------------------`
`y ∈ ELEMENTS ∖ elements`

34. SIMP_SETMINUS_EQUAL_EMPTY (elements ∖ {e} = ∅)

(simplify_hyp('SIMP_SETMINUS_EQUAL_EMPTY',equal(set_subtraction($(elements),set_extension([$(e)])),empty_set)))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`elements ⊆ {e}`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`---------------------`
`y ∈ ELEMENTS ∖ elements`

35. DEF_SUBSETEQ (elements ⊆ {e})

(simplify_hyp('DEF_SUBSETEQ',subset($(elements),set_extension([$(e)]))))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`(∀x·(x ∈ elements ⇒ x ∈ {e}))`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`---------------------`
`y ∈ ELEMENTS ∖ elements`

36. ∀ instantiation in hyp 6 for ID x: 'y'

(forall_inst(6,y))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`y ∈ elements ⇒ y ∈ {e}`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`---------------------`
`y ∈ ELEMENTS ∖ elements`

37. imp_case (y ∈ elements ⇒ y ∈ {e})

(imp_case(implication(member($(y),$(elements)),member($(y),set_extension([$(e)])))))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`0 < y`
`y ∈ ELEMENTS`	`y ∈ ELEMENTS`
`¬(y ∈ elements)`	`y ∈ {e}`
`---------------------`	`---------------------`
`y ∈ ELEMENTS ∖ elements`	`y ∈ ELEMENTS ∖ elements`

38. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)

(simplify_goal('DEF_IN_SETMINUS'))

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`0 < y`
`y ∈ ELEMENTS`	`y ∈ ELEMENTS`
`¬(y ∈ elements)`	`y ∈ {e}`
`---------------------`	`---------------------`
`y ∈ ELEMENTS ∧ ¬(y ∈ elements)`	`y ∈ ELEMENTS ∖ elements`

39. and_r

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`	`finite(ELEMENTS)`
`¬(elements = ∅)`	`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`0 < y`	`0 < y`
`y ∈ ELEMENTS`	`y ∈ ELEMENTS`	`y ∈ ELEMENTS`
`¬(y ∈ elements)`	`¬(y ∈ elements)`	`y ∈ {e}`
`---------------------`	`---------------------`	`---------------------`
`y ∈ ELEMENTS`	`¬(y ∈ elements)`	`y ∈ ELEMENTS ∖ elements`

40. hyp

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`0 < y`
`y ∈ ELEMENTS`	`y ∈ ELEMENTS`
`¬(y ∈ elements)`	`y ∈ {e}`
`---------------------`	`---------------------`
`¬(y ∈ elements)`	`y ∈ ELEMENTS ∖ elements`

41. hyp

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`y ∈ {e}`
`---------------------`
`y ∈ ELEMENTS ∖ elements`

42. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)

(simplify_goal('DEF_IN_SETMINUS'))

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`y ∈ {e}`
`---------------------`
`y ∈ ELEMENTS ∧ ¬(y ∈ elements)`

43. and_r

`e ≤ 0 ∧ e ∈ elements`	`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`	`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`	`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`	`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`	`finite(ELEMENTS)`
`¬(elements = ∅)`	`¬(elements = ∅)`
`0 < y`	`0 < y`
`y ∈ ELEMENTS`	`y ∈ ELEMENTS`
`y ∈ {e}`	`y ∈ {e}`
`---------------------`	`---------------------`
`y ∈ ELEMENTS`	`¬(y ∈ elements)`

44. hyp

`e ≤ 0 ∧ e ∈ elements`
`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`y ∈ {e}`
`---------------------`
`¬(y ∈ elements)`

45. and_l (e ≤ 0 ∧ e ∈ elements)

(and_l(conjunct(less_equal($(e),0),member($(e),$(elements)))))

`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`y ∈ {e}`
`e ≤ 0`
`e ∈ elements`
`---------------------`
`¬(y ∈ elements)`

46. SIMP_IN_SING (y ∈ {e})

(simplify_hyp('SIMP_IN_SING',member($(y),set_extension([$(e)]))))

`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`y = e`
`e ≤ 0`
`e ∈ elements`
`---------------------`
`¬(y ∈ elements)`

47. eq (rl,y = e)

(eq(rl,$(y),$(e)))

`{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS`
`elements ⊆ ELEMENTS`
`ELEMENTS ⊂ ℤ`
`finite(ELEMENTS)`
`¬(elements = ∅)`
`0 < y`
`y ∈ ELEMENTS`
`y ≤ 0`
`y ∈ elements`
`---------------------`
`¬(y ∈ elements)`

48. cntr

`Proof of step_neg/inv3/INV (true) succeeded.`