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 consider s being FinPartState of SCM such that
A1: (dl. 0 ),(dl. 1) --> 1,1 = s and
A2: ((Start-At (il. 0 )) +* Euclide-Algorithm ) +* s is pre-program of SCM and
Euclide-Function . s c= Result (((Start-At (il. 0 )) +* Euclide-Algorithm ) +* s) by AMI_1:def 29, AMI_4:13;
thus p is autonomic by A1, A2; :: 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 )
A3: dom p = (dom ((Start-At (il. 0 )) +* Euclide-Algorithm )) \/ (dom ((dl. 0 ),(dl. 1) --> 1,1)) by FUNCT_4:def 1;
A4: dom ((Start-At (il. 0 )) +* Euclide-Algorithm ) = (dom (Start-At (il. 0 ))) \/ (dom Euclide-Algorithm ) by FUNCT_4:def 1;
dom (Start-At (il. 0 )) = {(IC SCM )} by FUNCOP_1:19;
then IC SCM in dom (Start-At (il. 0 )) by TARSKI:def 1;
then IC SCM in dom ((Start-At (il. 0 )) +* Euclide-Algorithm ) by A4, XBOOLE_0:def 3;
hence IC SCM in dom p by A3, 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