reconsider a = {} as FinPartState of S by FUNCT_1:174, RELAT_1:206;
take a ; :: thesis: for s1, s2 being State of S st a c= s1 & a c= s2 holds
for q being NAT -defined the Instructions of S -valued finite Function st p c= q holds
for i being Nat holds (Comput p,s1,i) | (dom a) = (Comput q,s2,i) | (dom a)
let s1, s2 be State of S; :: thesis: ( a c= s1 & a c= s2 implies for q being NAT -defined the Instructions of S -valued finite Function st p c= q holds
for i being Nat holds (Comput p,s1,i) | (dom a) = (Comput q,s2,i) | (dom a) )
assume that
a c= s1 and
a c= s2 ; :: thesis: for q being NAT -defined the Instructions of S -valued finite Function st p c= q holds
for i being Nat holds (Comput p,s1,i) | (dom a) = (Comput q,s2,i) | (dom a)
let q be NAT -defined the Instructions of S -valued finite Function; :: thesis: ( p c= q implies for i being Nat holds (Comput p,s1,i) | (dom a) = (Comput q,s2,i) | (dom a) )
assume p c= q ; :: thesis: for i being Nat holds (Comput p,s1,i) | (dom a) = (Comput q,s2,i) | (dom a)
let i be Nat; :: thesis: (Comput p,s1,i) | (dom a) = (Comput q,s2,i) | (dom a)
thus (Comput p,s1,i) | (dom a) = {}
.= (Comput q,s2,i) | (dom a) ; :: thesis: verum