set f = the Object-Kind of SCM+FSA;
set s = the SCM+FSA-State;
assume A1:
goto la is halting
; contradiction
reconsider a3 = la as Element of NAT ;
set t = the SCM+FSA-State +* (NAT .--> (succ a3));
A3:
dom (NAT .--> (succ a3)) = {NAT}
by FUNCOP_1:13;
then
NAT in dom (NAT .--> (succ a3))
by TARSKI:def 1;
then A4: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . NAT =
(NAT .--> (succ a3)) . NAT
by FUNCT_4:13
.=
succ a3
by FUNCOP_1:72
;
A5:
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
A7:
{NAT} c= SCM+FSA-Memory
by SCMFSA_1:5, ZFMISC_1:31;
A8: 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 A7, XBOOLE_1:12
;
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 A8, A5, 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
;
(w +* (NAT .--> la)) . NAT =
(SCM+FSA-Chg (w,a3)) . NAT
.=
a3
by SCMFSA_1:19
.=
(Exec ((goto la),t)) . NAT
by Th7, Th95
.=
t . NAT
by A1, EXTPRO_1:def 3
;
hence
contradiction
by A4, A9; verum