Proof Trace Export for thm1/WD (true) from 
find_ctx/find_ctx.pl
Proof Steps
1. and_r
2. upper_bound_r
3. fin_rel_ran_r
4. fin_fun1_r(1..n +-> NATURAL1)
5. DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1)
6. and_l (arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n)
7. hyp
8. Evaluate tautology (finite(1 ‥ n))
9. true_goal
10. fun_goal
11. DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1)
12. and_l (arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n)
13. eq (lr,dom(arr) = 1 ‥ n)
14. hyp
15. SIMP_NOTEQUAL (ran(arr) ≠ ∅)
16. DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅))
17. exists_inst(arr(1))
18. DERIV_DOM_TOTALREL (1 ∈ dom(arr))
19. DEF_IN_UPTO (1 ∈ 1 ‥ n)
20. SIMP_LIT_LE (1 ≤ 1)
21. SIMP_SPECIAL_AND_BTRUE (⊤ ∧ 1 ≤ n)
22. DEF_IN_NATURAL1 (n ∈ ℕ1)
23. hyp
24. fun_goal
25. DEF_IN_RAN (arr(1) ∈ ran(arr))
26. exists_inst(1)
27. SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr)
28. true_goal

ProB Version: 1.16.0-nightly (1742b9cc6629604302028955e627f3b757167b11)
Generated on 26/01/2026 at 15:03
 
Proof Tree
prob_graph dot_node_0 Select PO dot_node_8 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) ≠ ∅ dot_node_0->dot_node_8 thm1/WD (true) dot_node_1 Proven. dot_node_2 Proven. dot_node_3 Proven. dot_node_4 Proven. dot_node_5 Proven. dot_node_6 Proven. dot_node_7 Proven. dot_node_9 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) (∃b·(∀x·(x ∈ ran(arr) ⇒ x ≤ b))) dot_node_8->dot_node_9 and_r dot_node_10 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ ℤ ⇸ ℤ dot_node_8->dot_node_10 and_r dot_node_11 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) mxi ∈ dom(arr) dot_node_8->dot_node_11 and_r dot_node_12 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ran(arr) ≠ ∅ dot_node_8->dot_node_12 and_r dot_node_13 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) finite(ran(arr)) dot_node_9->dot_node_13 upper_bound_r dot_node_10->dot_node_3 fun_goal dot_node_20 arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) mxi ∈ dom(arr) dot_node_11->dot_node_20 DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1) dot_node_23 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ¬(ran(arr) = ∅) dot_node_12->dot_node_23 SIMP_NOTEQUAL (ran(arr) ≠ ∅) dot_node_14 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) finite(arr) dot_node_13->dot_node_14 fin_rel_ran_r dot_node_15 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ 1 ‥ n ⇸ ℕ1 dot_node_14->dot_node_15 fin_fun1_r(1..n +-> NATURAL1) dot_node_16 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) finite(1 ‥ n) dot_node_14->dot_node_16 fin_fun1_r(1..n +-> NATURAL1) dot_node_17 arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ 1 ‥ n ⇸ ℕ1 dot_node_15->dot_node_17 DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1) dot_node_19 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_16->dot_node_19 Evaluate tautology (finite(1 ‥ n)) dot_node_18 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ 1 ‥ n ⇸ ℕ1 dom(arr) = 1 ‥ n arr ∈ 1 ‥ n ⇸ ℕ1 dot_node_17->dot_node_18 and_l (arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n) dot_node_18->dot_node_1 hyp dot_node_19->dot_node_2 true_goal dot_node_21 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ 1 ‥ n ⇸ ℕ1 dom(arr) = 1 ‥ n mxi ∈ dom(arr) dot_node_20->dot_node_21 and_l (arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n) dot_node_22 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ 1 ‥ n ⇸ ℕ1 mxi ∈ 1 ‥ n dot_node_21->dot_node_22 eq (lr,dom(arr) = 1 ‥ n) dot_node_22->dot_node_4 hyp dot_node_24 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) (∃x·x ∈ ran(arr)) dot_node_23->dot_node_24 DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅)) dot_node_25 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ∈ dom(arr) dot_node_24->dot_node_25 exists_inst(arr(1)) dot_node_26 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ ℤ ⇸ ℤ dot_node_24->dot_node_26 exists_inst(arr(1)) dot_node_27 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr(1) ∈ ran(arr) dot_node_24->dot_node_27 exists_inst(arr(1)) dot_node_28 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ∈ 1 ‥ n dot_node_25->dot_node_28 DERIV_DOM_TOTALREL (1 ∈ dom(arr)) dot_node_26->dot_node_6 fun_goal dot_node_33 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) (∃x·x ↦ arr(1) ∈ arr) dot_node_27->dot_node_33 DEF_IN_RAN (arr(1) ∈ ran(arr)) dot_node_29 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ 1 ∧ 1 ≤ n dot_node_28->dot_node_29 DEF_IN_UPTO (1 ∈ 1 ‥ n) dot_node_30 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ ∧ 1 ≤ n dot_node_29->dot_node_30 SIMP_LIT_LE (1 ≤ 1) dot_node_31 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ n dot_node_30->dot_node_31 SIMP_SPECIAL_AND_BTRUE (⊤ ∧ 1 ≤ n) dot_node_32 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n 1 ≤ n (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ n dot_node_31->dot_node_32 DEF_IN_NATURAL1 (n ∈ ℕ1) dot_node_32->dot_node_5 hyp dot_node_34 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ↦ arr(1) ∈ arr dot_node_33->dot_node_34 exists_inst(1) dot_node_35 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_34->dot_node_35 SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr) dot_node_35->dot_node_7 true_goal