let la be Element of NAT ; :: thesis: not goto la is halting
set f = the Object-Kind of SCM+FSA;
consider s being SCM+FSA-State;
assume A1: goto la is halting ; :: thesis: contradiction
reconsider a3 = la as Element of NAT ;
set t = s +* (NAT .--> (succ a3));
A2: dom s = the carrier of SCM+FSA by PARTFUN1:def 4;
A3: dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:19;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def 1;
then A4: (s +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:14
.= succ a3 by FUNCOP_1:87 ;
A5: for x being set st x in dom the Object-Kind of SCM+FSA holds
(s +* (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 (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM+FSA . x )
assume A6: x in dom the Object-Kind of SCM+FSA ; :: thesis: (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM+FSA . x

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

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

hence (s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM+FSA . x by A4, SCMFSA_1:9; :: thesis: verum

end;

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

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

end;

end;

end;

A7: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5, ZFMISC_1:37;
A8: dom (s +* (NAT .--> (succ a3))) = (dom s) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) by A2
.= SCM+FSA-Memory \/ {NAT} by FUNCOP_1:19
.= SCM+FSA-Memory by A7, XBOOLE_1:12 ;
dom the Object-Kind of SCM+FSA = SCM+FSA-Memory by FUNCT_2:def 1;
then reconsider t = s +* (NAT .--> (succ a3)) as State of SCM+FSA by A8, A5, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
reconsider w = t as SCM+FSA-State by PBOOLE:155;
dom (NAT .--> la) = {NAT} by FUNCOP_1:19;
then NAT in dom (NAT .--> la) by TARSKI:def 1;
then A9: (w +* (NAT .--> la)) . NAT = (NAT .--> la) . NAT by FUNCT_4:14
.= la by FUNCOP_1:87 ;
(w +* (NAT .--> la)) . NAT = (SCM+FSA-Chg (w,a3)) . NAT
.= a3 by SCMFSA_1:20
.= (Exec ((goto la),t)) . NAT by Th7, Th95
.= t . NAT by A1, EXTPRO_1:def 3 ;
hence contradiction by A4, A9; :: thesis: verum