Information
- Trace generated on 26.1.2026 at 14:06
- Trace length: 10
- Specification file (xtl): marsRover/Rover3.pl
- Git revision of file: 100644 304265c7dcc78c5e6277b3afbd9b94800370ddc4 0 Rover3.pl
- Git revision of repository HEAD: 7dd4db78da0a1149f00f426a1b6c40daeca5bac7
- ProB version: 1.16.0-nightly
- ProB revision: 25fadf907101913f4f3f41a98fdcdc96920fbb46 (Mon Jan 26 07:56:17 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. reselect_hyp (radiation ∈ ℤ × ℤ ⇸ ℤ)
(reselect_hyp(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))))
| radiation ∈ field → ℕ |
| {rover} ⊆ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| --------------------- |
| radiation ∈ ℤ × ℤ ⇸ ℤ ∧ rover ∈ dom(radiation) |
5. and_r
| radiation ∈ field → ℕ |
radiation ∈ field → ℕ |
| {rover} ⊆ field |
{rover} ⊆ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
radiation ∈ ℤ × ℤ ⇸ ℤ |
| --------------------- |
--------------------- |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
rover ∈ dom(radiation) |
6. hyp
| radiation ∈ field → ℕ |
| {rover} ⊆ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| --------------------- |
| rover ∈ dom(radiation) |
7. DEF_IN_TFCT (radiation ∈ field → ℕ)
(simplify_hyp('DEF_IN_TFCT',member($(radiation),total_function($(field),'NATURAL'))))
| radiation ∈ field ⇸ ℕ |
| dom(radiation) = field |
| {rover} ⊆ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| --------------------- |
| rover ∈ dom(radiation) |
8. eq (lr,dom(radiation) = field)
(eq(lr,domain($(radiation)),$(field)))
| radiation ∈ field ⇸ ℕ |
| {rover} ⊆ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| --------------------- |
| rover ∈ field |
9. SIMP_SUBSETEQ_SING ({rover} ⊆ field)
(simplify_hyp('SIMP_SUBSETEQ_SING',subset(set_extension([$(rover)]),$(field))))
| radiation ∈ field ⇸ ℕ |
| rover ∈ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| --------------------- |
| rover ∈ field |
10. hyp
| Proof of inv14/WD (true) succeeded. |