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 = 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
let s1, s2 be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) )
set GA = GCD-Algorithm ;
assume that
A1: GCD-Algorithm c= s1 and
A2: GCD-Algorithm c= s2 ; :: thesis: ( not IC s1 = 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) )
assume A3: IC s1 = 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) )
assume A4: 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) )
assume A5: 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) )
assume A6: 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) )
assume that
A7: IC s2 = IC s1 and
A8: s2 . SBP = s1 . SBP and
A9: 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 (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) )
assume that
A10: s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) and
A11: s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) ; :: thesis: ( IC (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 & (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
A12: DataLoc (s1 . SBP ),2 = intpos (n + 2) by A4, Th5;
A13: DataLoc (s1 . SBP ),3 = intpos (n + 3) by A4, Th5;
thus ( IC (Comput (ProgramPart s1),s1,7) = 5 + 7 & Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) & (Comput (ProgramPart s1),s1,7) . SBP = n + 4 & (Comput (ProgramPart s1),s1,7) . GBP = 0 ) by A1, A3, A4, A5, A6, Lm4; :: thesis: ( (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
thus (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A1, A3, A4, A5, A6, A12, A13, Lm4; :: thesis: ( (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
thus (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A1, A3, A4, A5, A6, A13, Lm4; :: thesis: ( IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
thus ( IC (Comput (ProgramPart s2),s2,7) = 5 + 7 & Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) & (Comput (ProgramPart s2),s2,7) . SBP = n + 4 & (Comput (ProgramPart s2),s2,7) . GBP = 0 ) by A2, A3, A4, A6, A7, A8, A9, A11, Lm4; :: thesis: ( (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) & (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
thus (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A2, A3, A4, A6, A7, A8, A9, A10, A11, A12, A13, Lm4; :: thesis: ( (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) & (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
thus (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A2, A3, A4, A6, A7, A8, A9, A11, A13, Lm4; :: thesis: ( (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 & (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
thus ( (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 ) by A1, A3, A4, A5, A6, Lm4; :: thesis: ( (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 )
thus ( (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n & (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 ) by A2, A3, A4, A6, A7, A8, A9, A11, Lm4; :: thesis: verum