reconsider a3 = la as Nat ;
set t = the SCM+FSA-State +* (NAT .--> (a3 + 1));
A11: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5, ZFMISC_1:31;
A12: dom ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) = (dom the SCM+FSA-State) \/ (dom (NAT .--> (a3 + 1))) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ (dom (NAT .--> (a3 + 1))) by SCMFSA_1:33
.= SCM+FSA-Memory \/ {NAT}
.= SCM+FSA-Memory by A11, XBOOLE_1:12 ;
assume A13: a >0_goto la is halting ; :: thesis: contradiction
NAT in dom (NAT .--> (a3 + 1)) by TARSKI:def 1;
then A14: ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . NAT = (NAT .--> (a3 + 1)) . NAT by FUNCT_4:13
.= a3 + 1 by FUNCOP_1:72 ;
A15: for x being object st x in dom (the_Values_of SCM+FSA) holds
( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM+FSA) . x

proof

let x be object ; :: thesis: ( x in dom (the_Values_of SCM+FSA) implies ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM+FSA) . x )
assume A16: x in dom (the_Values_of SCM+FSA) ; :: thesis: ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM+FSA) . x

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

suppose x = NAT ; :: thesis: ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM+FSA) . x

hence ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM+FSA) . x by A14, SCMFSA_1:9; :: thesis: verum

end;

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

then not x in dom (NAT .--> (a3 + 1)) by TARSKI:def 1;
then ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . x = the SCM+FSA-State . x by FUNCT_4:11;
hence ( the SCM+FSA-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM+FSA) . x by A16, CARD_3:9; :: thesis: verum

end;

end;

end;

dom (the_Values_of SCM+FSA) = SCM+FSA-Memory by SCMFSA_1:32;
then reconsider t = the SCM+FSA-State +* (NAT .--> (a3 + 1)) as State of SCM+FSA by A12, A15, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
NAT in dom (NAT .--> la) by TARSKI:def 1;
then A17: (w +* (NAT .--> la)) . NAT = (NAT .--> la) . NAT by FUNCT_4:13
.= la by FUNCOP_1:72 ;

per cases ( t . a <= 0 or t . a > 0 ) ;

suppose A18: t . a <= 0 ; :: thesis: contradiction

IC w = w . NAT ;
then reconsider e = w . NAT as Nat ;
IC t = IC w by SCMFSA_1:5, SUBSET_1:def 8;
then A19: (Exec ((a >0_goto la),t)) . (IC ) = e + 1 by A18, Th64;
(Exec ((a >0_goto la),t)) . (IC ) = w . NAT by A13, Th1;
hence contradiction by A19; :: thesis: verum

end;

suppose A20: t . a > 0 ; :: thesis: contradiction

(w +* (NAT .--> la)) . NAT = (SCM+FSA-Chg (w,a3)) . NAT
.= a3 by SCMFSA_1:19
.= (Exec ((a >0_goto la),t)) . NAT by A20, Th1, Th64
.= t . NAT by A13 ;
hence contradiction by A14, A17; :: thesis: verum

end;

end;