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