let loc be Nat; :: thesis: not SCM-goto loc is halting
set f = the_Values_of SCM;
set s = the SCM-State;
assume A1: SCM-goto loc is halting ; :: thesis: contradiction
reconsider a3 = loc as Nat ;
reconsider V = SCM-goto loc as Element of SCM-Instr ;
set t = the SCM-State +* (NAT .--> (a3 + 1));
A2: dom the SCM-State = the carrier of SCM by AMI_2:28;
NAT in dom (NAT .--> (a3 + 1)) by TARSKI:def 1;
then A4: ( the SCM-State +* (NAT .--> (a3 + 1))) . NAT = (NAT .--> (a3 + 1)) . NAT by FUNCT_4:13
.= a3 + 1 by FUNCOP_1:72 ;
A5: for x being object st x in dom (the_Values_of SCM) holds
( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x

proof

let x be object ; :: thesis: ( x in dom (the_Values_of SCM) implies ( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x )
assume A6: x in dom (the_Values_of SCM) ; :: thesis: ( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x

per cases ( x = NAT or x <> NAT ) ;

suppose A7: x = NAT ; :: thesis: ( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x

then (the_Values_of SCM) . x = NAT by AMI_2:6;
hence ( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x by A4, A7, ORDINAL1:def 12; :: thesis: verum

end;

suppose x <> NAT ; :: thesis: ( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x

then not x in dom (NAT .--> (a3 + 1)) by TARSKI:def 1;
then ( the SCM-State +* (NAT .--> (a3 + 1))) . x = the SCM-State . x by FUNCT_4:11;
hence ( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x by A6, CARD_3:9; :: thesis: verum

end;

end;

end;

A8: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31;
A9: dom ( the SCM-State +* (NAT .--> (a3 + 1))) = (dom the SCM-State) \/ (dom (NAT .--> (a3 + 1))) by FUNCT_4:def 1
.= SCM-Memory \/ (dom (NAT .--> (a3 + 1))) by A2
.= SCM-Memory \/ {NAT}
.= SCM-Memory by A8, XBOOLE_1:12 ;
dom (the_Values_of SCM) = SCM-Memory by AMI_2:27;
then reconsider t = the SCM-State +* (NAT .--> (a3 + 1)) as State of SCM by A9, A5, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
reconsider w = t as SCM-State by CARD_3:107;
NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A10: (w +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:13
.= loc by FUNCOP_1:72 ;
6 is Element of Segm 9 by NAT_1:44;
then w +* (NAT .--> loc) = SCM-Chg (w,(V jump_address)) by SCM_INST:6
.= SCM-Exec-Res (V,w) by AMI_2:def 14
.= Exec ((SCM-goto loc),t) by AMI_2:def 15
.= t by A1 ;
hence contradiction by A4, A10; :: thesis: verum