let I be Program of SCM+FSA ; :: thesis: ( I is InitHalting implies I is InitClosed )
set II = Initialized I;
assume I is InitHalting ; :: thesis: I is InitClosed
then A1: Initialized I is halting by Def2;
let s be State of SCM+FSA ; :: according to SCM_HALT:def 1 :: thesis: for n being Element of NAT st Initialized I c= s holds
IC (Comput (ProgramPart s),s,n) in dom I
let n be Element of NAT ; :: thesis: ( Initialized I c= s implies IC (Comput (ProgramPart s),s,n) in dom I )
assume A2: Initialized I c= s ; :: thesis: IC (Comput (ProgramPart s),s,n) in dom I
defpred S₁[ Nat] means not IC (Comput (ProgramPart s),s,c₁) in dom I;
assume not IC (Comput (ProgramPart s),s,n) in dom I ; :: thesis: contradiction
then A3: ex n being Nat st S₁[n] ;
consider n being Nat such that
A4: S₁[n] and
A5: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A3);
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A6: for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s),s,m) in dom I by A5;
set s2 = Comput (ProgramPart s),s,n;
set s0 = s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)));
set s1 = (Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)));
A7: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,n) by AMI_1:123;
A8: ProgramPart (Comput (ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))))),(s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))),n) = ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))) by AMI_1:123
.= ((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))) | NAT by A7, FUNCT_7:95 ;
A10: s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))),s equal_outside NAT by FUNCT_7:28, FUNCT_7:93;
A11: I c= Initialized I by SCMFSA6A:26;
then A12: I c= s by A2, XBOOLE_1:1;
A13: Comput (ProgramPart s),s,n,(Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) equal_outside NAT by FUNCT_7:93;
(Initialized I) | NAT = I by SCMFSA6A:33;
then dom I = (dom (Initialized I)) /\ NAT by RELAT_1:90;
then not IC (Comput (ProgramPart s),s,n) in dom (Initialized I) by A4, XBOOLE_0:def 4;
then A14: Initialized I c= s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) by A2, FUNCT_7:91;
then I c= s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) by A11, XBOOLE_1:1;
then Comput (ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))))),(s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))),n, Comput (ProgramPart s),s,n equal_outside NAT by A10, A12, A6, SCMFSA6B:21;
then Comput (ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))))),(s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))),n,(Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) equal_outside NAT by A13, A8, FUNCT_7:29;
then A15: Comput (ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))))),(s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))),n = (Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) by A13, A8, FUNCT_7:92;
A16: not ProgramPart ((Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))) halts_on (Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) by SCMFSA6B:20;
ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))) halts_on s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) by A1, A14, AMI_1:def 26;
then ProgramPart (s +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n)))) halts_on (Comput (ProgramPart s),s,n) +* (IC (Comput (ProgramPart s),s,n)),(goto (IC (Comput (ProgramPart s),s,n))) by A15, AMI_1:93;
hence contradiction by A15, A16, AMI_1:123; :: thesis: verum