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

proof

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

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

suppose A9: x = NAT ; :: thesis: (s +* (NAT .--> (Next ))) . x in the Object-Kind of (SCM R) . x

then the Object-Kind of (SCM R) . x = NAT by A1, AMI_2:30, SCMRING1:2;
hence (s +* (NAT .--> (Next ))) . x in the Object-Kind of (SCM R) . x by A3, A9; :: thesis: verum

end;

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

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

end;

end;

end;

then reconsider t = s +* (NAT .--> (Next )) as State of (SCM R) by A6, A7, CARD_3:18;
reconsider w = t as SCM-State of R by Def1;
dom (NAT .--> i1) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> i1) by TARSKI:def 1;
then A10: (w +* (NAT .--> i1)) . NAT = (NAT .--> i1) . NAT by FUNCT_4:14
.= i1 by FUNCOP_1:87 ;
A11: 7 is Element of Segm 8 by GR_CY_1:10;
A12: a is Element of SCM-Data-Loc by Th1;
assume A13: a =0_goto i1 is halting ; :: thesis: contradiction
A14: i1 in NAT by AMI_1:def 4;

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

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

A16: IC t = IC w by Def1;
A17: IC w = w . NAT ;
A18: (Exec (a =0_goto i1),t) . (IC (SCM R)) = w . NAT by A13, A16, AMI_1:def 8;
reconsider e = w . NAT as Instruction-Location of SCM R by A17, AMI_1:def 4;
a is Element of SCM-Data-Loc by Th1;
then t . a <> 0. R by A11, A14, A15, SCMRING1:19;
then A19: (Exec (a =0_goto i1),t) . (IC (SCM R)) = Next by A16, Th18;
thus contradiction by A18, A19; :: thesis: verum

end;

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

w +* (NAT .--> i1) = SCM-Chg w,i5
.= SCM-Chg w,(V cjump_address ) by A11, A12, SCMRING1:19
.= SCM-Chg w,(IFEQ (w . (V cond_address )),(0. R),(V cjump_address ),(succ (IC w))) by A20, FUNCOP_1:def 8
.= SCM-Exec-Res V,w by A12, A14, SCMRING1:def 14
.= Exec (a =0_goto i1),t by Th12
.= t by A13, AMI_1:def 8 ;
hence contradiction by A3, A10; :: thesis: verum

end;

end;