set q = ProgramPart ((Start-At 0 ,SCM ) +* Euclide-Algorithm );
set d = (Start-At 0 ,SCM ) +* Euclide-Algorithm ;
take p = ((ProgramPart ((Start-At 0 ,SCM ) +* Euclide-Algorithm )) +* ((Start-At 0 ,SCM ) +* Euclide-Algorithm )) +* ((dl. 0 ),(dl. 1) --> 1,1); :: thesis: ( p is autonomic & not p is NAT -defined )
X: ProgramPart ((Start-At 0 ,SCM ) +* Euclide-Algorithm ),(Start-At 0 ,SCM ) +* Euclide-Algorithm computes Euclide-Function by AMI_4:13;
(dl. 0 ),(dl. 1) --> 1,1 in dom Euclide-Function by AMI_4:11;
then ex s being FinPartState of SCM st
( (dl. 0 ),(dl. 1) --> 1,1 = s & ((ProgramPart ((Start-At 0 ,SCM ) +* Euclide-Algorithm )) +* ((Start-At 0 ,SCM ) +* Euclide-Algorithm )) +* s is pre-program of SCM & Euclide-Function . s c= Result (ProgramPart ((Start-At 0 ,SCM ) +* Euclide-Algorithm )),(((Start-At 0 ,SCM ) +* Euclide-Algorithm ) +* s) ) by X, AMI_1:def 30;
hence p is autonomic ; :: thesis: not p is NAT -defined
take dl. 0 ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( dl. 0 in proj1 p & not dl. 0 in NAT )
dom ((dl. 0 ),(dl. 1) --> 1,1) = {(dl. 0 ),(dl. 1)} by FUNCT_4:65;
then A: dl. 0 in dom ((dl. 0 ),(dl. 1) --> 1,1) by TARSKI:def 2;
dom p = (dom ((ProgramPart ((Start-At 0 ,SCM ) +* Euclide-Algorithm )) +* ((Start-At 0 ,SCM ) +* Euclide-Algorithm ))) \/ (dom ((dl. 0 ),(dl. 1) --> 1,1)) by FUNCT_4:def 1;
hence dl. 0 in dom p by A, XBOOLE_0:def 3; :: thesis: not dl. 0 in NAT
assume dl. 0 in NAT ; :: thesis: contradiction
hence contradiction by AMI_3:56; :: thesis: verum