let R be good Ring; :: thesis: for i1 being Element of NAT holds not goto i1,R is halting
let i1 be Element of NAT ; :: thesis: not goto i1,R is halting
reconsider i5 = i1 as Element of NAT ;
consider s being SCM-State of R;
set t = s +* (NAT .--> (succ i1));
set f = the Object-Kind of (SCM R);
A1: {NAT } c= SCM-Memory by AMI_2:30, ZFMISC_1:37;
A3: dom (s +* (NAT .--> (succ i1))) = (dom s) \/ (dom (NAT .--> (succ i1))) by FUNCT_4:def 1
.= SCM-Memory \/ (dom (NAT .--> (succ i1))) by PARTFUN1:def 4
.= SCM-Memory \/ {NAT } by FUNCOP_1:19
.= SCM-Memory by A1, XBOOLE_1:12 ;
A5: the Object-Kind of (SCM R) = SCM-OK R by Def1;
A6: dom (NAT .--> (succ i1)) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> (succ i1)) by TARSKI:def 1;
then A7: (s +* (NAT .--> (succ i1))) . NAT = (NAT .--> (succ i1)) . NAT by FUNCT_4:14
.= succ i5 by FUNCOP_1:87 ;
YY: dom (s +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A3, Def1
.= dom the Object-Kind of (SCM R) by PARTFUN1:def 4 ;
XX: for x being set st x in dom (s +* (NAT .--> (succ i1))) holds
(s +* (NAT .--> (succ i1))) . x in the Object-Kind of (SCM R) . x

proof

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

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

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

then the Object-Kind of (SCM R) . x = NAT by A5, AMI_2:30, SCMRING1:2;
hence (s +* (NAT .--> (succ i1))) . x in the Object-Kind of (SCM R) . x by A7, A10; :: thesis: verum

end;

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

then not x in dom (NAT .--> (succ i1)) by A6, TARSKI:def 1;
then (s +* (NAT .--> (succ i1))) . x = s . x by FUNCT_4:12;
hence (s +* (NAT .--> (succ i1))) . x in the Object-Kind of (SCM R) . x by A5, A9, YY, CARD_3:18; :: thesis: verum

end;

end;

end;

Y: the Object-Kind of (SCM R) = SCM-OK R by Def1;
dom (s +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A3, Def1;
then reconsider t = s +* (NAT .--> (succ i1)) as PartState of (SCM R) by XX, FUNCT_1:def 20, RELAT_1:def 18;
dom t = the carrier of (SCM R) by A3, Def1;
then reconsider t = t as State of (SCM R) by PARTFUN1:def 4;
reconsider w = t as SCM-State of R by Y, PBOOLE:155;
dom (NAT .--> i1) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> i1) by TARSKI:def 1;
then A11: (w +* (NAT .--> i1)) . NAT = (NAT .--> i1) . NAT by FUNCT_4:14
.= i1 by FUNCOP_1:87 ;
reconsider V = goto i1,R as Element of SCM-Instr R by Def1;
assume A12: goto i1,R is halting ; :: thesis: contradiction
A13: 6 is Element of Segm 8 by NAT_1:45;
w +* (NAT .--> i1) = SCM-Chg w,i5
.= SCM-Chg w,(V jump_address ) by A13, SCMRING1:18
.= SCM-Exec-Res V,w by SCMRING1:def 14
.= Exec (goto i1,R),t by Th12
.= t by A12, AMI_1:def 8 ;
hence contradiction by A7, A11; :: thesis: verum