let s1, s2 be State of S; :: thesis: ( ex k being Nat st
( s1 = Comput f,s,k & CurInstr f,s1 = halt S ) & ex k being Nat st
( s2 = Comput f,s,k & CurInstr f,s2 = halt S ) implies s1 = s2 )
given k1 being Nat such that A2: s1 = Comput f,s,k1 and
A3: CurInstr f,s1 = halt S ; :: thesis: ( for k being Nat holds
( not s2 = Comput f,s,k or not CurInstr f,s2 = halt S ) or s1 = s2 )
given k2 being Nat such that A4: s2 = Comput f,s,k2 and
A5: CurInstr f,s2 = halt S ; :: thesis: s1 = s2
( k1 <= k2 or k2 <= k1 ) ;
hence s1 = s2 by A2, A3, A4, A5, Th7; :: thesis: verum