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. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ ELEMENTS)
12. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS∣x})
13. all_r
14. imp_r
15. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
16. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
17. hyp
18. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
19. hyp
20. DEF_SUBSETEQ ({x·0 < x ∧ x ∈ ELEMENTS∣x} ⊆ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
21. all_r
22. imp_r
23. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
24. SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
25. hyp
26. SIMP_SETMINUS_EQUAL_EMPTY (elements ∖ {e} = ∅)
27. DEF_SUBSETEQ (elements ⊆ {e})
28. ∀ instantiation in hyp 6 for ID x: 'y'
29. true_goal
30. imp_case (y ∈ elements ⇒ y ∈ {e})
31. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
32. hyp
33. hyp
34. DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
35. hyp
36. and_l (e ≤ 0 ∧ e ∈ elements)
37. SIMP_IN_SING (y ∈ {e})
38. eq (rl,y = e)
39. cntr
ProB Version: 1.16.0-nightly (25fadf907101913f4f3f41a98fdcdc96920fbb46)
Generated on 26/01/2026 at 12:50
Proof Tree
prob_graph
dot_node_0
Select PO
dot_node_10
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_10
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_9
Proven.
dot_node_11
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_10->dot_node_11
reselect_hyp (pos ⊆ ELEMENTS)
dot_node_12
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_11->dot_node_12
reselect_hyp (elements ⊆ ELEMENTS)
dot_node_13
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_12->dot_node_13
reselect_hyp (ELEMENTS ⊂ ℤ)
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}
elements ∖ {e} = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_13->dot_node_14
reselect_hyp (pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
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
reselect_hyp (finite(ELEMENTS))
dot_node_16
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_15->dot_node_16
imp_r
dot_node_17
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_16->dot_node_17
imp_case (elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_18
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_16->dot_node_18
imp_case (elements = ∅ ⇒ pos = {x·0 < x ∧ x ∈ ELEMENTS∣x})
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}
dot_node_17->dot_node_19
eq (lr,pos = {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_18->dot_node_1
hyp
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
DERIV_EQUAL ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} = {x·0 < x ∧ x ∈ ELEMENTS∣x})
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
DERIV_EQUAL ({x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x} = {x·0 < x ∧ x ∈ ELEMENTS∣x})
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_30
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_30
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 = ∅)
0 < y
y ∈ ELEMENTS ∖ elements
y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x}
dot_node_25->dot_node_26
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ 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
dot_node_26->dot_node_27
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ 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
y ∈ ELEMENTS
dot_node_26->dot_node_28
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_27->dot_node_2
hyp
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
¬(y ∈ elements)
y ∈ ELEMENTS
dot_node_28->dot_node_29
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
dot_node_29->dot_node_3
hyp
dot_node_31
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_30->dot_node_31
all_r
dot_node_32
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_31->dot_node_32
imp_r
dot_node_33
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 ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x}
dot_node_32->dot_node_33
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS∣x})
dot_node_34
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_33->dot_node_34
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_35
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_33->dot_node_35
SIMP_IN_COMPSET_ONEPOINT (y ∈ {x·0 < x ∧ x ∈ ELEMENTS ∖ elements∣x})
dot_node_34->dot_node_4
hyp
dot_node_36
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_35->dot_node_36
SIMP_SETMINUS_EQUAL_EMPTY (elements ∖ {e} = ∅)
dot_node_37
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_36->dot_node_37
DEF_SUBSETEQ (elements ⊆ {e})
dot_node_38
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
⊤
dot_node_37->dot_node_38
∀ instantiation in hyp 6 for ID x: 'y'
dot_node_39
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_37->dot_node_39
∀ instantiation in hyp 6 for ID x: 'y'
dot_node_38->dot_node_5
true_goal
dot_node_40
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_39->dot_node_40
imp_case (y ∈ elements ⇒ y ∈ {e})
dot_node_41
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_39->dot_node_41
imp_case (y ∈ elements ⇒ y ∈ {e})
dot_node_42
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_40->dot_node_42
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
dot_node_43
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_40->dot_node_43
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
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 ∈ {e}
y ∈ ELEMENTS
dot_node_41->dot_node_44
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
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)
dot_node_41->dot_node_45
DEF_IN_SETMINUS (y ∈ ELEMENTS ∖ elements)
dot_node_42->dot_node_6
hyp
dot_node_43->dot_node_7
hyp
dot_node_44->dot_node_8
hyp
dot_node_46
{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_45->dot_node_46
and_l (e ≤ 0 ∧ e ∈ elements)
dot_node_47
{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_46->dot_node_47
SIMP_IN_SING (y ∈ {e})
dot_node_48
{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_47->dot_node_48
eq (rl,y = e)
dot_node_48->dot_node_9
cntr
Reset View