let R be Ring; :: thesis: for a being Data-Location of R

for i1 being Nat holds not a =0_goto i1 is halting

let a be Data-Location of R; :: thesis: for i1 being Nat holds not a =0_goto i1 is halting

let i1 be Nat; :: thesis: not a =0_goto i1 is halting

reconsider i5 = i1 as Element of NAT by ORDINAL1:def 12;

set s = the SCM-State of R;

set t = the SCM-State of R +* (NAT .--> (i1 + 1));

set f = the_Values_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 .--> (i1 + 1))) = (dom the SCM-State of R) \/ (dom (NAT .--> (i1 + 1))) by FUNCT_4:def 1

.= SCM-Memory \/ (dom (NAT .--> (i1 + 1))) by SCMRING1:19

.= SCM-Memory \/ {NAT}

.= SCM-Memory by A1, XBOOLE_1:12 ;

A3: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;

NAT in dom (NAT .--> (i1 + 1)) by TARSKI:def 1;

then A5: ( the SCM-State of R +* (NAT .--> (i1 + 1))) . NAT = (NAT .--> (i1 + 1)) . NAT by FUNCT_4:13

.= i5 + 1 by FUNCOP_1:72 ;

A6: dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) = the carrier of (SCM R) by A2, Def1

.= dom (the_Values_of (SCM R)) by PARTFUN1:def 2 ;

A7: for x being object st x in dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) holds

( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x

then reconsider t = the SCM-State of R +* (NAT .--> (i1 + 1)) 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_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;

reconsider w = t as SCM-State of R by A10, CARD_3:107;

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

A15: i1 in NAT by ORDINAL1:def 12;

for i1 being Nat holds not a =0_goto i1 is halting

let a be Data-Location of R; :: thesis: for i1 being Nat holds not a =0_goto i1 is halting

let i1 be Nat; :: thesis: not a =0_goto i1 is halting

reconsider i5 = i1 as Element of NAT by ORDINAL1:def 12;

set s = the SCM-State of R;

set t = the SCM-State of R +* (NAT .--> (i1 + 1));

set f = the_Values_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 .--> (i1 + 1))) = (dom the SCM-State of R) \/ (dom (NAT .--> (i1 + 1))) by FUNCT_4:def 1

.= SCM-Memory \/ (dom (NAT .--> (i1 + 1))) by SCMRING1:19

.= SCM-Memory \/ {NAT}

.= SCM-Memory by A1, XBOOLE_1:12 ;

A3: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;

NAT in dom (NAT .--> (i1 + 1)) by TARSKI:def 1;

then A5: ( the SCM-State of R +* (NAT .--> (i1 + 1))) . NAT = (NAT .--> (i1 + 1)) . NAT by FUNCT_4:13

.= i5 + 1 by FUNCOP_1:72 ;

A6: dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) = the carrier of (SCM R) by A2, Def1

.= dom (the_Values_of (SCM R)) by PARTFUN1:def 2 ;

A7: for x being object st x in dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) holds

( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x

proof

dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) = the carrier of (SCM R)
by A2, Def1;
let x be object ; :: thesis: ( x in dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) implies ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x )

assume A8: x in dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) ; :: thesis: ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x

end;assume A8: x in dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) ; :: thesis: ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x

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

end;

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

then
(the_Values_of (SCM R)) . x = NAT
by A3, SCMRING1:2;

hence ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x by A5, A9, ORDINAL1:def 12; :: thesis: verum

end;hence ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x by A5, A9, ORDINAL1:def 12; :: thesis: verum

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

then
not x in dom (NAT .--> (i1 + 1))
by TARSKI:def 1;

then ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x = the SCM-State of R . x by FUNCT_4:11;

hence ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x by A3, A8, A6, CARD_3:9; :: thesis: verum

end;then ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x = the SCM-State of R . x by FUNCT_4:11;

hence ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x by A3, A8, A6, CARD_3:9; :: thesis: verum

then reconsider t = the SCM-State of R +* (NAT .--> (i1 + 1)) 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_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;

reconsider w = t as SCM-State of R by A10, CARD_3:107;

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

A15: i1 in NAT by ORDINAL1:def 12;

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

end;

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

IC w = w . NAT
;

then reconsider e = w . NAT as Element of NAT ;

A17: IC t = IC w by Def1;

then A18: (Exec ((a =0_goto i1),t)) . (IC ) = w . NAT by A14;

a is Element of Data-Locations by Th1;

then t . a <> 0. R by A12, A16, AMI_3:27, SCMRINGI:3, A15;

then (Exec ((a =0_goto i1),t)) . (IC ) = e + 1 by A17, Th16;

hence contradiction by A18; :: thesis: verum

end;then reconsider e = w . NAT as Element of NAT ;

A17: IC t = IC w by Def1;

then A18: (Exec ((a =0_goto i1),t)) . (IC ) = w . NAT by A14;

a is Element of Data-Locations by Th1;

then t . a <> 0. R by A12, A16, AMI_3:27, SCMRINGI:3, A15;

then (Exec ((a =0_goto i1),t)) . (IC ) = e + 1 by A17, Th16;

hence contradiction by A18; :: thesis: verum

suppose A19:
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, SCMRINGI:3

.= SCM-Chg (w,(IFEQ ((w . (V cond_address)),(0. R),(V cjump_address),((IC w) + 1)))) by A19, FUNCOP_1:def 8

.= SCM-Exec-Res (V,w) by A13, AMI_3:27, SCMRING1:def 14, A15

.= Exec ((a =0_goto i1),t) by Th10

.= t by A14 ;

hence contradiction by A5, A11; :: thesis: verum

end;.= SCM-Chg (w,(V cjump_address)) by A12, A13, AMI_3:27, SCMRINGI:3

.= SCM-Chg (w,(IFEQ ((w . (V cond_address)),(0. R),(V cjump_address),((IC w) + 1)))) by A19, FUNCOP_1:def 8

.= SCM-Exec-Res (V,w) by A13, AMI_3:27, SCMRING1:def 14, A15

.= Exec ((a =0_goto i1),t) by Th10

.= t by A14 ;

hence contradiction by A5, A11; :: thesis: verum