let a be Data-Location ; :: thesis: for loc being Instruction-Location of SCM holds not a =0_goto loc is halting
let loc be Instruction-Location of SCM ; :: thesis: not a =0_goto loc is halting
reconsider V = a =0_goto loc as Element of SCM-Instr ;
reconsider a3 = loc as Element of NAT by AMI_1:def 4;
consider s being SCM-State;
set t = s +* (NAT .--> (succ a3));
set f = the Object-Kind of SCM ;
A1: dom (NAT .--> (succ a3)) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def 1;
then A2: (s +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:14
.= succ a3 by FUNCOP_1:87 ;
A3: {NAT } c= SCM-Memory by AMI_2:30, ZFMISC_1:37;
A4: dom s = dom SCM-OK by CARD_3:18;
A5: dom (s +* (NAT .--> (succ a3))) = (dom s) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def 1
.= SCM-Memory \/ (dom (NAT .--> (succ a3))) by A4, FUNCT_2:def 1
.= SCM-Memory \/ {NAT } by FUNCOP_1:19
.= SCM-Memory by A3, XBOOLE_1:12 ;
A6: dom the Object-Kind of SCM = SCM-Memory by FUNCT_2:def 1;
for x being set st x in dom the Object-Kind of SCM holds
(s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x

proof

let x be set ; :: thesis: ( x in dom the Object-Kind of SCM implies (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x )
assume A7: x in dom the Object-Kind of SCM ; :: thesis: (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x

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

suppose A8: x = NAT ; :: thesis: (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x

then the Object-Kind of SCM . x = NAT by AMI_2:7, AMI_2:30;
hence (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x by A2, A8; :: thesis: verum

end;

suppose x <> NAT ; :: thesis: (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x

then not x in dom (NAT .--> (succ a3)) by A1, TARSKI:def 1;
then (s +* (NAT .--> (succ a3))) . x = s . x by FUNCT_4:12;
hence (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x by A7, CARD_3:18; :: thesis: verum

end;

end;

end;

then reconsider t = s +* (NAT .--> (succ a3)) as State of SCM by A5, A6, CARD_3:18;
reconsider w = t as SCM-State ;
dom (NAT .--> loc) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A9: (w +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:14
.= loc by FUNCOP_1:87 ;
A10: 7 is Element of Segm 9 by GR_CY_1:10;
A11: a is Element of SCM-Data-Loc by Def2;
assume A12: a =0_goto loc is halting ; :: thesis: contradiction

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

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

A14: IC t = IC w by AMI_2:30, FUNCT_7:def 1;
A15: IC w = w . NAT ;
A16: (Exec (a =0_goto loc),t) . (IC SCM ) = w . NAT by A12, Th4, AMI_1:def 8;
reconsider e = w . NAT as Instruction-Location of SCM by A15, AMI_1:def 4;
t . a <> 0 by A10, A11, A13, AMI_2:25;
then A17: (Exec (a =0_goto loc),t) . (IC SCM ) = Next by A14, Th14;
thus contradiction by A16, A17; :: 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 A10, A11, AMI_2:25
.= SCM-Exec-Res V,w by A11, AMI_2:def 16
.= Exec (a =0_goto loc),t by AMI_2:def 17
.= t by A12, AMI_1:def 8 ;
hence contradiction by A2, A9; :: thesis: verum

end;

end;