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. eq (lr,dom(radiation) = field)
8. SIMP_SUBSETEQ_SING ({rover} ⊆ field)
9. hyp

ProB Version: 1.16.0-nightly (25fadf907101913f4f3f41a98fdcdc96920fbb46)
Generated on 26/01/2026 at 14:06
 
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 radiation ∈ field ⇸ ℕ {rover} ⊆ field radiation ∈ ℤ × ℤ ⇸ ℤ rover ∈ field dot_node_9->dot_node_10 eq (lr,dom(radiation) = field) dot_node_11 radiation ∈ field ⇸ ℕ rover ∈ field radiation ∈ ℤ × ℤ ⇸ ℤ rover ∈ field dot_node_10->dot_node_11 SIMP_SUBSETEQ_SING ({rover} ⊆ field) dot_node_11->dot_node_2 hyp