let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for F being non empty NAT -defined initial 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 IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for F being non empty NAT -defined initial 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 non empty NAT -defined initial 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, Def26;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by VALUED_1:37;
then not I in {(LastLoc F)} by A1, XBOOLE_0:def 5;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum