reconsider a3 = la as Element of NAT ;
set t = the SCM+FSA-State +* (NAT .--> (succ a3));
A1: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5, ZFMISC_1:31;
A3: dom ( the SCM+FSA-State +* (NAT .--> (succ a3))) = (dom the SCM+FSA-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) by PARTFUN1:def 2
.= SCM+FSA-Memory \/ {NAT} by FUNCOP_1:13
.= SCM+FSA-Memory by A1, XBOOLE_1:12 ;
assume A4: a >0_goto la is halting ; :: thesis: contradiction
A5: dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def 1;
then A6: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A7: for x being set st x in dom the Object-Kind of SCM+FSA holds
( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM+FSA . x
proof
let x be set ; :: thesis: ( x in dom the Object-Kind of SCM+FSA implies ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM+FSA . x )
assume A8: x in dom the Object-Kind of SCM+FSA ; :: thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM+FSA . x
per cases ( x = NAT or x <> NAT ) ;
end;
end;
dom the Object-Kind of SCM+FSA = SCM+FSA-Memory by FUNCT_2:def 1;
then reconsider t = the SCM+FSA-State +* (NAT .--> (succ a3)) as State of SCM+FSA by A3, A7, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
dom (NAT .--> la) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> la) by TARSKI:def 1;
then A9: (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 A10: t . a <= 0 ; :: thesis: contradiction
IC w = w . NAT ;
then reconsider e = w . NAT as Element of NAT ;
IC t = IC w by FUNCT_7:def 1, SCMFSA_1:5;
then A11: (Exec ((a >0_goto la),t)) . (IC ) = succ e by A10, Th97;
(Exec ((a >0_goto la),t)) . (IC ) = w . NAT by A4, Th7, EXTPRO_1:def 3;
hence contradiction by A11; :: thesis: verum
end;
suppose A12: 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 A12, Th7, Th97
.= t . NAT by A4, EXTPRO_1:def 3 ;
hence contradiction by A6, A9; :: thesis: verum
end;
end;