set q = Euclid-Algorithm ;
set p = Start-At (0,SCM);
let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in dom Euclid-Function or ex b1 being set st
( x = b1 & (Start-At (0,SCM)) +* b1 is Autonomy of Euclid-Algorithm & Euclid-Function . b1 c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* b1)) ) )

DataPart (Start-At (0,SCM)) = {} by MEMSTR_0:20;
then A1: dom (DataPart (Start-At (0,SCM))) = {} ;
assume x in dom Euclid-Function ; :: thesis: ex b1 being set st
( x = b1 & (Start-At (0,SCM)) +* b1 is Autonomy of Euclid-Algorithm & Euclid-Function . b1 c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* b1)) )

then consider i1, i2 being Integer such that
A2: i1 > 0 and
A3: i2 > 0 and
A4: x = ((),(dl. 1)) --> (i1,i2) by Th8;
x = (() .--> i1) +* ((dl. 1) .--> i2) by A4;
then reconsider d = x as FinPartState of SCM ;
consider t being State of SCM such that
A5: (Start-At (0,SCM)) +* d c= t by PBOOLE:141;
consider T being Instruction-Sequence of SCM such that
A6: Euclid-Algorithm c= T by PBOOLE:145;
A7: dom d = {(),(dl. 1)} by ;
then A8: dl. 1 in dom d by TARSKI:def 2;
A9: dl. 0 in dom d by ;
A10: for t being State of SCM st (Start-At (0,SCM)) +* d c= t holds
( t . () = i1 & t . (dl. 1) = i2 )
proof
let t be State of SCM; :: thesis: ( (Start-At (0,SCM)) +* d c= t implies ( t . () = i1 & t . (dl. 1) = i2 ) )
assume A11: (Start-At (0,SCM)) +* d c= t ; :: thesis: ( t . () = i1 & t . (dl. 1) = i2 )
d c= (Start-At (0,SCM)) +* d by FUNCT_4:25;
then A12: d c= t by A11;
hence t . () = d . () by
.= i1 by ;
:: thesis: t . (dl. 1) = i2
thus t . (dl. 1) = d . (dl. 1) by
.= i2 by ; :: thesis: verum
end;
A14: now :: thesis: not dom (Start-At (0,SCM)) meets dom d
assume dom (Start-At (0,SCM)) meets dom d ; :: thesis: contradiction
then consider x being object such that
A15: x in dom (Start-At (0,SCM)) and
A16: x in dom d by XBOOLE_0:3;
A17: x = IC by ;
( x = dl. 0 or x = dl. 1 ) by ;
hence contradiction by A17, AMI_3:13; :: thesis: verum
end;
then A18: Start-At (0,SCM) c= (Start-At (0,SCM)) +* d by FUNCT_4:32;
A19: IC in dom (Start-At (0,SCM)) by TARSKI:def 1;
(dom (Start-At (0,SCM))) /\ (dom d) = {} by ;
then A20: not IC in dom d by ;
set A = {(),(),(dl. 1)};
set C = 5;
A21: dom ((Start-At (0,SCM)) +* d) = dom ((Start-At (0,SCM)) +* d)
.= (dom (Start-At (0,SCM))) \/ (dom d) by FUNCT_4:def 1
.= ({()} \/ (dom (DataPart (Start-At (0,SCM))))) \/ (dom d) by
.= {()} \/ {(),(dl. 1)} by
.= {(),(),(dl. 1)} by ENUMSET1:2 ;
A22: dom (Start-At (0,SCM)) c= dom ((Start-At (0,SCM)) +* d) by ;
IC ((Start-At (0,SCM)) +* d) = IC (Start-At (0,SCM)) by
.= 0 by FUNCOP_1:72 ;
then A23: (Start-At (0,SCM)) +* d is 0 -started by ;
then A24: t is 0 -started by ;
A25: (Start-At (0,SCM)) +* d is Euclid-Algorithm -autonomic
proof
set A = {(),(),(dl. 1)};
set C = 5;
let P, Q be Instruction-Sequence of SCM; :: according to EXTPRO_1:def 10 :: thesis: ( not Euclid-Algorithm c= P or not Euclid-Algorithm c= Q or for b1, b2 being set holds
( not (Start-At (0,SCM)) +* d c= b1 or not (Start-At (0,SCM)) +* d c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,b2,b3)) | (dom ((Start-At (0,SCM)) +* d)) ) )

assume that
A26: Euclid-Algorithm c= P and
A27: Euclid-Algorithm c= Q ; :: thesis: for b1, b2 being set holds
( not (Start-At (0,SCM)) +* d c= b1 or not (Start-At (0,SCM)) +* d c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,b2,b3)) | (dom ((Start-At (0,SCM)) +* d)) )

let s1, s2 be State of SCM; :: thesis: ( not (Start-At (0,SCM)) +* d c= s1 or not (Start-At (0,SCM)) +* d c= s2 or for b1 being set holds (Comput (P,s1,b1)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b1)) | (dom ((Start-At (0,SCM)) +* d)) )
assume that
A28: (Start-At (0,SCM)) +* d c= s1 and
A29: (Start-At (0,SCM)) +* d c= s2 ; :: thesis: for b1 being set holds (Comput (P,s1,b1)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b1)) | (dom ((Start-At (0,SCM)) +* d))
A30: ( s2 . () = i1 & s2 . (dl. 1) = i2 ) by ;
let k be Nat; :: thesis: (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d))
defpred S2[ Nat] means ( IC (Comput (P,s1,\$1)) = IC (Comput (Q,s2,\$1)) & (Comput (P,s1,\$1)) . () = (Comput (Q,s2,\$1)) . () & (Comput (P,s1,\$1)) . (dl. 1) = (Comput (Q,s2,\$1)) . (dl. 1) );
A31: ( Comput (P,s1,0) = s1 & Comput (Q,s2,0) = s2 ) by EXTPRO_1:2;
A32: s1 is 0 -started by ;
A33: dom (Comput (P,s1,k)) = the carrier of SCM by PARTFUN1:def 2
.= dom (Comput (Q,s2,k)) by PARTFUN1:def 2 ;
A34: s2 is 0 -started by ;
A35: for i, j being Nat st S2[4 * i] & j <> 0 & j <= 4 holds
S2[(4 * i) + j]
proof
let i, j be Nat; :: thesis: ( S2[4 * i] & j <> 0 & j <= 4 implies S2[(4 * i) + j] )
assume that
A36: IC (Comput (P,s1,(4 * i))) = IC (Comput (Q,s2,(4 * i))) and
A37: (Comput (P,s1,(4 * i))) . () = (Comput (Q,s2,(4 * i))) . () and
A38: (Comput (P,s1,(4 * i))) . (dl. 1) = (Comput (Q,s2,(4 * i))) . (dl. 1) ; :: thesis: ( not j <> 0 or not j <= 4 or S2[(4 * i) + j] )
assume A39: ( j <> 0 & j <= 4 ) ; :: thesis: S2[(4 * i) + j]
then not not j = 0 & ... & not j = 4 ;
then A40: not not j = 1 & ... & not j = 4 by A39;
per cases ( IC (Comput (Q,s2,(4 * i))) = 0 or IC (Comput (Q,s2,(4 * i))) = 4 ) by A2, A3, A34, A27, A30, Lm4;
suppose A41: IC (Comput (Q,s2,(4 * i))) = 0 ; :: thesis: S2[(4 * i) + j]
A42: (Comput (P,s1,((4 * i) + 1))) . () = (Comput (P,s1,(4 * i))) . () by A26, A36, A41, Th2
.= (Comput (Q,s2,((4 * i) + 1))) . () by A27, A37, A41, Th2 ;
A43: (Comput (P,s1,((4 * i) + 1))) . (dl. 2) = (Comput (P,s1,(4 * i))) . (dl. 1) by A26, A36, A41, Th2
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 2) by A27, A38, A41, Th2 ;
A44: (Comput (P,s1,((4 * i) + 1))) . (dl. 1) = (Comput (P,s1,(4 * i))) . (dl. 1) by A26, A36, A41, Th2
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 1) by A27, A38, A41, Th2 ;
A45: ((4 * i) + 1) + 1 = (4 * i) + (1 + 1) ;
A46: ((4 * i) + 2) + 1 = (4 * i) + (2 + 1) ;
A47: IC (Comput (Q,s2,((4 * i) + 1))) = 1 by ;
then A48: IC (Comput (Q,s2,((4 * i) + 2))) = 2 by ;
then A49: IC (Comput (Q,s2,((4 * i) + 3))) = 3 by ;
A50: IC (Comput (P,s1,((4 * i) + 1))) = 1 by A26, A36, A41, Th2;
then A51: (Comput (P,s1,((4 * i) + 2))) . (dl. 2) = (Comput (P,s1,((4 * i) + 1))) . (dl. 2) by
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 2) by A27, A45, A47, A43, Th3 ;
A52: (Comput (P,s1,((4 * i) + 2))) . (dl. 1) = ((Comput (P,s1,((4 * i) + 1))) . ()) mod ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 1) by A27, A45, A47, A42, A44, Th3 ;
A53: IC (Comput (P,s1,((4 * i) + 2))) = 2 by A26, A45, A50, Th3;
then A54: IC (Comput (P,s1,((4 * i) + 3))) = 3 by ;
A55: (Comput (P,s1,((4 * i) + 2))) . () = ((Comput (P,s1,((4 * i) + 1))) . ()) div ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3
.= (Comput (Q,s2,((4 * i) + 2))) . () by A27, A45, A47, A42, A44, Th3 ;
A56: ((4 * i) + 3) + 1 = (4 * i) + (3 + 1) ;
A57: (Comput (P,s1,((4 * i) + 3))) . () = (Comput (P,s1,((4 * i) + 2))) . (dl. 2) by A26, A46, A53, Th4
.= (Comput (Q,s2,((4 * i) + 3))) . () by A27, A46, A48, A51, Th4 ;
A58: (Comput (P,s1,((4 * i) + 3))) . (dl. 1) = (Comput (P,s1,((4 * i) + 2))) . (dl. 1) by A26, A46, A53, Th4
.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 1) by A27, A46, A48, A52, Th4 ;
( (Comput (P,s1,((4 * i) + 3))) . (dl. 1) <= 0 or (Comput (P,s1,((4 * i) + 3))) . (dl. 1) > 0 ) ;
then ( ( IC (Comput (P,s1,((4 * i) + 4))) = 4 & IC (Comput (Q,s2,((4 * i) + 4))) = 4 ) or ( IC (Comput (P,s1,((4 * i) + 4))) = 0 & IC (Comput (Q,s2,((4 * i) + 4))) = 0 ) ) by A26, A27, A56, A54, A49, A58, Th5;
hence IC (Comput (P,s1,((4 * i) + j))) = IC (Comput (Q,s2,((4 * i) + j))) by A40, A50, A27, A41, Th2, A26, A45, Th3, A48, A54, A46, Th4; :: thesis: ( (Comput (P,s1,((4 * i) + j))) . () = (Comput (Q,s2,((4 * i) + j))) . () & (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) )
(Comput (P,s1,((4 * i) + 4))) . () = (Comput (P,s1,((4 * i) + 3))) . () by A26, A56, A54, Th5
.= (Comput (Q,s2,((4 * i) + 4))) . () by A27, A56, A49, A57, Th5 ;
hence (Comput (P,s1,((4 * i) + j))) . () = (Comput (Q,s2,((4 * i) + j))) . () by A40, A42, A55, A57; :: thesis: (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1)
(Comput (P,s1,((4 * i) + 4))) . (dl. 1) = (Comput (P,s1,((4 * i) + 3))) . (dl. 1) by A26, A56, A54, Th5
.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 1) by A27, A56, A49, A58, Th5 ;
hence (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) by A40, A44, A52, A58; :: thesis: verum
end;
suppose A59: IC (Comput (Q,s2,(4 * i))) = 4 ; :: thesis: S2[(4 * i) + j]
then P halts_at IC (Comput (P,s1,(4 * i))) by ;
then A60: Comput (P,s1,((4 * i) + j)) = Comput (P,s1,(4 * i)) by ;
Q halts_at IC (Comput (Q,s2,(4 * i))) by ;
hence S2[(4 * i) + j] by ; :: thesis: verum
end;
end;
end;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
(Comput (P,s1,0)) . () = IC s1 by EXTPRO_1:2
.= 0 by A32
.= IC s2 by A34
.= (Comput (Q,s2,0)) . () by EXTPRO_1:2 ;
then A61: S2[ 0 ] by A10, A28, A30, A31;
A62: 4 > 0 ;
S2[k] from NAT_D:sch 2(A61, A62, A35);
hence (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d)) by ; :: thesis: verum
end;
take d ; :: thesis: ( x = d & (Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm & Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) )
thus x = d ; :: thesis: ( (Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm & Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) )
A63: (Start-At (0,SCM)) +* d is Euclid-Algorithm -halted
proof
reconsider i19 = i1, i29 = i2 as Element of NAT by ;
let t be State of SCM; :: according to EXTPRO_1:def 11 :: thesis: ( not (Start-At (0,SCM)) +* d c= t or for b1 being set holds
( not Euclid-Algorithm c= b1 or b1 halts_on t ) )

assume A64: (Start-At (0,SCM)) +* d c= t ; :: thesis: for b1 being set holds
( not Euclid-Algorithm c= b1 or b1 halts_on t )

let P be Instruction-Sequence of SCM; :: thesis: ( not Euclid-Algorithm c= P or P halts_on t )
assume A65: Euclid-Algorithm c= P ; :: thesis: P halts_on t
set t9 = Comput (P,t,4);
A66: t . (dl. 1) = i2 by ;
A67: ( t is 0 -started & t . () = i1 ) by ;
per cases ( i1 > i2 or i1 = i2 or i1 < i2 ) by XXREAL_0:1;
suppose A68: i1 = i2 ; :: thesis: P halts_on t
A69: i1 mod i2 = i19 mod i29
.= 0 by ;
A70: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ;
t = Comput (P,t,(4 * 0)) by EXTPRO_1:2;
then (Comput (P,t,4)) . (dl. 1) = (t . ()) mod (t . (dl. 1)) by A2, A3, A65, A67, A66, A70, Lm5;
then IC (Comput (P,t,4)) = 4 by A2, A3, A65, A67, A66, A69, A70, Lm4;
then P halts_at IC (Comput (P,t,4)) by ;
hence P halts_on t by EXTPRO_1:16; :: thesis: verum
end;
suppose A71: i1 < i2 ; :: thesis: P halts_on t
A72: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ;
A73: t = Comput (P,t,(4 * 0)) by EXTPRO_1:2;
i1 mod i2 = i19 mod i29
.= i19 by ;
then A74: (Comput (P,t,4)) . (dl. 1) = i1 by A2, A3, A65, A67, A66, A73, A72, Lm5;
then IC (Comput (P,t,4)) = 0 by A2, A3, A65, A67, A66, A72, Lm4;
then A75: Comput (P,t,4) is 0 -started ;
(Comput (P,t,4)) . () = i2 by A2, A3, A65, A67, A66, A73, A72, Lm5;
then consider k0 being Nat such that
A76: P halts_at IC (Comput (P,(Comput (P,t,4)),k0)) by A2, A71, A74, A75, A65, Lm6;
P halts_at IC (Comput (P,t,(k0 + 4))) by ;
hence P halts_on t by EXTPRO_1:16; :: thesis: verum
end;
end;
end;
thus (Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm by ; :: thesis: Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d))
then A77: Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) = (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by ;
dl. 0 in the carrier of SCM ;
then A78: dl. 0 in dom (Result (T,t)) by PARTFUN1:def 2;
A79: d . () = i1 by ;
A80: d . (dl. 1) = i2 by ;
A81: d c= (Start-At (0,SCM)) +* d by FUNCT_4:25;
A82: dom d c= dom ((Start-At (0,SCM)) +* d) by ;
A83: d c= t by ;
A84: dom d = {(),(dl. 1)} by ;
then A85: dl. 1 in dom d by TARSKI:def 2;
A86: t . (dl. 1) = i2 by ;
A87: dl. 0 in dom d by ;
t . () = i1 by ;
then A88: (Result (T,t)) . () = i1 gcd i2 by A2, A3, A24, A86, Th7, A6;
dom (() .--> (i1 gcd i2)) c= dom d by ;
then A90: dom (() .--> (i1 gcd i2)) c= dom ((Start-At (0,SCM)) +* d) by A82;
(dl. 0) .--> (i1 gcd i2) c= (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by ;
hence Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) by A77, A2, A3, A4, Th9; :: thesis: verum