let s1, s2 be All-State of T; :: thesis: ( ex k being Nat st

( s1 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) & ex k being Nat st

( s2 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) implies s1 = s2 )

given k1 being Nat such that A2: ( s1 = (Computation s) . k1 & ((Computation s) . k1) `1_3 = the AcceptS of T ) ; :: thesis: ( for k being Nat holds

( not s2 = (Computation s) . k or not ((Computation s) . k) `1_3 = the AcceptS of T ) or s1 = s2 )

given k2 being Nat such that A3: ( s2 = (Computation s) . k2 & ((Computation s) . k2) `1_3 = the AcceptS of T ) ; :: thesis: s1 = s2

( k1 <= k2 or k2 <= k1 ) ;

hence s1 = s2 by A2, A3, Th12; :: thesis: verum

( s1 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) & ex k being Nat st

( s2 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) implies s1 = s2 )

given k1 being Nat such that A2: ( s1 = (Computation s) . k1 & ((Computation s) . k1) `1_3 = the AcceptS of T ) ; :: thesis: ( for k being Nat holds

( not s2 = (Computation s) . k or not ((Computation s) . k) `1_3 = the AcceptS of T ) or s1 = s2 )

given k2 being Nat such that A3: ( s2 = (Computation s) . k2 & ((Computation s) . k2) `1_3 = the AcceptS of T ) ; :: thesis: s1 = s2

( k1 <= k2 or k2 <= k1 ) ;

hence s1 = s2 by A2, A3, Th12; :: thesis: verum