let R be good Ring; :: thesis: for a being Data-Location of R
for i1 being Element of NAT holds not a =0_goto i1 is halting
let a be Data-Location of R; :: thesis: for i1 being Element of NAT holds not a =0_goto i1 is halting
let i1 be Element of NAT ; :: thesis: not a =0_goto i1 is halting
reconsider i5 = i1 as Element of NAT ;
set s = the SCM-State of R;
set t = the SCM-State of R +* (NAT .--> (succ i1));
set f = the Object-Kind of (SCM R);
reconsider V = a =0_goto i1 as Element of SCM-Instr R by Def1;
A1: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31;
A2: dom ( the SCM-State of R +* (NAT .--> (succ i1))) = (dom the SCM-State of R) \/ (dom (NAT .--> (succ i1))) by FUNCT_4:def 1
.= SCM-Memory \/ (dom (NAT .--> (succ i1))) by PARTFUN1:def 2
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= SCM-Memory by A1, XBOOLE_1:12 ;
A3: the Object-Kind of (SCM R) = SCM-OK R by Def1;
A4: dom (NAT .--> (succ i1)) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> (succ i1)) by TARSKI:def 1;
then A5: ( the SCM-State of R +* (NAT .--> (succ i1))) . NAT = (NAT .--> (succ i1)) . NAT by FUNCT_4:13
.= succ i5 by FUNCOP_1:72 ;
A6: dom ( the SCM-State of R +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A2, Def1
.= dom the Object-Kind of (SCM R) by PARTFUN1:def 2 ;
A7: for x being set st x in dom ( the SCM-State of R +* (NAT .--> (succ i1))) holds
( the SCM-State of R +* (NAT .--> (succ i1))) . x in the Object-Kind of (SCM R) . x

proof

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

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

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

then the Object-Kind of (SCM R) . x = NAT by A3, AMI_2:22, SCMRING1:2;
hence ( the SCM-State of R +* (NAT .--> (succ i1))) . x in the Object-Kind of (SCM R) . x by A5, A9; :: thesis: verum

end;

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

then not x in dom (NAT .--> (succ i1)) by A4, TARSKI:def 1;
then ( the SCM-State of R +* (NAT .--> (succ i1))) . x = the SCM-State of R . x by FUNCT_4:11;
hence ( the SCM-State of R +* (NAT .--> (succ i1))) . x in the Object-Kind of (SCM R) . x by A3, A8, A6, CARD_3:9; :: thesis: verum

end;

end;

end;

dom ( the SCM-State of R +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A2, Def1;
then reconsider t = the SCM-State of R +* (NAT .--> (succ i1)) as PartState of (SCM R) by A7, FUNCT_1:def 14, RELAT_1:def 18;
dom t = the carrier of (SCM R) by A2, Def1;
then reconsider t = t as State of (SCM R) by PARTFUN1:def 2;
A10: the Object-Kind of (SCM R) = SCM-OK R by Def1;
reconsider w = t as SCM-State of R by A10, CARD_3:107;
dom (NAT .--> i1) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> i1) by TARSKI:def 1;
then A11: (w +* (NAT .--> i1)) . NAT = (NAT .--> i1) . NAT by FUNCT_4:13
.= i1 by FUNCOP_1:72 ;
A12: 7 is Element of Segm 8 by NAT_1:44;
A13: a is Element of Data-Locations by Th1;
assume A14: a =0_goto i1 is halting ; :: thesis: contradiction

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

IC w = w . NAT ;
then reconsider e = w . NAT as Element of NAT ;
A16: IC t = IC w by Def1;
then A17: (Exec ((a =0_goto i1),t)) . (IC ) = w . NAT by A14, EXTPRO_1:def 3;
a is Element of Data-Locations by Th1;
then t . a <> 0. R by A12, A15, AMI_3:27, SCMRING1:15;
then (Exec ((a =0_goto i1),t)) . (IC ) = succ e by A16, Th18;
hence contradiction by A17; :: thesis: verum

end;

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

w +* (NAT .--> i1) = SCM-Chg (w,i5)
.= SCM-Chg (w,(V cjump_address)) by A12, A13, AMI_3:27, SCMRING1:15
.= SCM-Chg (w,(IFEQ ((w . (V cond_address)),(0. R),(V cjump_address),(succ (IC w))))) by A18, FUNCOP_1:def 8
.= SCM-Exec-Res (V,w) by A13, AMI_3:27, SCMRING1:def 14
.= Exec ((a =0_goto i1),t) by Th12
.= t by A14, EXTPRO_1:def 3 ;
hence contradiction by A5, A11; :: thesis: verum

end;

end;