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