let I be Program of SCM+FSA; :: thesis: ( I is parahalting implies I is paraclosed )
set IAt = I +* (Start-At (0,SCM+FSA));
dom I misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then A1: I c= I +* (Start-At (0,SCM+FSA)) by FUNCT_4:33;
assume I is parahalting ; :: thesis: I is paraclosed
then A2: I +* (Start-At (0,SCM+FSA)) is halting by Def3;
let s be State of SCM+FSA; :: according to SCMFSA6B:def 2 :: thesis: for n being Element of NAT st I +* (Start-At (0,SCM+FSA)) c= s holds
IC (Comput ((ProgramPart s),s,n)) in dom I
let n be Element of NAT ; :: thesis: ( I +* (Start-At (0,SCM+FSA)) c= s implies IC (Comput ((ProgramPart s),s,n)) in dom I )
defpred S₁[ Nat] means not IC (Comput ((ProgramPart s),s,c₁)) in dom I;
assume A3: I +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: IC (Comput ((ProgramPart s),s,n)) in dom I
then A4: I c= s by A1, XBOOLE_1:1;
assume not IC (Comput ((ProgramPart s),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 13;
A8: for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s),s,m)) in dom I by A7;
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)))));
A9: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,n)) by AMI_1:123;
A10: 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
.= ProgramPart ((Comput ((ProgramPart s),s,n)) +* ((IC (Comput ((ProgramPart s),s,n))),(goto (IC (Comput ((ProgramPart s),s,n)))))) by A9, FUNCT_7:95 ;
A12: 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;
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;
(I +* (Start-At (0,SCM+FSA))) | NAT = I by Th6;
then dom I = (dom (I +* (Start-At (0,SCM+FSA)))) /\ NAT by RELAT_1:90;
then not IC (Comput ((ProgramPart s),s,n)) in dom (I +* (Start-At (0,SCM+FSA))) by A6, XBOOLE_0:def 4;
then A14: I +* (Start-At (0,SCM+FSA)) c= s +* ((IC (Comput ((ProgramPart s),s,n))),(goto (IC (Comput ((ProgramPart s),s,n))))) by A3, FUNCT_7:91;
then I c= s +* ((IC (Comput ((ProgramPart s),s,n))),(goto (IC (Comput ((ProgramPart s),s,n))))) by A1, 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 A12, A4, A8, Th21;
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, A10, FUNCT_7:29, 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 Th20;
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 A2, A14, EXTPRO_1:def 10;
then ProgramPart (s +* ((IC (Comput ((ProgramPart s),s,n))),(goto (IC (Comput ((ProgramPart s),s,n)))))) halts_on 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) by EXTPRO_1:22;
hence contradiction by A15, A16, AMI_1:123; :: thesis: verum