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. true_goal
6. DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1)
7. hyp
8. Evaluate tautology (finite(1 ‥ n))
9. true_goal
10. fun_goal
11. DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1)
12. eq (lr,dom(arr) = 1 ‥ n)
13. hyp
14. SIMP_NOTEQUAL (ran(arr) ≠ ∅)
15. DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅))
16. exists_inst(arr(1))
17. and_r
18. DERIV_DOM_TOTALREL (1 ∈ dom(arr))
19. DEF_IN_UPTO (1 ∈ 1 ‥ n)
20. SIMP_LIT_LE (1 ≤ 1)
21. true_goal
22. DEF_IN_NATURAL1 (n ∈ ℕ1)
23. hyp
24. fun_goal
25. DEF_IN_RAN (arr(1) ∈ ran(arr))
26. exists_inst(1)
27. true_goal
28. SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr)
29. 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_11 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_11 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_8 Proven. dot_node_9 Proven. dot_node_10 Proven. dot_node_12 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_11->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))) arr ∈ ℤ ⇸ ℤ dot_node_11->dot_node_13 and_r dot_node_14 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) mxi ∈ dom(arr) dot_node_11->dot_node_14 and_r dot_node_15 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ran(arr) ≠ ∅ dot_node_11->dot_node_15 and_r dot_node_16 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) finite(ran(arr)) dot_node_12->dot_node_16 upper_bound_r dot_node_13->dot_node_4 fun_goal dot_node_23 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_14->dot_node_23 DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1) dot_node_25 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ¬(ran(arr) = ∅) dot_node_15->dot_node_25 SIMP_NOTEQUAL (ran(arr) ≠ ∅) dot_node_17 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) finite(arr) dot_node_16->dot_node_17 fin_rel_ran_r dot_node_18 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_17->dot_node_18 fin_fun1_r(1..n +-> NATURAL1) dot_node_19 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ 1 ‥ n ⇸ ℕ1 dot_node_17->dot_node_19 fin_fun1_r(1..n +-> NATURAL1) dot_node_20 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) finite(1 ‥ n) dot_node_17->dot_node_20 fin_fun1_r(1..n +-> NATURAL1) dot_node_18->dot_node_1 true_goal dot_node_21 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_19->dot_node_21 DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1) dot_node_22 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_20->dot_node_22 Evaluate tautology (finite(1 ‥ n)) dot_node_21->dot_node_2 hyp dot_node_22->dot_node_3 true_goal dot_node_24 arr ∈ 1 ‥ n ⇸ ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) mxi ∈ 1 ‥ n dot_node_23->dot_node_24 eq (lr,dom(arr) = 1 ‥ n) dot_node_24->dot_node_5 hyp dot_node_26 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) (∃x·x ∈ ran(arr)) dot_node_25->dot_node_26 DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅)) dot_node_27 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ∈ dom(arr) ∧ arr ∈ ℤ ⇸ ℤ dot_node_26->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))) arr(1) ∈ ran(arr) dot_node_26->dot_node_28 exists_inst(arr(1)) dot_node_29 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ∈ dom(arr) dot_node_27->dot_node_29 and_r dot_node_30 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ ℤ ⇸ ℤ dot_node_27->dot_node_30 and_r dot_node_36 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) (∃x·x ↦ arr(1) ∈ arr) dot_node_28->dot_node_36 DEF_IN_RAN (arr(1) ∈ ran(arr)) dot_node_31 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ∈ 1 ‥ n dot_node_29->dot_node_31 DERIV_DOM_TOTALREL (1 ∈ dom(arr)) dot_node_30->dot_node_8 fun_goal dot_node_32 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ 1 dot_node_31->dot_node_32 DEF_IN_UPTO (1 ∈ 1 ‥ n) dot_node_33 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ n dot_node_31->dot_node_33 DEF_IN_UPTO (1 ∈ 1 ‥ n) dot_node_34 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_32->dot_node_34 SIMP_LIT_LE (1 ≤ 1) dot_node_35 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n 1 ≤ n (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ n dot_node_33->dot_node_35 DEF_IN_NATURAL1 (n ∈ ℕ1) dot_node_34->dot_node_6 true_goal dot_node_35->dot_node_7 hyp dot_node_37 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_36->dot_node_37 exists_inst(1) dot_node_38 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ↦ arr(1) ∈ arr dot_node_36->dot_node_38 exists_inst(1) dot_node_37->dot_node_9 true_goal dot_node_39 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_38->dot_node_39 SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr) dot_node_39->dot_node_10 true_goal