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. and_l (arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n)
11. eq (lr,dom(arr) = 1 ‥ n)
12. hyp
13. SIMP_NOTEQUAL (ran(arr) ≠ ∅)
14. DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅))
15. exists_inst(arr(1))
16. DERIV_DOM_TOTALREL (1 ∈ dom(arr))
17. DEF_IN_UPTO (1 ∈ 1 ‥ n)
18. SIMP_LIT_LE (1 ≤ 1)
19. SIMP_SPECIAL_AND_BTRUE (⊤ ∧ 1 ≤ n)
20. DEF_IN_NATURAL1 (n ∈ ℕ1)
21. hyp
22. fun_goal
23. DEF_IN_RAN (arr(1) ∈ ran(arr))
24. exists_inst(1)
25. SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr)
26. 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_18 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_18 DEF_IN_TFCT (arr ∈ 1 ‥ n → ℕ1) dot_node_21 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ¬(ran(arr) = ∅) dot_node_12->dot_node_21 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))) ⊤ dot_node_14->dot_node_15 fin_fun_dom 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_fun_dom dot_node_15->dot_node_1 true_goal 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 Evaluate tautology (finite(1 ‥ n)) dot_node_17->dot_node_2 true_goal dot_node_19 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_18->dot_node_19 and_l (arr ∈ 1 ‥ n ⇸ ℕ1 ∧ dom(arr) = 1 ‥ n) dot_node_20 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ 1 ‥ n ⇸ ℕ1 mxi ∈ 1 ‥ n dot_node_19->dot_node_20 eq (lr,dom(arr) = 1 ‥ n) dot_node_20->dot_node_4 hyp dot_node_22 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) (∃x·x ∈ ran(arr)) dot_node_21->dot_node_22 DEF_SPECIAL_NOT_EQUAL (¬(ran(arr) = ∅)) dot_node_23 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ∈ dom(arr) dot_node_22->dot_node_23 exists_inst(arr(1)) dot_node_24 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) arr ∈ ℤ ⇸ ℤ dot_node_22->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_22->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 ∈ 1 ‥ n dot_node_23->dot_node_26 DERIV_DOM_TOTALREL (1 ∈ dom(arr)) dot_node_24->dot_node_6 fun_goal dot_node_31 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_31 DEF_IN_RAN (arr(1) ∈ ran(arr)) dot_node_27 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ 1 ∧ 1 ≤ n dot_node_26->dot_node_27 DEF_IN_UPTO (1 ∈ 1 ‥ n) dot_node_28 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ ∧ 1 ≤ n dot_node_27->dot_node_28 SIMP_LIT_LE (1 ≤ 1) dot_node_29 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ n dot_node_28->dot_node_29 SIMP_SPECIAL_AND_BTRUE (⊤ ∧ 1 ≤ n) dot_node_30 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n 1 ≤ n (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ≤ n dot_node_29->dot_node_30 DEF_IN_NATURAL1 (n ∈ ℕ1) dot_node_30->dot_node_5 hyp dot_node_32 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) 1 ↦ arr(1) ∈ arr dot_node_31->dot_node_32 exists_inst(1) dot_node_33 arr ∈ 1 ‥ n → ℕ1 mxi ∈ 1 ‥ n n ∈ ℕ1 (∀j·(j ∈ 1 ‥ n ⇒ arr(j) ≤ arr(mxi))) ⊤ dot_node_32->dot_node_33 SIMP_IN_FUNIMAGE (1 ↦ arr(1) ∈ arr) dot_node_33->dot_node_7 true_goal