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

begin

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 m = j holds
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 = m1 + m2 holds
ICplusConst s,(- m2) = 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) . (card I) = i & 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) . (card I) = i

proof end;

begin

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 ;

begin

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 n in dom GCD-Algorithm ) by Th12, SCMPDS_4:1;

theorem Th14: :: SCMP_GCD:14

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

proof end;

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

proof end;

theorem Th15: :: SCMP_GCD:15

for s being State of SCMPDS st Initialized GCD-Algorithm c= s holds
( IC (Comput (ProgramPart s),s,4) = 5 & (Comput (ProgramPart s),s,4) . GBP = 0 & (Comput (ProgramPart s),s,4) . SBP = 7 & (Comput (ProgramPart s),s,4) . (intpos (7 + RetIC )) = 2 & (Comput (ProgramPart s),s,4) . (intpos 9) = s . (intpos 9) & (Comput (ProgramPart s),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 = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 holds
( IC (Comput (ProgramPart s),s,7) = 5 + 7 & Comput (ProgramPart s),s,8 = Exec (goto (- 7)),(Comput (ProgramPart s),s,7) & (Comput (ProgramPart s),s,7) . SBP = n + 4 & (Comput (ProgramPart s),s,7) . GBP = 0 & (Comput (ProgramPart s),s,7) . (intpos (n + 7)) = (s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3)) & (Comput (ProgramPart s),s,7) . (intpos (n + 6)) = s . (DataLoc (s . SBP ),3) & (Comput (ProgramPart s),s,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s),s,7) . (intpos (n + 5)) = 11 )

proof end;

Lm5: for n, m being Element of NAT
for s being State of SCMPDS st GCD-Algorithm c= s & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc (s . SBP ),3) > 0 & 1 < m & m <= n + 1 holds
(Comput (ProgramPart s),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 = 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 (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & s . SBP = (Comput (ProgramPart s),s,n) . SBP & (Comput (ProgramPart s),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) = (Comput (ProgramPart s),s,n) . (intpos j) ) )

proof end;

theorem Th17: :: SCMP_GCD:17

for s being State of SCMPDS st GCD-Algorithm c= s & IC s = 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 (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & s . SBP = (Comput (ProgramPart s),s,n) . SBP & (Comput (ProgramPart s),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) = (Comput (ProgramPart s),s,n) . (intpos j) ) )

proof end;

begin

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 = 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 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 = 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 (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a )

proof end;

Lm8: for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 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 (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),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 (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a )

proof end;

begin

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;