Proof Trace Export for inv14/WD (true) from 
marsRover/Rover3.pl
Proof Steps
1. reselect_hyp (radiation ∈ field → ℕ)
2. reselect_hyp ({rover} ⊆ field)
3. and_r
4. fun_goal
5. DERIV_DOM_TOTALREL (rover ∈ dom(radiation))
6. SIMP_SUBSETEQ_SING ({rover} ⊆ field)
7. hyp

ProB Version: 1.16.0-nightly (fc7197358de5296cb229afa2bb1fd93b8e64c2ca)
Generated on 25/01/2026 at 7:13
 
Proof Tree
prob_graph dot_node_0 Select PO dot_node_3 no hypotheses radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) dot_node_0->dot_node_3 inv14/WD (true) dot_node_1 Proven. dot_node_2 Proven. dot_node_4 radiation ∈ field → ℕ radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) dot_node_3->dot_node_4 reselect_hyp (radiation ∈ field → ℕ) dot_node_5 radiation ∈ field → ℕ {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) dot_node_4->dot_node_5 reselect_hyp ({rover} ⊆ field) dot_node_6 radiation ∈ field → ℕ {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ dot_node_5->dot_node_6 and_r dot_node_7 radiation ∈ field → ℕ {rover} ⊆ field rover ∈ dom(radiation) dot_node_5->dot_node_7 and_r dot_node_6->dot_node_1 fun_goal dot_node_8 radiation ∈ field → ℕ {rover} ⊆ field rover ∈ field dot_node_7->dot_node_8 DERIV_DOM_TOTALREL (rover ∈ dom(radiation)) dot_node_9 radiation ∈ field → ℕ rover ∈ field rover ∈ field dot_node_8->dot_node_9 SIMP_SUBSETEQ_SING ({rover} ⊆ field) dot_node_9->dot_node_2 hyp