:: Recursive Euclid's Algorithm
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

definition

let k be Nat;

func intpos k -> Int_position equals :: SCMP_GCD:def 1
dl. k;

coherence
dl. k is Int_position by SCMPDS_2:def 1;

end;

:: deftheorem defines intpos SCMP_GCD:def 1 :
for k being Nat holds intpos k = dl. k;

theorem Th1: :: SCMP_GCD:1

for n1, n2 being Nat holds DataLoc (n1,n2) = intpos (n1 + n2)

proof end;

theorem Th2: :: SCMP_GCD:2

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

proof end;

:: GBP:Global Base Pointer

definition

func GBP -> Int_position equals :: SCMP_GCD:def 2
intpos 0;

coherence
intpos 0 is Int_position ;

:: SBP:Stack Base(bottom) Pointer

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:3

GBP <> SBP by AMI_3:10;

theorem Th4: :: SCMP_GCD:4

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

proof end;

theorem Th5: :: SCMP_GCD:5

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

proof end;

theorem Th6: :: SCMP_GCD:6

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 Th7: :: SCMP_GCD:7

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

proof end;

:: Greatest Common Divisor
:: gcd(x,y) < x=(SBP,2) y=(SBP,3) >
:: BEGIN
:: if y=0 then gcd:=x else
:: gcd:=gcd(y, x mod y)
:: END

definition

::Def04

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 Th8: :: SCMP_GCD:8

card GCD-Algorithm = 15

proof end;

theorem :: SCMP_GCD:9

for n being Nat holds
( n < 15 iff n in dom GCD-Algorithm ) by Th8, AFINSQ_1:66;

theorem Th10: :: SCMP_GCD:10

( 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 P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P holds
( P . 0 = GBP := 0 & P . 1 = SBP := 7 & P . 2 = saveIC (SBP,RetIC) & P . 3 = goto 2 & P . 4 = halt SCMPDS & P . 5 = (SBP,3) <=0_goto 9 & P . 6 = (SBP,6) := (SBP,3) & P . 7 = Divide (SBP,2,SBP,3) & P . 8 = (SBP,7) := (SBP,3) & P . 9 = (SBP,(4 + RetSP)) := (GBP,1) & P . 10 = AddTo (GBP,1,4) & P . 11 = saveIC (SBP,RetIC) & P . 12 = goto (- 7) & P . 13 = (SBP,2) := (SBP,6) & P . 14 = return SBP )
by Th8, AFINSQ_1:66, Th10, GRFUNC_1:2;

theorem Th11: :: SCMP_GCD:11

for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P holds
for s being 0 -started State of SCMPDS holds
( IC (Comput (P,s,4)) = 5 & (Comput (P,s,4)) . GBP = 0 & (Comput (P,s,4)) . SBP = 7 & (Comput (P,s,4)) . (intpos (7 + RetIC)) = 2 & (Comput (P,s,4)) . (intpos 9) = s . (intpos 9) & (Comput (P,s,4)) . (intpos 10) = s . (intpos 10) )

proof end;

Lm2: for m, n being Nat st n > 0 holds
GBP <> intpos (m + n)
by AMI_3:10;

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

proof end;

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

proof end;

Lm5: for m, n being Nat
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P & IC s = 5 & n = s . SBP & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) > 0 & 1 < m & m <= n + 1 holds
(Comput (P,s,7)) . (intpos m) = s . (intpos m)

proof end;

theorem Th12: :: SCMP_GCD:12

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS st GCD-Algorithm c= P & 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 Nat st
( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )

proof end;

theorem Th13: :: SCMP_GCD:13

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS st GCD-Algorithm c= P & 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 Nat st
( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )

proof end;

theorem :: SCMP_GCD:14

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

proof end;

Lm6: for n being Nat
for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & 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 (P1,s1,7)) = 5 + 7 & Comput (P1,s1,8) = Exec ((goto (- 7)),(Comput (P1,s1,7))) & (Comput (P1,s1,7)) . SBP = n + 4 & (Comput (P1,s1,7)) . GBP = 0 & (Comput (P1,s1,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (P1,s1,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (P2,s2,7)) = 5 + 7 & Comput (P2,s2,8) = Exec ((goto (- 7)),(Comput (P2,s2,7))) & (Comput (P2,s2,7)) . SBP = n + 4 & (Comput (P2,s2,7)) . GBP = 0 & (Comput (P2,s2,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (P2,s2,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (P1,s1,7)) . (intpos (n + 4)) = n & (Comput (P1,s1,7)) . (intpos (n + 5)) = 11 & (Comput (P2,s2,7)) . (intpos (n + 4)) = n & (Comput (P2,s2,7)) . (intpos (n + 5)) = 11 )

proof end;

Lm7: for n being Nat
for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & 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 Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )

proof end;

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

proof end;

Lm9: for P1, P2 being Instruction-Sequence of SCMPDS
for s1, s2 being State of SCMPDS
for a being Int_position
for k being Nat st Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & s1 . a = s2 . a & k <= 4 holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )

proof end;

theorem :: SCMP_GCD:15

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

proof end;