let p be FinPartState of SCMPDS ; :: thesis: for x, y being Integer st y >= 0 & x >= y & p = (intpos 9),(intpos 10) --> x,y holds
(Initialized GCD-Algorithm ) +* p is autonomic
let x, y be Integer; :: thesis: ( y >= 0 & x >= y & p = (intpos 9),(intpos 10) --> x,y implies (Initialized GCD-Algorithm ) +* p is autonomic )
set GA = GCD-Algorithm ;
set IA = Initialized GCD-Algorithm ;
set a = intpos 9;
set b = intpos 10;
assume A1: ( y >= 0 & x >= y & p = (intpos 9),(intpos 10) --> x,y ) ; :: thesis: (Initialized GCD-Algorithm ) +* p is autonomic
then A2: dom p = {(intpos 9),(intpos 10)} by FUNCT_4:65;
A3: dom (Initialized GCD-Algorithm ) = {(IC SCMPDS )} \/ (dom GCD-Algorithm ) by SCMPDS_4:27;

now

assume dom (Initialized GCD-Algorithm ) meets dom p ; :: thesis: contradiction
then consider z being set such that
A4: ( z in dom (Initialized GCD-Algorithm ) & z in dom p ) by XBOOLE_0:3;
( z = intpos 9 or z = intpos 10 ) by A2, A4, TARSKI:def 2;
hence contradiction by A4, SCMPDS_4:31; :: thesis: verum

end;

then A5: Initialized GCD-Algorithm c= (Initialized GCD-Algorithm ) +* p by FUNCT_4:33;
A6: ( intpos 9 in dom p & intpos 10 in dom p ) by A2, TARSKI:def 2;
A7: for t being State of SCMPDS st (Initialized GCD-Algorithm ) +* p c= t holds
( t . (intpos 9) = x & t . (intpos 10) = y )

proof

let t be State of SCMPDS ; :: thesis: ( (Initialized GCD-Algorithm ) +* p c= t implies ( t . (intpos 9) = x & t . (intpos 10) = y ) )
assume A8: (Initialized GCD-Algorithm ) +* p c= t ; :: thesis: ( t . (intpos 9) = x & t . (intpos 10) = y )
p c= (Initialized GCD-Algorithm ) +* p by FUNCT_4:26;
then A9: p c= t by A8, XBOOLE_1:1;
A10: intpos 9 <> intpos 10 by AMI_3:52;
thus t . (intpos 9) = p . (intpos 9) by A6, A9, GRFUNC_1:8
.= x by A1, A10, FUNCT_4:66 ; :: thesis: t . (intpos 10) = y
thus t . (intpos 10) = p . (intpos 10) by A6, A9, GRFUNC_1:8
.= y by A1, FUNCT_4:66 ; :: thesis: verum

end;

thus (Initialized GCD-Algorithm ) +* p is autonomic :: thesis: verum

proof

let s1, s2 be State of SCMPDS ; :: according to AMI_1:def 25 :: thesis: ( not (Initialized GCD-Algorithm ) +* p c= s1 or not (Initialized GCD-Algorithm ) +* p c= s2 or for b₁ being Element of NAT holds (Computation s1,b₁) | (dom ((Initialized GCD-Algorithm ) +* p)) = (Computation s2,b₁) | (dom ((Initialized GCD-Algorithm ) +* p)) )
assume that
A11: (Initialized GCD-Algorithm ) +* p c= s1 and
A12: (Initialized GCD-Algorithm ) +* p c= s2 ; :: thesis: for b₁ being Element of NAT holds (Computation s1,b₁) | (dom ((Initialized GCD-Algorithm ) +* p)) = (Computation s2,b₁) | (dom ((Initialized GCD-Algorithm ) +* p))
A13: Initialized GCD-Algorithm c= s1 by A5, A11, XBOOLE_1:1;
then A14: GCD-Algorithm c= s1 by SCMPDS_4:57;
A15: Initialized GCD-Algorithm c= s2 by A5, A12, XBOOLE_1:1;
then A16: GCD-Algorithm c= s2 by SCMPDS_4:57;
A17: ( s1 . (intpos 9) = x & s1 . (intpos 10) = y ) by A7, A11;
A18: ( s2 . (intpos 9) = x & s2 . (intpos 10) = y ) by A7, A12;
set s4 = Computation s1,4;
set t4 = Computation s2,4;
A19: GCD-Algorithm c= Computation s1,4 by A13, AMI_1:81, SCMPDS_4:57;
A20: ( IC (Computation s1,4) = inspos 5 & (Computation s1,4) . GBP = 0 & (Computation s1,4) . SBP = 7 & (Computation s1,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s1,4) . (intpos 9) = s1 . (intpos 9) & (Computation s1,4) . (intpos 10) = s1 . (intpos 10) ) by A13, Th15;
then A21: (Computation s1,4) . (DataLoc ((Computation s1,4) . SBP ),3) = (Computation s1,4) . (intpos (7 + 3)) by Th5
.= y by A7, A11, A20 ;
A22: DataLoc ((Computation s1,4) . SBP ),2 = intpos (7 + 2) by A20, Th5;
then A23: (Computation s1,4) . (DataLoc ((Computation s1,4) . SBP ),2) = x by A7, A11, A20;
A24: GCD-Algorithm c= Computation s2,4 by A15, AMI_1:81, SCMPDS_4:57;
A25: ( IC (Computation s2,4) = inspos 5 & (Computation s2,4) . GBP = 0 & (Computation s2,4) . SBP = 7 & (Computation s2,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s2,4) . (intpos 9) = s2 . (intpos 9) & (Computation s2,4) . (intpos 10) = s2 . (intpos 10) ) by A15, Th15;
then A26: (Computation s2,4) . (DataLoc ((Computation s2,4) . SBP ),3) = (Computation s2,4) . (intpos (7 + 3)) by Th5
.= (Computation s1,4) . (DataLoc ((Computation s1,4) . SBP ),3) by A7, A12, A21, A25 ;
DataLoc ((Computation s2,4) . SBP ),2 = intpos (7 + 2) by A25, Th5;
then A27: (Computation s2,4) . (DataLoc ((Computation s2,4) . SBP ),2) = (Computation s1,4) . (DataLoc ((Computation s1,4) . SBP ),2) by A7, A12, A23, A25;
consider n being Element of NAT such that
A28: ( CurInstr (Computation (Computation s1,4),n) = return SBP & (Computation s1,4) . SBP = (Computation (Computation s1,4),n) . SBP & CurInstr (Computation (Computation s2,4),n) = return SBP & (Computation s2,4) . SBP = (Computation (Computation s2,4),n) . SBP & ( for j being Element of NAT st 1 < j & j <= ((Computation s1,4) . SBP ) + 1 holds
( (Computation s1,4) . (intpos j) = (Computation (Computation s1,4),n) . (intpos j) & (Computation s2,4) . (intpos j) = (Computation (Computation s2,4),n) . (intpos j) ) ) & ( for k being Element of NAT
for c being Int_position st k <= n & (Computation s1,4) . c = (Computation s2,4) . c holds
( IC (Computation (Computation s1,4),k) = IC (Computation (Computation s2,4),k) & (Computation (Computation s1,4),k) . c = (Computation (Computation s2,4),k) . c ) ) ) by A1, A17, A19, A20, A21, A22, A24, A25, A26, A27, Lm8;
A29: (Computation (Computation s1,4),n) . (DataLoc ((Computation (Computation s1,4),n) . SBP ),RetIC ) = (Computation (Computation s1,4),n) . (intpos (7 + 1)) by A20, A28, Th5, SCMPDS_1:def 23
.= inspos 2 by A20, A28, SCMPDS_1:def 23 ;
A30: (Computation (Computation s2,4),n) . (DataLoc ((Computation (Computation s2,4),n) . SBP ),RetIC ) = (Computation (Computation s2,4),n) . (intpos (7 + 1)) by A25, A28, Th5, SCMPDS_1:def 23
.= inspos 2 by A20, A25, A28, SCMPDS_1:def 23 ;
A31: Computation (Computation s1,4),(n + 1) = Following (Computation (Computation s1,4),n) by AMI_1:14
.= Exec (return SBP ),(Computation (Computation s1,4),n) by A28 ;
then A32: IC (Computation (Computation s1,4),(n + 1)) = (abs ((Computation (Computation s1,4),n) . (DataLoc ((Computation (Computation s1,4),n) . SBP ),RetIC ))) + 2 by SCMPDS_2:70
.= inspos (2 + 2) by A29, Th3 ;
then A33: CurInstr (Computation (Computation s1,4),(n + 1)) = (Computation s1,4) . (inspos 4) by AMI_1:54
.= s1 . (inspos 4) by AMI_1:54
.= halt SCMPDS by A14, Lm1 ;
A34: Computation (Computation s2,4),(n + 1) = Following (Computation (Computation s2,4),n) by AMI_1:14
.= Exec (return SBP ),(Computation (Computation s2,4),n) by A28 ;
then A35: IC (Computation (Computation s2,4),(n + 1)) = (abs ((Computation (Computation s2,4),n) . (DataLoc ((Computation (Computation s2,4),n) . SBP ),RetIC ))) + 2 by SCMPDS_2:70
.= inspos (2 + 2) by A30, Th3 ;
then A36: CurInstr (Computation (Computation s2,4),(n + 1)) = (Computation s2,4) . (inspos 4) by AMI_1:54
.= s2 . (inspos 4) by AMI_1:54
.= halt SCMPDS by A16, Lm1 ;
A37: (Computation s1,4) . (intpos 9) = (Computation s2,4) . (intpos 9) by A13, A15, A17, A18, Lm9;
A38: (Computation s1,4) . (intpos 10) = (Computation s2,4) . (intpos 10) by A13, A15, A17, A18, Lm9;
A39: intpos 9 <> SBP by AMI_3:52;
then A40: (Computation (Computation s1,4),(n + 1)) . (intpos 9) = (Computation (Computation s1,4),n) . (intpos 9) by A31, SCMPDS_2:70
.= (Computation (Computation s2,4),n) . (intpos 9) by A28, A37
.= (Computation (Computation s2,4),(n + 1)) . (intpos 9) by A34, A39, SCMPDS_2:70 ;
A41: intpos 10 <> SBP by AMI_3:52;
then A42: (Computation (Computation s1,4),(n + 1)) . (intpos 10) = (Computation (Computation s1,4),n) . (intpos 10) by A31, SCMPDS_2:70
.= (Computation (Computation s2,4),n) . (intpos 10) by A28, A38
.= (Computation (Computation s2,4),(n + 1)) . (intpos 10) by A34, A41, SCMPDS_2:70 ;

A43: now

let j be Element of NAT ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . (intpos 9) = (Computation s2,b₁) . (intpos 9) & (Computation s1,b₁) . (intpos 10) = (Computation s2,b₁) . (intpos 10) )
A44: ( j < (n + 4) + 1 or j >= n + 5 ) ;

A45: now

assume A46: j <= n + 4 ; :: thesis: ( ( j <= 3 & j <= 3 ) or ( j >= 4 & j >= 4 & j <= n + 4 ) )
A47: ( j < 3 + 1 or j >= 4 ) ;

per cases ( j <= 3 or j >= 4 ) by A47, NAT_1:13;

case j <= 3 ; :: thesis: j <= 3

hence j <= 3 ; :: thesis: verum

end;

case j >= 4 ; :: thesis: ( j >= 4 & j <= n + 4 )

hence ( j >= 4 & j <= n + 4 ) by A46; :: thesis: verum

end;

end;

end;

per cases ( j <= 3 or ( j >= 4 & j <= n + 4 ) or j >= n + 5 ) by A44, A45, NAT_1:13;

suppose j <= 3 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . (intpos 9) = (Computation s2,b₁) . (intpos 9) & (Computation s1,b₁) . (intpos 10) = (Computation s2,b₁) . (intpos 10) )

then A48: j <= 4 by XXREAL_0:2;
hence IC (Computation s1,j) = IC (Computation s2,j) by A13, A15, A17, A18, Lm9; :: thesis: ( (Computation s1,j) . (intpos 9) = (Computation s2,j) . (intpos 9) & (Computation s1,j) . (intpos 10) = (Computation s2,j) . (intpos 10) )
thus (Computation s1,j) . (intpos 9) = (Computation s2,j) . (intpos 9) by A13, A15, A17, A18, A48, Lm9; :: thesis: (Computation s1,j) . (intpos 10) = (Computation s2,j) . (intpos 10)
thus (Computation s1,j) . (intpos 10) = (Computation s2,j) . (intpos 10) by A13, A15, A17, A18, A48, Lm9; :: thesis: verum

end;

suppose A49: ( j >= 4 & j <= n + 4 ) ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . (intpos 9) = (Computation s2,b₁) . (intpos 9) & (Computation s1,b₁) . (intpos 10) = (Computation s2,b₁) . (intpos 10) )

then consider j1 being Nat such that
A50: j = 4 + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
A51: j1 <= n by A49, A50, XREAL_1:8;
thus IC (Computation s1,j) = IC (Computation (Computation s1,4),j1) by A50, AMI_1:51
.= IC (Computation (Computation s2,4),j1) by A28, A37, A51
.= IC (Computation s2,j) by A50, AMI_1:51 ; :: thesis: ( (Computation s1,j) . (intpos 9) = (Computation s2,j) . (intpos 9) & (Computation s1,j) . (intpos 10) = (Computation s2,j) . (intpos 10) )
thus (Computation s1,j) . (intpos 9) = (Computation (Computation s1,4),j1) . (intpos 9) by A50, AMI_1:51
.= (Computation (Computation s2,4),j1) . (intpos 9) by A28, A37, A51
.= (Computation s2,j) . (intpos 9) by A50, AMI_1:51 ; :: thesis: (Computation s1,j) . (intpos 10) = (Computation s2,j) . (intpos 10)
thus (Computation s1,j) . (intpos 10) = (Computation (Computation s1,4),j1) . (intpos 10) by A50, AMI_1:51
.= (Computation (Computation s2,4),j1) . (intpos 10) by A28, A38, A51
.= (Computation s2,j) . (intpos 10) by A50, AMI_1:51 ; :: thesis: verum

end;

suppose j >= n + 5 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . (intpos 9) = (Computation s2,b₁) . (intpos 9) & (Computation s1,b₁) . (intpos 10) = (Computation s2,b₁) . (intpos 10) )

then consider j1 being Nat such that
A52: j = (n + (1 + 4)) + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
A53: j = ((n + 1) + j1) + 4 by A52;
hence IC (Computation s1,j) = IC (Computation (Computation s1,4),((n + 1) + j1)) by AMI_1:51
.= IC (Computation (Computation s2,4),(n + 1)) by A32, A33, A35, AMI_1:52, NAT_1:11
.= IC (Computation (Computation s2,4),((n + 1) + j1)) by A36, AMI_1:52, NAT_1:11
.= IC (Computation s2,j) by A53, AMI_1:51 ;
:: thesis: ( (Computation s1,j) . (intpos 9) = (Computation s2,j) . (intpos 9) & (Computation s1,j) . (intpos 10) = (Computation s2,j) . (intpos 10) )
thus (Computation s1,j) . (intpos 9) = (Computation (Computation s1,4),((n + 1) + j1)) . (intpos 9) by A53, AMI_1:51
.= (Computation (Computation s2,4),(n + 1)) . (intpos 9) by A33, A40, AMI_1:52, NAT_1:11
.= (Computation (Computation s2,4),((n + 1) + j1)) . (intpos 9) by A36, AMI_1:52, NAT_1:11
.= (Computation s2,j) . (intpos 9) by A53, AMI_1:51 ; :: thesis: (Computation s1,j) . (intpos 10) = (Computation s2,j) . (intpos 10)
thus (Computation s1,j) . (intpos 10) = (Computation (Computation s1,4),((n + 1) + j1)) . (intpos 10) by A53, AMI_1:51
.= (Computation (Computation s2,4),(n + 1)) . (intpos 10) by A33, A42, AMI_1:52, NAT_1:11
.= (Computation (Computation s2,4),((n + 1) + j1)) . (intpos 10) by A36, AMI_1:52, NAT_1:11
.= (Computation s2,j) . (intpos 10) by A53, AMI_1:51 ; :: thesis: verum

end;

end;

end;

set A = {(IC SCMPDS ),(intpos 9),(intpos 10)};
A54: dom ((Initialized GCD-Algorithm ) +* p) = ({(IC SCMPDS )} \/ (dom GCD-Algorithm )) \/ {(intpos 9),(intpos 10)} by A2, A3, FUNCT_4:def 1
.= ({(IC SCMPDS )} \/ {(intpos 9),(intpos 10)}) \/ (dom GCD-Algorithm ) by XBOOLE_1:4
.= {(IC SCMPDS ),(intpos 9),(intpos 10)} \/ (dom GCD-Algorithm ) by ENUMSET1:42 ;
let k be Element of NAT ; :: thesis: (Computation s1,k) | (dom ((Initialized GCD-Algorithm ) +* p)) = (Computation s2,k) | (dom ((Initialized GCD-Algorithm ) +* p))
A55: GCD-Algorithm c= Computation s2,k by A16, AMI_1:86;
GCD-Algorithm c= Computation s1,k by A14, AMI_1:86;
then A56: (Computation s1,k) | (dom GCD-Algorithm ) = GCD-Algorithm by GRFUNC_1:64
.= (Computation s2,k) | (dom GCD-Algorithm ) by A55, GRFUNC_1:64 ;
A57: (Computation s1,k) . (IC SCMPDS ) = IC (Computation s1,k)
.= IC (Computation s2,k) by A43
.= (Computation s2,k) . (IC SCMPDS ) ;
A58: ( (Computation s1,k) . (intpos 9) = (Computation s2,k) . (intpos 9) & (Computation s1,k) . (intpos 10) = (Computation s2,k) . (intpos 10) ) by A43;
dom (Computation s1,k) = the carrier of SCMPDS by AMI_1:79
.= dom (Computation s2,k) by AMI_1:79 ;
then (Computation s1,k) | {(IC SCMPDS ),(intpos 9),(intpos 10)} = (Computation s2,k) | {(IC SCMPDS ),(intpos 9),(intpos 10)} by A57, A58, GRFUNC_1:92;
hence (Computation s1,k) | (dom ((Initialized GCD-Algorithm ) +* p)) = (Computation s2,k) | (dom ((Initialized GCD-Algorithm ) +* p)) by A54, A56, RELAT_1:185; :: thesis: verum

end;