Information
- Trace generated on 25.1.2026 at 7:15
- Trace length: 8
- Specification file (xtl): marsRover/Rover3.pl
- Git revision of file: 100644 304265c7dcc78c5e6277b3afbd9b94800370ddc4 0 Rover3.pl
- Git revision of repository HEAD: 923651a1117ae7c552cc39a63e823a9a2d46ae46
- ProB version: 1.16.0-nightly
- ProB revision: aa3f38aab7276da2a958ce9c0f91fc2d45a08bce (Sat Jan 24 15:10:00 2026 +0100)
1. inv14/WD (true)
(start_xtl_system)
| --------------------- |
| radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) |
2. reselect_hyp (radiation ∈ field → ℕ)
(reselect_hyp(member($(radiation),total_function($(field),'NATURAL'))))
| radiation ∈ field → ℕ |
| --------------------- |
| radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) |
3. reselect_hyp ({rover} ⊆ field)
(reselect_hyp(subset(set_extension([$(rover)]),$(field))))
| radiation ∈ field → ℕ |
| {rover} ⊆ field |
| --------------------- |
| radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) |
4. and_r
| radiation ∈ field → ℕ |
radiation ∈ field → ℕ |
| {rover} ⊆ field |
{rover} ⊆ field |
| --------------------- |
--------------------- |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
rover ∈ dom(radiation) |
5. fun_goal
| radiation ∈ field → ℕ |
| {rover} ⊆ field |
| --------------------- |
| rover ∈ dom(radiation) |
6. DERIV_DOM_TOTALREL (rover ∈ dom(radiation))
(simplify_goal('DERIV_DOM_TOTALREL'))
| radiation ∈ field → ℕ |
| {rover} ⊆ field |
| --------------------- |
| rover ∈ field |
7. SIMP_SUBSETEQ_SING ({rover} ⊆ field)
(simplify_hyp('SIMP_SUBSETEQ_SING',subset(set_extension([$(rover)]),$(field))))
| radiation ∈ field → ℕ |
| rover ∈ field |
| --------------------- |
| rover ∈ field |
8. hyp
| Proof of inv14/WD (true) succeeded. |