let I be Program of SCM+FSA; :: thesis: ( I is InitHalting implies I is InitClosed )
assume Z: I is InitHalting ; :: thesis: I is InitClosed
let s be State of SCM+FSA; :: according to SCM_HALT:def 1 :: thesis: for P being Instruction-Sequence of SCM+FSA st I c= P holds
for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (P,s,n)) in dom I
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( I c= P implies for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (P,s,n)) in dom I )
assume A2: I c= P ; :: thesis: for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (P,s,n)) in dom I
let n be Element of NAT ; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies IC (Comput (P,s,n)) in dom I )
assume A3: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: IC (Comput (P,s,n)) in dom I
defpred S₁[ Nat] means not IC (Comput (P,s,c₁)) in dom I;
assume not IC (Comput (P,s,n)) in dom I ; :: thesis: contradiction
then A5: ex n being Nat st S₁[n] ;
consider n being Nat such that
A6: S₁[n] and
A7: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A5);
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A8: for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I by A7;
set s2 = Comput (P,s,n);
set p2 = P;
set s0 = s;
set p0 = P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))));
set s1 = Comput (P,s,n);
set p1 = P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))));
YY: I c= P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A2, A6, FUNCT_7:89;
then XX: Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),s,n) = Comput (P,s,n) by A8, A2, AMISTD_2:10;
P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on s by Z, Def2, A3, YY;
then P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),s,n) by EXTPRO_1:22;
hence contradiction by XX, SCMFSA6B:21; :: thesis: verum