:: Recursive Euclide Algorithm
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users

theorem :: SCMP_GCD:1

canceled;

theorem :: SCMP_GCD:2

canceled;

theorem Th3: :: SCMP_GCD:3

for m being Element of NAT
for j being Integer st inspos m = j holds
inspos (m + 2) = (abs j) + 2

proof end;

definition

let k be Nat;
func intpos k -> Int_position equals :: SCMP_GCD:def 1
dl. k;
coherence
dl. k is Int_position

proof end;

end;

:: deftheorem defines intpos SCMP_GCD:def 1 :

for k being Nat holds intpos k = dl. k;

theorem :: SCMP_GCD:4

canceled;

theorem Th5: :: SCMP_GCD:5

for n1, n2 being Element of NAT holds DataLoc n1,n2 = intpos (n1 + n2)

proof end;

theorem Th6: :: SCMP_GCD:6

for s being State of SCMPDS
for m1, m2 being Element of NAT st IC s = inspos (m1 + m2) holds
ICplusConst s,(- m2) = inspos m1

proof end;

definition

func GBP -> Int_position equals :: SCMP_GCD:def 2
intpos 0 ;
coherence
intpos 0 is Int_position ;
func SBP -> Int_position equals :: SCMP_GCD:def 3
intpos 1;
coherence
intpos 1 is Int_position ;

end;

:: deftheorem defines GBP SCMP_GCD:def 2 :

GBP = intpos 0 ;

:: deftheorem defines SBP SCMP_GCD:def 3 :

SBP = intpos 1;

theorem :: SCMP_GCD:7

GBP <> SBP by AMI_3:52;

theorem Th8: :: SCMP_GCD:8

for i being Instruction of SCMPDS
for I being Program of SCMPDS holds card (I ';' i) = (card I) + 1

proof end;

theorem Th9: :: SCMP_GCD:9

for i, j being Instruction of SCMPDS holds card (i ';' j) = 2

proof end;

theorem Th10: :: SCMP_GCD:10

for i being Instruction of SCMPDS
for I being Program of SCMPDS holds
( (I ';' i) . (inspos (card I)) = i & inspos (card I) in dom (I ';' i) )

proof end;

theorem Th11: :: SCMP_GCD:11

for i being Instruction of SCMPDS
for I, J being Program of SCMPDS holds ((I ';' i) ';' J) . (inspos (card I)) = i

proof end;

definition

func GCD-Algorithm -> Program of SCMPDS equals :: SCMP_GCD:def 4
((((((((((((((GBP := 0 ) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) ';' (SBP ,3 <=0_goto 9)) ';' (SBP ,6 := SBP ,3)) ';' (Divide SBP ,2,SBP ,3)) ';' (SBP ,7 := SBP ,3)) ';' (SBP ,(4 + RetSP ) := GBP ,1)) ';' (AddTo GBP ,1,4)) ';' (saveIC SBP ,RetIC )) ';' (goto (- 7))) ';' (SBP ,2 := SBP ,6)) ';' (return SBP );
coherence
((((((((((((((GBP := 0 ) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) ';' (SBP ,3 <=0_goto 9)) ';' (SBP ,6 := SBP ,3)) ';' (Divide SBP ,2,SBP ,3)) ';' (SBP ,7 := SBP ,3)) ';' (SBP ,(4 + RetSP ) := GBP ,1)) ';' (AddTo GBP ,1,4)) ';' (saveIC SBP ,RetIC )) ';' (goto (- 7))) ';' (SBP ,2 := SBP ,6)) ';' (return SBP ) is Program of SCMPDS ;

end;

:: deftheorem defines GCD-Algorithm SCMP_GCD:def 4 :

GCD-Algorithm = ((((((((((((((GBP := 0 ) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) ';' (SBP ,3 <=0_goto 9)) ';' (SBP ,6 := SBP ,3)) ';' (Divide SBP ,2,SBP ,3)) ';' (SBP ,7 := SBP ,3)) ';' (SBP ,(4 + RetSP ) := GBP ,1)) ';' (AddTo GBP ,1,4)) ';' (saveIC SBP ,RetIC )) ';' (goto (- 7))) ';' (SBP ,2 := SBP ,6)) ';' (return SBP );

set i00 = GBP := 0 ;

set i01 = SBP := 7;

set i02 = saveIC SBP ,RetIC ;

set i03 = goto 2;

set i04 = halt SCMPDS ;

set i05 = SBP ,3 <=0_goto 9;

set i06 = SBP ,6 := SBP ,3;

set i07 = Divide SBP ,2,SBP ,3;

set i08 = SBP ,7 := SBP ,3;

set i09 = SBP ,(4 + RetSP ) := GBP ,1;

set i10 = AddTo GBP ,1,4;

set i11 = saveIC SBP ,RetIC ;

set i12 = goto (- 7);

set i13 = SBP ,2 := SBP ,6;

set i14 = return SBP ;


theorem Th12: :: SCMP_GCD:12

card GCD-Algorithm = 15

proof end;

theorem :: SCMP_GCD:13

for n being Element of NAT holds
( n < 15 iff inspos n in dom GCD-Algorithm ) by Th12, SCMPDS_4:1;

theorem Th14: :: SCMP_GCD:14

( GCD-Algorithm . (inspos 0 ) = GBP := 0 & GCD-Algorithm . (inspos 1) = SBP := 7 & GCD-Algorithm . (inspos 2) = saveIC SBP ,RetIC & GCD-Algorithm . (inspos 3) = goto 2 & GCD-Algorithm . (inspos 4) = halt SCMPDS & GCD-Algorithm . (inspos 5) = SBP ,3 <=0_goto 9 & GCD-Algorithm . (inspos 6) = SBP ,6 := SBP ,3 & GCD-Algorithm . (inspos 7) = Divide SBP ,2,SBP ,3 & GCD-Algorithm . (inspos 8) = SBP ,7 := SBP ,3 & GCD-Algorithm . (inspos 9) = SBP ,(4 + RetSP ) := GBP ,1 & GCD-Algorithm . (inspos 10) = AddTo GBP ,1,4 & GCD-Algorithm . (inspos 11) = saveIC SBP ,RetIC & GCD-Algorithm . (inspos 12) = goto (- 7) & GCD-Algorithm . (inspos 13) = SBP ,2 := SBP ,6 & GCD-Algorithm . (inspos 14) = return SBP )

proof end;

Lm1: for s being State of SCMPDS st GCD-Algorithm c= s holds
( s . (inspos 0 ) = GBP := 0 & s . (inspos 1) = SBP := 7 & s . (inspos 2) = saveIC SBP ,RetIC & s . (inspos 3) = goto 2 & s . (inspos 4) = halt SCMPDS & s . (inspos 5) = SBP ,3 <=0_goto 9 & s . (inspos 6) = SBP ,6 := SBP ,3 & s . (inspos 7) = Divide SBP ,2,SBP ,3 & s . (inspos 8) = SBP ,7 := SBP ,3 & s . (inspos 9) = SBP ,(4 + RetSP ) := GBP ,1 & s . (inspos 10) = AddTo GBP ,1,4 & s . (inspos 11) = saveIC SBP ,RetIC & s . (inspos 12) = goto (- 7) & s . (inspos 13) = SBP ,2 := SBP ,6 & s . (inspos 14) = return SBP )

proof end;

theorem Th15: :: SCMP_GCD:15

for s being State of SCMPDS st Initialized GCD-Algorithm c= s holds
( IC (Computation s,4) = inspos 5 & (Computation s,4) . GBP = 0 & (Computation s,4) . SBP = 7 & (Computation s,4) . (intpos (7 + RetIC )) = inspos 2 & (Computation s,4) . (intpos 9) = s . (intpos 9) & (Computation s,4) . (intpos 10) = s . (intpos 10) )

proof end;

Lm2: for n, m being Element of NAT st n > 0 holds
GBP <> intpos (m + n)

proof end;

Lm3: for n, m being Element of NAT st n > 1 holds
SBP <> intpos (m + n)

proof end;

Lm4: for n being Element of NAT
for s being State of SCMPDS st GCD-Algorithm c= s & IC s = inspos 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 holds
( IC (Computation s,7) = inspos (5 + 7) & Computation s,8 = Exec (goto (- 7)),(Computation s,7) & (Computation s,7) . SBP = n + 4 & (Computation s,7) . GBP = 0 & (Computation s,7) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) & (Computation s,7) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) & (Computation s,7) . (intpos (n + 4)) = n & (Computation s,7) . (intpos (n + 5)) = inspos 11 )

proof end;

Lm5: for n, m being Element of NAT
for s being State of SCMPDS st GCD-Algorithm c= s & IC s = inspos 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 & 1 < m & m <= n + 1 holds
(Computation s,7) . (intpos m) = s . (intpos m)

proof end;

theorem Th16: :: SCMP_GCD:16

for s being State of SCMPDS st GCD-Algorithm c= s & IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) holds
ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & s . SBP = (Computation s,n) . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )

proof end;

theorem Th17: :: SCMP_GCD:17

for s being State of SCMPDS st GCD-Algorithm c= s & IC s = inspos 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= 0 holds
ex n being Element of NAT st
( CurInstr (Computation s,n) = return SBP & s . SBP = (Computation s,n) . SBP & (Computation s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Computation s,n) . (intpos j) ) )

proof end;

theorem :: SCMP_GCD:18

for s being State of SCMPDS st Initialized GCD-Algorithm c= s holds
for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result s) . (intpos 9) = x gcd y

proof end;

Lm6: for n being Element of NAT
for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) holds
( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )

proof end;

Lm7: for n being Element of NAT
for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) holds
for k being Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )

proof end;

Lm8: for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) holds
ex n being Element of NAT st
( CurInstr (Computation s1,n) = return SBP & s1 . SBP = (Computation s1,n) . SBP & CurInstr (Computation s2,n) = return SBP & s2 . SBP = (Computation s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Computation s1,n) . (intpos j) & s2 . (intpos j) = (Computation s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) ) )

proof end;

Lm9: for s1, s2 being State of SCMPDS
for a being Int_position
for k being Element of NAT st Initialized GCD-Algorithm c= s1 & Initialized GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )

proof end;

theorem :: SCMP_GCD:19

for p being FinPartState of SCMPDS
for x, y being Integer st y >= 0 & x >= y & p = (intpos 9),(intpos 10) --> x,y holds
(Initialized GCD-Algorithm ) +* p is autonomic

proof end;