:: Recursive Euclid's Algorithm
:: by JingChao Chen
::
:: 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 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
coherence ;
:: SBP:Stack Base(bottom) Pointer
coherence ;
end;

:: deftheorem defines GBP SCMP_GCD:def 2 :

:: deftheorem defines SBP SCMP_GCD:def 3 :

theorem :: SCMP_GCD:3

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
(((((((((((((() ';' ()) ';' ()) ';' (goto 2)) ';' ()) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,()) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' ()) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) ';' ();
coherence
(((((((((((((() ';' ()) ';' ()) ';' (goto 2)) ';' ()) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,()) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' ()) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) ';' () is Program of SCMPDS
;
end;

:: deftheorem defines GCD-Algorithm SCMP_GCD:def 4 :
GCD-Algorithm = (((((((((((((() ';' ()) ';' ()) ';' (goto 2)) ';' ()) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,()) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' ()) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) ';' ();

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,()) := (GBP,1);

set i11 = saveIC (SBP,RetIC);

set i12 = goto (- 7);

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

set i14 = return SBP;

theorem Th8: :: SCMP_GCD:8
proof end;

theorem :: SCMP_GCD:9
for n being Nat holds
( n < 15 iff n in dom GCD-Algorithm ) by ;

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,()) := (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,()) := (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 ;

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 ()) = 2 & (Comput (P,s,4)) . () = s . () & (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)) . () = s . ()

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 . () = (Comput (P,s,n)) . () ) )
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 . () = (Comput (P,s,n)) . () ) )
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 . () = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result (P,s)) . () = 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 . () = (Comput (P1,s1,n)) . () & s2 . () = (Comput (P2,s2,n)) . () ) ) & ( 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 10)) --> (x,y) holds
Initialize p is GCD-Algorithm -autonomic
proof end;