let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined non empty lower unique-halt FinPartState of
for I being Element of NAT st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for F being NAT -defined non empty lower unique-halt FinPartState of
for I being Element of NAT st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S
let F be NAT -defined non empty lower unique-halt FinPartState of ; :: thesis: for I being Element of NAT st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S
let I be Element of NAT ; :: thesis: ( I in dom (CutLastLoc F) implies (CutLastLoc F) . I <> halt S )
assume that
A1: I in dom (CutLastLoc F) and
A2: (CutLastLoc F) . I = halt S ; :: thesis: contradiction
A3: dom (CutLastLoc F) c= dom F by GRFUNC_1:8;
F . I = halt S by A1, A2, GRFUNC_1:8;
then A4: I = LastLoc F by A1, A3, AMISTD_1:def 23;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by Th47;
then not I in {(LastLoc F)} by A1, XBOOLE_0:def 5;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum