take p = ((Start-At (il. 0 )) +* Euclide-Algorithm ) +* ((dl. 0 ),(dl. 1) --> 1,1); :: thesis: ( p is autonomic & not p is NAT -defined )
(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 & ((Start-At (il. 0 )) +* Euclide-Algorithm ) +* s is pre-program of SCM & Euclide-Function . s c= Result (((Start-At (il. 0 )) +* Euclide-Algorithm ) +* s) ) by AMI_1:def 29, AMI_4:13;
hence p is autonomic ; :: thesis: not p is NAT -defined
take IC SCM ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( IC SCM in dom p & not IC SCM in NAT )
dom (Start-At (il. 0 )) = {(IC SCM )} by FUNCOP_1:19;
then ( dom ((Start-At (il. 0 )) +* Euclide-Algorithm ) = (dom (Start-At (il. 0 ))) \/ (dom Euclide-Algorithm ) & IC SCM in dom (Start-At (il. 0 )) ) by FUNCT_4:def 1, TARSKI:def 1;
then ( dom p = (dom ((Start-At (il. 0 )) +* Euclide-Algorithm )) \/ (dom ((dl. 0 ),(dl. 1) --> 1,1)) & IC SCM in dom ((Start-At (il. 0 )) +* Euclide-Algorithm ) ) by FUNCT_4:def 1, XBOOLE_0:def 3;
hence IC SCM in dom p by XBOOLE_0:def 3; :: thesis: not IC SCM in NAT
assume IC SCM in NAT ; :: thesis: contradiction
hence contradiction by AMI_3:4; :: thesis: verum