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