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_fun_dom
5. true_goal
6. Evaluate tautology (finite(1 ‥ n))
7. true_goal
8. fun_goal
9. DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1)
10. eq (lr,dom(arr) = 1 ‥ n)
11. hyp
12. SIMP_NOTEQUAL (ran(arr) ≠ ∅)
13. DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅))
14. exists_inst(arr(1))
15. and_r
16. DERIV_DOM_TOTALREL (1 ∈ dom(arr))
17. DEF_IN_UPTO (1 ∈ 1 ‥ n)
18. SIMP_LIT_LE (1 ≤ 1)
19. true_goal
20. DEF_IN_NATURAL1 (n ∈ ℕ1)
21. hyp
22. fun_goal
23. DEF_IN_RAN (arr(1) ∈ ran(arr))
24. exists_inst(1)
25. true_goal
26. SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr)
27. true_goal

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