Proof Trace Export for
step_neg/inv3/INV (true)
from
GetPositiveElements/GetPositiveElements.pl
Proof Steps
< Previous Step
Next Step >
Run Steps
1. reselect_hyp (pos ⊆ ELEMENTS)
2. reselect_hyp (elements ⊆ ELEMENTS)
3. reselect_hyp (ELEMENTS ⊂ ℤ)
4. reselect_hyp (pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
5. reselect_hyp (finite(ELEMENTS))
6. imp_r
7. imp_case (elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x})
8. hyp
9. eq (lr,pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
10. DERIV_EQUAL ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} = {x·0 < x ∧ x ∈ ELEMENTS∣x})
11. and_r
12. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS)
13. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x})
14. all_r
15. imp_r
16. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
17. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
18. and_l (0 < y ∧ y ∈ ELEMENTS ∖ elements)
19. and_r
20. hyp
21. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
22. and_l (y ∈ ELEMENTS ∧ ¬(y ∈ elements))
23. hyp
24. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
25. all_r
26. imp_r
27. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
28. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
29. and_l (0 < y ∧ y ∈ ELEMENTS)
30. and_r
31. hyp
32. SIMP_SETMINUS_EQUAL_EMPTY (elements ∖ {e} = ∅)
33. DEF_SUBSETEQ (elements ⊆ {e})
34. ∀ instantiation in hyp 6 for ID x: 'y'
35. imp_case (y ∈ elements ⇒ y ∈ {e})
36. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
37. and_r
38. hyp
39. hyp
40. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
41. and_r
42. hyp
43. and_l (e ≤ 0 ∧ e ∈ elements)
44. SIMP_IN_SING (y ∈ {e})
45. eq (rl,y = e)
46. cntr
ProB Version: 1.16.0-nightly (25fadf907101913f4f3f41a98fdcdc96920fbb46)
Generated on 26/01/2026 at 12:55
Proof Tree
prob_graph
dot_node_0
Select PO
dot_node_9
e ≤ 0 ∧ e ∈ elements
elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}
elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_0->dot_node_9
step_neg/inv3/INV (true)
dot_node_1
Proven.
dot_node_2
Proven.
dot_node_3
Proven.
dot_node_4
Proven.
dot_node_5
Proven.
dot_node_6
Proven.
dot_node_7
Proven.
dot_node_8
Proven.
dot_node_10
e ≤ 0 ∧ e ∈ elements
elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}
pos ⊆ ELEMENTS
elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_9->dot_node_10
reselect_hyp (pos ⊆ ELEMENTS)
dot_node_11
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}
dot_node_10->dot_node_11
reselect_hyp (elements ⊆ ELEMENTS)
dot_node_12
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}
dot_node_11->dot_node_12
reselect_hyp (ELEMENTS ⊂ ℤ)
dot_node_13
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}
dot_node_12->dot_node_13
reselect_hyp (pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_14
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}
dot_node_13->dot_node_14
reselect_hyp (finite(ELEMENTS))
dot_node_15
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}
dot_node_14->dot_node_15
imp_r
dot_node_16
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}
dot_node_15->dot_node_16
imp_case (elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_17
e ≤ 0 ∧ e ∈ elements
pos ⊆ ELEMENTS
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}
finite(ELEMENTS)
elements ∖ {e} = ∅
pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}
pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_15->dot_node_17
imp_case (elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_18
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}
dot_node_16->dot_node_18
eq (lr,pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_17->dot_node_1
hyp
dot_node_19
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}
dot_node_18->dot_node_19
DERIV_EQUAL ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} = {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_20
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}
dot_node_19->dot_node_20
and_r
dot_node_21
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}
dot_node_19->dot_node_21
and_r
dot_node_22
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_20->dot_node_22
DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS)
dot_node_33
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}))
dot_node_21->dot_node_33
DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_23
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}))
dot_node_22->dot_node_23
DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_24
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_23->dot_node_24
all_r
dot_node_25
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}
y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_24->dot_node_25
imp_r
dot_node_26
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}
0 < y ∧ y ∈ ELEMENTS
dot_node_25->dot_node_26
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_27
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
0 < y ∧ y ∈ ELEMENTS ∖ elements
0 < y ∧ y ∈ ELEMENTS
dot_node_26->dot_node_27
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_28
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
0 < y
y ∈ ELEMENTS ∖ elements
0 < y ∧ y ∈ ELEMENTS
dot_node_27->dot_node_28
and_l (0 < y ∧ y ∈ ELEMENTS ∖ elements)
dot_node_29
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
0 < y
y ∈ ELEMENTS ∖ elements
0 < y
dot_node_28->dot_node_29
and_r
dot_node_30
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
0 < y
y ∈ ELEMENTS ∖ elements
y ∈ ELEMENTS
dot_node_28->dot_node_30
and_r
dot_node_29->dot_node_2
hyp
dot_node_31
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
0 < y
y ∈ ELEMENTS ∧ ¬(y ∈ elements)
y ∈ ELEMENTS
dot_node_30->dot_node_31
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
dot_node_32
e ≤ 0 ∧ e ∈ elements
(∀y·(y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⇒ y ∈ ELEMENTS))
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
elements ∖ {e} = ∅
¬(elements = ∅)
0 < y
y ∈ ELEMENTS
¬(y ∈ elements)
y ∈ ELEMENTS
dot_node_31->dot_node_32
and_l (y ∈ ELEMENTS ∧ ¬(y ∈ elements))
dot_node_32->dot_node_3
hyp
dot_node_34
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}
dot_node_33->dot_node_34
all_r
dot_node_35
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}
dot_node_34->dot_node_35
imp_r
dot_node_36
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
dot_node_35->dot_node_36
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_37
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
dot_node_36->dot_node_37
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_38
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
dot_node_37->dot_node_38
and_l (0 < y ∧ y ∈ ELEMENTS)
dot_node_39
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
dot_node_38->dot_node_39
and_r
dot_node_40
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
dot_node_38->dot_node_40
and_r
dot_node_39->dot_node_4
hyp
dot_node_41
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
dot_node_40->dot_node_41
SIMP_SETMINUS_EQUAL_EMPTY (elements ∖ {e} = ∅)
dot_node_42
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
dot_node_41->dot_node_42
DEF_SUBSETEQ (elements ⊆ {e})
dot_node_43
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
dot_node_42->dot_node_43
∀ instantiation in hyp 6 for ID x: 'y'
dot_node_44
e ≤ 0 ∧ e ∈ elements
{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
¬(elements = ∅)
0 < y
y ∈ ELEMENTS
¬(y ∈ elements)
y ∈ ELEMENTS ∖ elements
dot_node_43->dot_node_44
imp_case (y ∈ elements ⇒ y ∈ {e})
dot_node_45
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
dot_node_43->dot_node_45
imp_case (y ∈ elements ⇒ y ∈ {e})
dot_node_46
e ≤ 0 ∧ e ∈ elements
{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
¬(elements = ∅)
0 < y
y ∈ ELEMENTS
¬(y ∈ elements)
y ∈ ELEMENTS ∧ ¬(y ∈ elements)
dot_node_44->dot_node_46
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
dot_node_49
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)
dot_node_45->dot_node_49
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
dot_node_47
e ≤ 0 ∧ e ∈ elements
{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
¬(elements = ∅)
0 < y
y ∈ ELEMENTS
¬(y ∈ elements)
y ∈ ELEMENTS
dot_node_46->dot_node_47
and_r
dot_node_48
e ≤ 0 ∧ e ∈ elements
{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
¬(elements = ∅)
0 < y
y ∈ ELEMENTS
¬(y ∈ elements)
¬(y ∈ elements)
dot_node_46->dot_node_48
and_r
dot_node_47->dot_node_5
hyp
dot_node_48->dot_node_6
hyp
dot_node_50
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
dot_node_49->dot_node_50
and_r
dot_node_51
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)
dot_node_49->dot_node_51
and_r
dot_node_50->dot_node_7
hyp
dot_node_52
{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)
dot_node_51->dot_node_52
and_l (e ≤ 0 ∧ e ∈ elements)
dot_node_53
{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)
dot_node_52->dot_node_53
SIMP_IN_SING (y ∈ {e})
dot_node_54
{x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS
elements ⊆ ELEMENTS
ELEMENTS ⊂ ℤ
finite(ELEMENTS)
¬(elements = ∅)
0 < y
y ∈ ELEMENTS
y ≤ 0
y ∈ elements
¬(y ∈ elements)
dot_node_53->dot_node_54
eq (rl,y = e)
dot_node_54->dot_node_8
cntr
Reset View