Information
- Trace generated on 25.1.2026 at 7:15
- Trace length: 11
- 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. 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. and_l (radiation ∈ field ⇸ ℕ ∧ dom(radiation) = field)
(and_l(conjunct(member($(radiation),partial_function($(field),'NATURAL')),equal(domain($(radiation)),$(field)))))
| {rover} ⊆ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| radiation ∈ field ⇸ ℕ |
| dom(radiation) = field |
| --------------------- |
| rover ∈ dom(radiation) |
9. eq (lr,dom(radiation) = field)
(eq(lr,domain($(radiation)),$(field)))
| {rover} ⊆ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| radiation ∈ field ⇸ ℕ |
| --------------------- |
| rover ∈ field |
10. SIMP_SUBSETEQ_SING ({rover} ⊆ field)
(simplify_hyp('SIMP_SUBSETEQ_SING',subset(set_extension([$(rover)]),$(field))))
| rover ∈ field |
| radiation ∈ ℤ × ℤ ⇸ ℤ |
| radiation ∈ field ⇸ ℕ |
| --------------------- |
| rover ∈ field |
11. hyp
| Proof of inv14/WD (true) succeeded. |