set q = Euclid-Algorithm ;
set p = Start-At (0,SCM);
let x be set ; EXTPRO_1:def 14 ( 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
; 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. 0),(dl. 1)) --> (i1,i2)
by Th8;
x = ((dl. 0) .--> 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. 0),(dl. 1)}
by A4, FUNCT_4:62;
then A8:
dl. 1 in dom d
by TARSKI:def 2;
A9:
dl. 0 in dom d
by A7, TARSKI:def 2;
A10:
for t being State of SCM st (Start-At (0,SCM)) +* d c= t holds
( t . (dl. 0) = i1 & t . (dl. 1) = i2 )
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 A14, XBOOLE_0:def 7;
then A20:
not IC in dom d
by A19, XBOOLE_0:def 4;
set A = {(IC ),(dl. 0),(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
.=
({(IC )} \/ (dom (DataPart (Start-At (0,SCM))))) \/ (dom d)
by A19, MEMSTR_0:24
.=
{(IC )} \/ {(dl. 0),(dl. 1)}
by A4, A1, FUNCT_4:62
.=
{(IC ),(dl. 0),(dl. 1)}
by ENUMSET1:2
;
A22:
dom (Start-At (0,SCM)) c= dom ((Start-At (0,SCM)) +* d)
by A18, RELAT_1:11;
IC ((Start-At (0,SCM)) +* d) =
IC (Start-At (0,SCM))
by A20, FUNCT_4:11
.=
0
by FUNCOP_1:72
;
then A23:
(Start-At (0,SCM)) +* d is 0 -started
by A22, A19;
then A24:
t is 0 -started
by A5, MEMSTR_0:17;
A25:
(Start-At (0,SCM)) +* d is Euclid-Algorithm -autonomic
proof
set A =
{(IC ),(dl. 0),(dl. 1)};
set C = 5;
let P,
Q be
Instruction-Sequence of
SCM;
EXTPRO_1:def 10 ( 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
;
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;
( 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
;
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 . (dl. 0) = i1 &
s2 . (dl. 1) = i2 )
by A10, A29;
let k be
Nat;
(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)) . (dl. 0) = (Comput (Q,s2,$1)) . (dl. 0) &
(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 A23, A28, MEMSTR_0:17;
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 A23, A29, MEMSTR_0:17;
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;
( 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))) . (dl. 0) = (Comput (Q,s2,(4 * i))) . (dl. 0)
and A38:
(Comput (P,s1,(4 * i))) . (dl. 1) = (Comput (Q,s2,(4 * i))) . (dl. 1)
;
( not j <> 0 or not j <= 4 or S2[(4 * i) + j] )
assume A39:
(
j <> 0 &
j <= 4 )
;
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
;
S2[(4 * i) + j]A42:
(Comput (P,s1,((4 * i) + 1))) . (dl. 0) =
(Comput (P,s1,(4 * i))) . (dl. 0)
by A26, A36, A41, Th2
.=
(Comput (Q,s2,((4 * i) + 1))) . (dl. 0)
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 A27, A41, Th2;
then A48:
IC (Comput (Q,s2,((4 * i) + 2))) = 2
by A27, A45, Th3;
then A49:
IC (Comput (Q,s2,((4 * i) + 3))) = 3
by A27, A46, Th4;
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 A26, A45, Th3
.=
(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))) . (dl. 0)) 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 A26, A46, Th4;
A55:
(Comput (P,s1,((4 * i) + 2))) . (dl. 0) =
((Comput (P,s1,((4 * i) + 1))) . (dl. 0)) div ((Comput (P,s1,((4 * i) + 1))) . (dl. 1))
by A26, A45, A50, Th3
.=
(Comput (Q,s2,((4 * i) + 2))) . (dl. 0)
by A27, A45, A47, A42, A44, Th3
;
A56:
((4 * i) + 3) + 1
= (4 * i) + (3 + 1)
;
A57:
(Comput (P,s1,((4 * i) + 3))) . (dl. 0) =
(Comput (P,s1,((4 * i) + 2))) . (dl. 2)
by A26, A46, A53, Th4
.=
(Comput (Q,s2,((4 * i) + 3))) . (dl. 0)
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;
( (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) & (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) )(Comput (P,s1,((4 * i) + 4))) . (dl. 0) =
(Comput (P,s1,((4 * i) + 3))) . (dl. 0)
by A26, A56, A54, Th5
.=
(Comput (Q,s2,((4 * i) + 4))) . (dl. 0)
by A27, A56, A49, A57, Th5
;
hence
(Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0)
by A40, A42, A55, A57;
(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;
verum end; suppose A59:
IC (Comput (Q,s2,(4 * i))) = 4
;
S2[(4 * i) + j]then
P halts_at IC (Comput (P,s1,(4 * i)))
by A26, A36, Lm3;
then A60:
Comput (
P,
s1,
((4 * i) + j))
= Comput (
P,
s1,
(4 * i))
by EXTPRO_1:20, NAT_1:11;
Q halts_at IC (Comput (Q,s2,(4 * i)))
by A27, A59, Lm3;
hence
S2[
(4 * i) + j]
by A36, A37, A38, A60, EXTPRO_1:20, NAT_1:11;
verum end; end;
end;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
(Comput (P,s1,0)) . (IC ) =
IC s1
by EXTPRO_1:2
.=
0
by A32
.=
IC s2
by A34
.=
(Comput (Q,s2,0)) . (IC )
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 A21, A33, GRFUNC_1:31;
verum
end;
take
d
; ( 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
; ( (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 A2, A3, INT_1:3;
let t be
State of
SCM;
EXTPRO_1:def 11 ( 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
;
for b1 being set holds
( not Euclid-Algorithm c= b1 or b1 halts_on t )
let P be
Instruction-Sequence of
SCM;
( not Euclid-Algorithm c= P or P halts_on t )
assume A65:
Euclid-Algorithm c= P
;
P halts_on t
set t9 =
Comput (
P,
t,4);
A66:
t . (dl. 1) = i2
by A10, A64;
A67:
(
t is
0 -started &
t . (dl. 0) = i1 )
by A23, A10, A64, MEMSTR_0:17;
per cases
( i1 > i2 or i1 = i2 or i1 < i2 )
by XXREAL_0:1;
suppose A68:
i1 = i2
;
P halts_on tA69:
i1 mod i2 =
i19 mod i29
.=
0
by A68, NAT_D:25
;
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 . (dl. 0)) 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 A65, Lm3;
hence
P halts_on t
by EXTPRO_1:16;
verum end; suppose A71:
i1 < i2
;
P halts_on tA72:
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 A71, NAT_D:24
;
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)) . (dl. 0) = 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 A76, EXTPRO_1:4;
hence
P halts_on t
by EXTPRO_1:16;
verum end; end;
end;
thus
(Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm
by A25, A63, EXTPRO_1:def 12; 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 A6, A5, EXTPRO_1:def 13;
dl. 0 in the carrier of SCM
;
then A78:
dl. 0 in dom (Result (T,t))
by PARTFUN1:def 2;
A79:
d . (dl. 0) = i1
by A4, AMI_3:10, FUNCT_4:63;
A80:
d . (dl. 1) = i2
by A4, FUNCT_4:63;
A81:
d c= (Start-At (0,SCM)) +* d
by FUNCT_4:25;
A82:
dom d c= dom ((Start-At (0,SCM)) +* d)
by A81, RELAT_1:11;
A83:
d c= t
by A81, A5;
A84:
dom d = {(dl. 0),(dl. 1)}
by A4, FUNCT_4:62;
then A85:
dl. 1 in dom d
by TARSKI:def 2;
A86:
t . (dl. 1) = i2
by A83, A80, A85, GRFUNC_1:2;
A87:
dl. 0 in dom d
by A84, TARSKI:def 2;
t . (dl. 0) = i1
by A83, A79, A87, GRFUNC_1:2;
then A88:
(Result (T,t)) . (dl. 0) = i1 gcd i2
by A2, A3, A24, A86, Th7, A6;
dom ((dl. 0) .--> (i1 gcd i2)) c= dom d
by A84, ZFMISC_1:7;
then A90:
dom ((dl. 0) .--> (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 A90, A78, A88, FUNCT_4:85, RELAT_1:151;
hence
Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d))
by A77, A2, A3, A4, Th9; verum