let P be Instruction-Sequence of SCMPDS; ( GCD-Algorithm c= P implies ( 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 ) )
set GA = GCD-Algorithm ;
assume A1:
GCD-Algorithm c= P
; ( 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 )
0 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 0 = GBP := 0
by A1, Th14, GRFUNC_1:2; ( 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 )
1 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 1 = SBP := 7
by A1, Th14, GRFUNC_1:2; ( 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 )
2 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 2 = saveIC (SBP,RetIC)
by A1, Th14, GRFUNC_1:2; ( 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 )
3 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 3 = goto 2
by A1, Th14, GRFUNC_1: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 )
4 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 4 = halt SCMPDS
by A1, Th14, GRFUNC_1:2; ( 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 )
5 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 5 = (SBP,3) <=0_goto 9
by A1, Th14, GRFUNC_1:2; ( 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 )
6 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 6 = (SBP,6) := (SBP,3)
by A1, Th14, GRFUNC_1:2; ( 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 )
7 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 7 = Divide (SBP,2,SBP,3)
by A1, Th14, GRFUNC_1:2; ( 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 )
8 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 8 = (SBP,7) := (SBP,3)
by A1, Th14, GRFUNC_1:2; ( 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 )
9 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 9 = (SBP,(4 + RetSP)) := (GBP,1)
by A1, Th14, GRFUNC_1:2; ( 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 )
10 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 10 = AddTo (GBP,1,4)
by A1, Th14, GRFUNC_1:2; ( P . 11 = saveIC (SBP,RetIC) & P . 12 = goto (- 7) & P . 13 = (SBP,2) := (SBP,6) & P . 14 = return SBP )
11 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 11 = saveIC (SBP,RetIC)
by A1, Th14, GRFUNC_1:2; ( P . 12 = goto (- 7) & P . 13 = (SBP,2) := (SBP,6) & P . 14 = return SBP )
12 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 12 = goto (- 7)
by A1, Th14, GRFUNC_1:2; ( P . 13 = (SBP,2) := (SBP,6) & P . 14 = return SBP )
13 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 13 = (SBP,2) := (SBP,6)
by A1, Th14, GRFUNC_1:2; P . 14 = return SBP
14 in dom GCD-Algorithm
by Th12, AFINSQ_1:66;
hence
P . 14 = return SBP
by A1, Th14, GRFUNC_1:2; verum