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 ;
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 \/
.= SCM-Memory by ;
A3: the_Values_of (SCM 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
.= 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
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
per cases ( x = NAT or x <> NAT ) ;
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 ;
hence ( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x by ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
end;
end;
dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) = the carrier of (SCM R) by ;
then reconsider t = the SCM-State of R +* (NAT .--> (i1 + 1)) as PartState of (SCM R) by ;
dom t = the carrier of (SCM R) by ;
then reconsider t = t as State of (SCM R) by PARTFUN1:def 2;
A10: the_Values_of (SCM R) = () * SCM-OK by Lm1;
reconsider w = t as SCM-State of R by ;
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 . () <> 0. R or w . () = 0. R ) ;
suppose A16: w . () <> 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)) . () = w . NAT by A14;
a is Element of Data-Locations by Th1;
then t . a <> 0. R by ;
then (Exec ((a =0_goto i1),t)) . () = e + 1 by ;
hence contradiction by A18; :: thesis: verum
end;
suppose A19: w . () = 0. R ; :: thesis: contradiction
w +* (NAT .--> i1) = SCM-Chg (w,i5)
.= SCM-Chg (w,()) by
.= SCM-Chg (w,(IFEQ ((w . ()),(0. R),(),((IC w) + 1)))) by
.= SCM-Exec-Res (V,w) by
.= Exec ((a =0_goto i1),t) by Th10
.= t by A14 ;
hence contradiction by A5, A11; :: thesis: verum
end;
end;