let I be Program of SCM+FSA ; :: thesis: ( I is parahalting implies I is paraclosed )
assume A1: I is parahalting ; :: thesis: I is paraclosed
let s be State of SCM+FSA ; :: according to SCMFSA6B:def 2 :: thesis: for n being Element of NAT st I +* (Start-At (insloc 0 )) c= s holds
IC (Computation s,n) in dom I
let n be Element of NAT ; :: thesis: ( I +* (Start-At (insloc 0 )) c= s implies IC (Computation s,n) in dom I )
assume A2: I +* (Start-At (insloc 0 )) c= s ; :: thesis: IC (Computation s,n) in dom I
defpred S₁[ Nat] means not IC (Computation s,c₁) in dom I;
assume not IC (Computation 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;
set s2 = Computation s,n;
set s0 = s +* (IC (Computation s,n)),(goto (IC (Computation s,n)));
set s1 = (Computation s,n) +* (IC (Computation s,n)),(goto (IC (Computation s,n)));
set IAt = I +* (Start-At (insloc 0 ));
dom I misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then A6: I c= I +* (Start-At (insloc 0 )) by FUNCT_4:33;
A7: IC (Computation s,n) in NAT by AMI_1:def 4;
A8: I +* (Start-At (insloc 0 )) is halting by A1, Def3;
(I +* (Start-At (insloc 0 ))) | NAT = I by Th6;
then dom I = (dom (I +* (Start-At (insloc 0 )))) /\ NAT by RELAT_1:90;
then not IC (Computation s,n) in dom (I +* (Start-At (insloc 0 ))) by A4, A7, XBOOLE_0:def 4;
then A9: I +* (Start-At (insloc 0 )) c= s +* (IC (Computation s,n)),(goto (IC (Computation s,n))) by A2, FUNCT_7:91;
then A10: s +* (IC (Computation s,n)),(goto (IC (Computation s,n))) is halting by A8, AMI_1:def 26;
A11: s +* (IC (Computation s,n)),(goto (IC (Computation s,n))),s equal_outside NAT by A7, FUNCT_7:28, FUNCT_7:93;
A12: I c= s +* (IC (Computation s,n)),(goto (IC (Computation s,n))) by A6, A9, XBOOLE_1:1;
A13: I c= s by A2, A6, XBOOLE_1:1;
for m being Element of NAT st m < n holds
IC (Computation s,m) in dom I by A5;
then A14: Computation (s +* (IC (Computation s,n)),(goto (IC (Computation s,n)))),n, Computation s,n equal_outside NAT by A11, A12, A13, Th21;
A15: Computation s,n,(Computation s,n) +* (IC (Computation s,n)),(goto (IC (Computation s,n))) equal_outside NAT by A7, FUNCT_7:93;
A16: s | NAT = (Computation s,n) | NAT by AMI_1:123;
(Computation (s +* (IC (Computation s,n)),(goto (IC (Computation s,n)))),n) | NAT = (s +* (IC (Computation s,n)),(goto (IC (Computation s,n)))) | NAT by AMI_1:123
.= ((Computation s,n) +* (IC (Computation s,n)),(goto (IC (Computation s,n)))) | NAT by A16, FUNCT_7:95 ;
then A17: Computation (s +* (IC (Computation s,n)),(goto (IC (Computation s,n)))),n = (Computation s,n) +* (IC (Computation s,n)),(goto (IC (Computation s,n))) by A14, A15, FUNCT_7:29, FUNCT_7:92;
not (Computation s,n) +* (IC (Computation s,n)),(goto (IC (Computation s,n))) is halting by Th20;
hence contradiction by A10, A17, AMI_1:93; :: thesis: verum