Information

Trace generated on 26.1.2026 at 14:57
Trace length: 27
Specification file (xtl): find_ctx/find_ctx.pl
Git revision of file: 100644 aeb1dc7ff1e00a21f6b0f79d11df91ccc64a31bf 0 find_ctx.pl
Git revision of repository HEAD: cd19d00422d82514eec2f9464304c1349a4c362b
ProB version: 1.16.0-nightly
ProB revision: 25fadf907101913f4f3f41a98fdcdc96920fbb46 (Mon Jan 26 07:56:17 2026 +0100)

1. thm1/WD (true)

(start_xtl_system)

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`(∃b·(∀x·(x ∈ ran(arr) ⇒ x ≤ b))) ∧ arr ∈ ℤ ⇸ ℤ ∧ mxi ∈ dom(arr) ∧ ran(arr) ≠ ∅`

2. and_r

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`	`---------------------`
`(∃b·(∀x·(x ∈ ran(arr) ⇒ x ≤ b)))`	`arr ∈ ℤ ⇸ ℤ`	`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

3. upper_bound_r

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`	`---------------------`
`finite(ran(arr))`	`arr ∈ ℤ ⇸ ℤ`	`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

4. fin_rel_ran_r

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`	`---------------------`
`finite(arr)`	`arr ∈ ℤ ⇸ ℤ`	`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

5. fin_fun_dom

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`	`---------------------`	`---------------------`
`⊤`	`finite(1 ‥ n)`	`arr ∈ ℤ ⇸ ℤ`	`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

6. true_goal

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`	`---------------------`
`finite(1 ‥ n)`	`arr ∈ ℤ ⇸ ℤ`	`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

7. Evaluate tautology (finite(1 ‥ n))

(simplify_goal('Evaluate tautology'))

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`	`---------------------`
`⊤`	`arr ∈ ℤ ⇸ ℤ`	`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

8. true_goal

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`
`arr ∈ ℤ ⇸ ℤ`	`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

9. fun_goal

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`
`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

10. DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1)

(simplify_hyp('DEF_IN_TFCT',member($(arr),total_function(interval(1,$(n)),'NATURAL1'))))

`arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`
`mxi ∈ dom(arr)`	`ran(arr) ≠ ∅`

11. and_l (arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n)

(and_l(conjunct(member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),equal(domain($(arr)),interval(1,$(n))))))

`mxi ∈ 1 ‥ n`	`arr ∈ 1 ‥ n → ℕ1`
`n ∈ ℕ1`	`mxi ∈ 1 ‥ n`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`n ∈ ℕ1`
`arr ∈ 1 ‥ n ⇸ ℕ1`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`dom(arr) = 1 ‥ n`	`---------------------`
`---------------------`	`ran(arr) ≠ ∅`
`mxi ∈ dom(arr)`

12. eq (lr,dom(arr) = 1 ‥ n)

(eq(lr,domain($(arr)),interval(1,$(n))))

`mxi ∈ 1 ‥ n`	`arr ∈ 1 ‥ n → ℕ1`
`n ∈ ℕ1`	`mxi ∈ 1 ‥ n`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`n ∈ ℕ1`
`arr ∈ 1 ‥ n ⇸ ℕ1`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`
`mxi ∈ 1 ‥ n`	`ran(arr) ≠ ∅`

13. hyp

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`ran(arr) ≠ ∅`

14. SIMP_NOTEQUAL (ran(arr) ≠ ∅)

(simplify_goal('SIMP_NOTEQUAL'))

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`¬(ran(arr) = ∅)`

15. DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅))

(simplify_goal('DEF_SPECIAL_NOT_EQUAL'))

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`(∃x·x ∈ ran(arr))`

16. exists_inst('arr(1)')

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`
`1 ∈ dom(arr)`	`arr ∈ ℤ ⇸ ℤ`	`arr(1) ∈ ran(arr)`

17. DERIV_DOM_TOTALREL (1 ∈ dom(arr))

(simplify_goal('DERIV_DOM_TOTALREL'(interval(1,$(n)))))

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`
`1 ∈ 1 ‥ n`	`arr ∈ ℤ ⇸ ℤ`	`arr(1) ∈ ran(arr)`

18. DEF_IN_UPTO (1 ∈ 1 ‥ n)

(simplify_goal('DEF_IN_UPTO'))

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`
`1 ≤ 1 ∧ 1 ≤ n`	`arr ∈ ℤ ⇸ ℤ`	`arr(1) ∈ ran(arr)`

19. SIMP_LIT_LE (1 ≤ 1)

(simplify_goal('SIMP_LIT_LE'))

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`
`⊤ ∧ 1 ≤ n`	`arr ∈ ℤ ⇸ ℤ`	`arr(1) ∈ ran(arr)`

20. SIMP_SPECIAL_AND_BTRUE (⊤ ∧ 1 ≤ n)

(simplify_goal('SIMP_SPECIAL_AND_BTRUE'))

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`
`1 ≤ n`	`arr ∈ ℤ ⇸ ℤ`	`arr(1) ∈ ran(arr)`

21. DEF_IN_NATURAL1 (n ∈ ℕ1)

(simplify_hyp('DEF_IN_NATURAL1',member($(n),'NATURAL1')))

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`1 ≤ n`	`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`	`---------------------`
`1 ≤ n`	`arr ∈ ℤ ⇸ ℤ`	`arr(1) ∈ ran(arr)`

22. hyp

`arr ∈ 1 ‥ n → ℕ1`	`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`	`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`	`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`	`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`	`---------------------`
`arr ∈ ℤ ⇸ ℤ`	`arr(1) ∈ ran(arr)`

23. fun_goal

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`arr(1) ∈ ran(arr)`

24. DEF_IN_RAN (arr(1) ∈ ran(arr))

(simplify_goal('DEF_IN_RAN'))

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`(∃x·x ↦ arr(1) ∈ arr)`

25. exists_inst('1')

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`1 ↦ arr(1) ∈ arr`

26. SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr)

(simplify_goal('SIMP_IN_FUNIMAGE'))

`arr ∈ 1 ‥ n → ℕ1`
`mxi ∈ 1 ‥ n`
`n ∈ ℕ1`
`(∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi)))`
`---------------------`
`⊤`

27. true_goal

`Proof of thm1/WD (true) succeeded.`