Lemma 43 ([Access]). Under A:s , m:M(A) , y:L(A) and the proof input d_m: D(m) , there is a proof of Access(Bundle(m,y);o,x.Ψ) ↔Ψ(m,Round(y)). The definitions of Bundle and Access themselves do not use d_m .

Throughout this proof w abbreviates the exact data expression Bundle(m,y) ; it is not a fresh datum with an assumed property. For any f:F(A) , cancellation of the bundle gives a proof of ⟨w,f⟩_ Single ↔ if( ⟨f,dummy⟩_F; ⟨f,m⟩_F, ⟨f,point(y)⟩_F). First apply cancellation to f_e(w) at dummy:M(A) . It gives ⟨f_e(w),dummy⟩_F ↔ if(D(dummy);, ⟨w,f_i(dummy)⟩_ Single ). Together with D(dummy) from Lemma 42 ([Dummy and point laws]) and the proof of , this gives, by pl , a proof of ⟨f_e(w),dummy⟩_F . Cancellation at the exact input m gives ⟨f_e(w),m⟩_F ↔ if(D(m);, ⟨w,f_i(m)⟩_ Single ). Use d_m and pl to obtain ⟨f_e(w),m⟩_F ↔⟨w,f_i(m)⟩_ Single . Now use with f=f_e(w) . Its condition has the positive proof just constructed, so pl selects its first branch and gives Access(w;o,x.Ψ) ↔⟨w,f_i(m)⟩_ Single . This is where the first occurrence of the callback parameter is fixed: it is the original m by the exact substitution in cancellation. For the second selection, cancellation of f_i(m) at dummy gives ⟨f_i(m),dummy⟩_F ↔ if(D(dummy);, qry_ pt (dummy,pred(x.Ψ(m,x)))). The proof of D(dummy) therefore gives a proof of ⟨f_i(m),dummy⟩_F by pl . Cancellation of f_i(m) at point(y) , followed by D(point(y)) , gives ⟨f_i(m),point(y)⟩_F ↔ qry_ pt (point(y),pred(x.Ψ(m,x))). The point-query proof, at the exact predicate pred(x.Ψ(m,x)) , compares this right side with pred(x.Ψ(m,x))@y . In turn, compares that formula with Ψ(m,Round(y)) . Combining these proofs gives ⟨f_i(m),point(y)⟩_F ↔Ψ(m,Round(y)). Use once more, now with f=f_i(m) . Its condition has the negative proof above, so pl selects its second branch and yields ⟨w,f_i(m)⟩_ Single ↔Ψ(m,Round(y)). Finally combine this with by pl . Only predicate evaluation rounded an argument, and that argument was y . Every occurrence of m in this derivation comes from exact data substitution, without a logical replacement of data.