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 Element of NAT by ORDINAL1:def 12;
set t = the SCM-State +* (NAT .--> (succ a3));
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 .--> (succ a3))) = (dom the SCM-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def 1
.= SCM-Memory \/ (dom (NAT .--> (succ a3))) by A2
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= SCM-Memory by A1, XBOOLE_1:12 ;
A4: 7 is Element of Segm 9 by NAT_1:44;
A5: dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def 1;
then A6: ( the SCM-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A7: for x being set st x in dom (the_Values_of SCM) holds
( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x

proof

let x be set ; :: thesis: ( x in dom (the_Values_of SCM) implies ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x )
assume A8: x in dom (the_Values_of SCM) ; :: thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x

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

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

then (the_Values_of SCM) . x = NAT by AMI_2:6;
hence ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x by A6, A9; :: thesis: verum

end;

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

then not x in dom (NAT .--> (succ a3)) by A5, TARSKI:def 1;
then ( the SCM-State +* (NAT .--> (succ a3))) . x = the SCM-State . x by FUNCT_4:11;
hence ( the SCM-State +* (NAT .--> (succ a3))) . 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 .--> (succ a3)) 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;
dom (NAT .--> loc) = {NAT} by FUNCOP_1:13;
then 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 Element of NAT ;
( IC t = IC w & t . a <> 0 ) by A4, A12, A13, AMI_2:22, FUNCT_7:def 1, SCM_INST:7;
then A14: (Exec ((a =0_goto loc),t)) . (IC ) = succ e by Th8;
(Exec ((a =0_goto loc),t)) . (IC ) = w . NAT by A11, Th1, EXTPRO_1:def 3;
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),(succ (IC w))) = V cjump_address by FUNCOP_1:def 8;
then w +* (NAT .--> loc) = SCM-Chg (w,(IFEQ ((w . (V cond_address)),0,(V cjump_address),(succ (IC w))))) 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, EXTPRO_1:def 3 ;
hence contradiction by A6, A10; :: thesis: verum

end;

end;