let a be Data-Location; :: thesis: for loc being Nat holds not a =0_goto loc is halting
let loc be Nat; :: thesis: not a =0_goto loc is halting
set f = the_Values_of SCM;
set s = the SCM-State;
reconsider V = a =0_goto loc as Element of SCM-Instr ;
reconsider a3 = loc as Nat ;
set t = the SCM-State +* (NAT .--> (a3 + 1));
A1: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31;
A2: dom the SCM-State = the carrier of SCM by AMI_2:28;
A3: 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 A1, XBOOLE_1:12 ;
A4: 7 is Element of Segm 9 by NAT_1:44;
NAT in dom (NAT .--> (a3 + 1)) by TARSKI:def 1;
then A6: ( the SCM-State +* (NAT .--> (a3 + 1))) . NAT = (NAT .--> (a3 + 1)) . NAT by FUNCT_4:13
.= a3 + 1 by FUNCOP_1:72 ;
A7: 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 A8: 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 A9: 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 A6, A9, 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 A8, CARD_3:9; :: thesis: verum

end;

end;

end;

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 A3, A7, 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 ;
assume A11: a =0_goto loc is halting ; :: thesis: contradiction
A12: a is Element of SCM-Data-Loc by AMI_2:def 16;

per cases ( w . (V cond_address) <> 0 or w . (V cond_address) = 0 ) ;

suppose A13: w . (V cond_address) <> 0 ; :: thesis: contradiction

IC w = w . NAT ;
then reconsider e = w . NAT as Nat ;
( IC t = IC w & t . a <> 0 ) by A4, A12, A13, AMI_2:22, SCM_INST:7, SUBSET_1:def 8;
then A14: (Exec ((a =0_goto loc),t)) . (IC ) = e + 1 by Th8;
(Exec ((a =0_goto loc),t)) . (IC ) = w . NAT by A11, Th1;
hence contradiction by A14; :: thesis: verum

end;

suppose w . (V cond_address) = 0 ; :: thesis: contradiction

then IFEQ ((w . (V cond_address)),0,(V cjump_address),((IC w) + 1)) = V cjump_address by FUNCOP_1:def 8;
then w +* (NAT .--> loc) = SCM-Chg (w,(IFEQ ((w . (V cond_address)),0,(V cjump_address),((IC w) + 1)))) by A4, A12, SCM_INST:7
.= SCM-Exec-Res (V,w) by A12, AMI_2:def 14
.= Exec ((a =0_goto loc),t) by AMI_2:def 15
.= t by A11 ;
hence contradiction by A6, A10; :: thesis: verum

end;

end;