let n be Element of NAT ; :: thesis: for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 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 (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
let s1, s2 be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 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) implies ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) )
set GA = GCD-Algorithm ;
assume A1: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 ) ; :: thesis: ( not IC s1 = inspos 5 or not n = s1 . SBP or not s1 . GBP = 0 or not s1 . (DataLoc (s1 . SBP ),3) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) )
assume A2: IC s1 = inspos 5 ; :: thesis: ( not n = s1 . SBP or not s1 . GBP = 0 or not s1 . (DataLoc (s1 . SBP ),3) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) )
assume A3: n = s1 . SBP ; :: thesis: ( not s1 . GBP = 0 or not s1 . (DataLoc (s1 . SBP ),3) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) )
assume A4: s1 . GBP = 0 ; :: thesis: ( not s1 . (DataLoc (s1 . SBP ),3) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) )
assume A5: s1 . (DataLoc (s1 . SBP ),3) > 0 ; :: thesis: ( not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) )
assume A6: ( IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 ) ; :: thesis: ( not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) )
assume A7: ( s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) ) ; :: thesis: ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 & (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
A8: DataLoc (s1 . SBP ),2 = intpos (n + 2) by A3, Th5;
A9: DataLoc (s1 . SBP ),3 = intpos (n + 3) by A3, Th5;
thus ( IC (Computation s1,7) = inspos (5 + 7) & Computation s1,8 = Exec (goto (- 7)),(Computation s1,7) & (Computation s1,7) . SBP = n + 4 & (Computation s1,7) . GBP = 0 ) by A1, A2, A3, A4, A5, Lm4; :: thesis: ( (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
thus (Computation s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A1, A2, A3, A4, A5, A8, A9, Lm4; :: thesis: ( (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
thus (Computation s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A1, A2, A3, A4, A5, A9, Lm4; :: thesis: ( IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 & (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
thus ( IC (Computation s2,7) = inspos (5 + 7) & Computation s2,8 = Exec (goto (- 7)),(Computation s2,7) & (Computation s2,7) . SBP = n + 4 & (Computation s2,7) . GBP = 0 ) by A1, A2, A3, A5, A6, A7, Lm4; :: thesis: ( (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
thus (Computation s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A1, A2, A3, A5, A6, A7, A8, A9, Lm4; :: thesis: ( (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
thus (Computation s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A1, A2, A3, A5, A6, A7, A9, Lm4; :: thesis: ( (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 & (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
thus ( (Computation s1,7) . (intpos (n + 4)) = n & (Computation s1,7) . (intpos (n + 5)) = inspos 11 ) by A1, A2, A3, A4, A5, Lm4; :: thesis: ( (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 )
thus ( (Computation s2,7) . (intpos (n + 4)) = n & (Computation s2,7) . (intpos (n + 5)) = inspos 11 ) by A1, A2, A3, A5, A6, A7, Lm4; :: thesis: verum