let la be Instruction-Location of SCM+FSA ; :: thesis: for a being Int-Location holds not a >0_goto la is halting
let a be Int-Location ; :: thesis: not a >0_goto la is halting
reconsider a3 = la as Element of NAT by AMI_1:def 4;
consider s being SCM+FSA-State;
set t = s +* (NAT .--> (succ a3));
set f = the Object-Kind of SCM+FSA ;
A1: dom (NAT .--> (succ a3)) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def 1;
then A2: (s +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:14
.= succ a3 by FUNCOP_1:87 ;
A3: {NAT } c= SCM+FSA-Memory by SCMFSA_1:5, ZFMISC_1:37;
A4: dom s = dom SCM+FSA-OK by CARD_3:18;
A5: dom (s +* (NAT .--> (succ a3))) = (dom s) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) by A4, FUNCT_2:def 1
.= SCM+FSA-Memory \/ {NAT } by FUNCOP_1:19
.= SCM+FSA-Memory by A3, XBOOLE_1:12 ;
A6: dom the Object-Kind of SCM+FSA = SCM+FSA-Memory by FUNCT_2:def 1;
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 A7: 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 A2, SCMFSA_1:9; :: thesis: verum
end;
end;
end;
then reconsider t = s +* (NAT .--> (succ a3)) as State of SCM+FSA by A5, A6, CARD_3:18;
reconsider w = t as SCM+FSA-State ;
dom (NAT .--> la) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> la) by TARSKI:def 1;
then A8: (w +* (NAT .--> la)) . NAT = (NAT .--> la) . NAT by FUNCT_4:14
.= la by FUNCOP_1:87 ;
assume A9: a >0_goto la is halting ; :: thesis: contradiction
per cases ( t . a <= 0 or t . a > 0 ) ;
suppose A10: t . a <= 0 ; :: thesis: contradiction
A11: IC t = IC w by FUNCT_7:def 1, SCMFSA_1:5;
A12: IC w = w . NAT ;
A13: (Exec (a >0_goto la),t) . (IC SCM+FSA ) = w . NAT by A9, Th7, AMI_1:def 8;
reconsider e = w . NAT as Instruction-Location of SCM+FSA by A12, AMI_1:def 4;
A14: (Exec (a >0_goto la),t) . (IC SCM+FSA ) = Next by A10, A11, Th97;
thus contradiction by A13, A14; :: thesis: verum
end;
suppose A15: t . a > 0 ; :: thesis: contradiction
(w +* (NAT .--> la)) . NAT = (SCM+FSA-Chg w,a3) . NAT
.= a3 by SCMFSA_1:20
.= (Exec (a >0_goto la),t) . NAT by A15, Th7, Th97
.= t . NAT by A9, AMI_1:def 8 ;
hence contradiction by A2, A8; :: thesis: verum
end;
end;