Proof Trace Export for inv14/WD (true) from 
marsRover/Rover3.pl
Proof Steps
1. reselect_hyp (radiation ∈ field → ℕ)
2. reselect_hyp ({rover} ⊆ field)
3. reselect_hyp (radiation ∈ ℤ × ℤ ⇸ ℤ)
4. and_r
5. hyp
6. DEF_IN_TFCT (radiation ∈ field → ℕ)
7. and_l (radiation ∈ field ⇸ ℕ ∧ dom(radiation) = field)
8. eq (lr,dom(radiation) = field)
9. SIMP_SUBSETEQ_SING ({rover} ⊆ field)
10. 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 ∈ ℤ × ℤ ⇸ ℤ radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) dot_node_5->dot_node_6 reselect_hyp (radiation ∈ ℤ × ℤ ⇸ ℤ) dot_node_7 radiation ∈ field → ℕ {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ radiation ∈ ℤ × ℤ ⇸ ℤ dot_node_6->dot_node_7 and_r dot_node_8 radiation ∈ field → ℕ {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ rover ∈ dom(radiation) dot_node_6->dot_node_8 and_r dot_node_7->dot_node_1 hyp dot_node_9 radiation ∈ field ⇸ ℕ ∧ dom(radiation) = field {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ rover ∈ dom(radiation) dot_node_8->dot_node_9 DEF_IN_TFCT (radiation ∈ field → ℕ) dot_node_10 {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ radiation ∈ field ⇸ ℕ dom(radiation) = field rover ∈ dom(radiation) dot_node_9->dot_node_10 and_l (radiation ∈ field ⇸ ℕ ∧ dom(radiation) = field) dot_node_11 {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ radiation ∈ field ⇸ ℕ rover ∈ field dot_node_10->dot_node_11 eq (lr,dom(radiation) = field) dot_node_12 rover ∈ field radiation ∈ ℤ × ℤ ⇸ ℤ radiation ∈ field ⇸ ℕ rover ∈ field dot_node_11->dot_node_12 SIMP_SUBSETEQ_SING ({rover} ⊆ field) dot_node_12->dot_node_2 hyp