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