let S be COM-Struct ; :: thesis: for F being unique-halt Program of S
for I being Nat st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S
let F be unique-halt Program of S; :: thesis: for I being Nat st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S
let I be 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:2;
F . I = halt S by A1, A2, GRFUNC_1:2;
then A4: I = LastLoc F by A1, A3, Def7;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by VALUED_1:36;
then not I in {(LastLoc F)} by A1, XBOOLE_0:def 5;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum