let s1, s2 be State of S; :: thesis: ( ex k being Element of NAT st
( s1 = Comput (ProgramPart s),s,k & CurInstr (ProgramPart s1),s1 = halt S ) & ex k being Element of NAT st
( s2 = Comput (ProgramPart s),s,k & CurInstr (ProgramPart s2),s2 = halt S ) implies s1 = s2 )
given k1 being Element of NAT such that A2: ( s1 = Comput (ProgramPart s),s,k1 & CurInstr (ProgramPart s1),s1 = halt S ) ; :: thesis: ( for k being Element of NAT holds
( not s2 = Comput (ProgramPart s),s,k or not CurInstr (ProgramPart s2),s2 = halt S ) or s1 = s2 )
given k2 being Element of NAT such that A3: ( s2 = Comput (ProgramPart s),s,k2 & CurInstr (ProgramPart s2),s2 = halt S ) ; :: thesis: s1 = s2
X: ProgramPart s1 = ProgramPart s by A2, LmY;
Y: ProgramPart s2 = ProgramPart s by A3, LmY;
( k1 <= k2 or k2 <= k1 ) ;
hence s1 = s2 by A2, A3, Th52, X, Y; :: thesis: verum