:: Justifying the Correctness of Fibonacci Sequence and Euclide Algorithm by Loop Invariant :: by JingChao Chen :: :: Received June 14, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin theorem Th5: :: SCPINVAR:1 for i, j being Instruction of SCMPDS for I being Program of SCMPDS holds ( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j ) proofend; theorem Th6: :: SCPINVAR:2 for a, b being Int_position ex f being Function of (product (the_Values_of SCMPDS)),NAT st for s being State of SCMPDS holds ( ( s . a = s . b implies f . s = 0 ) & ( s . a <> s . b implies f . s = max ((abs (s . a)),(abs (s . b))) ) ) proofend; theorem Th7: :: SCPINVAR:3 for a being Int_position ex f being Function of (product (the_Values_of SCMPDS)),NAT st for s being State of SCMPDS holds ( ( s . a >= 0 implies f . s = 0 ) & ( s . a < 0 implies f . s = - (s . a) ) ) proofend; set A = NAT ; set D = SCM-Data-Loc ; begin scheme :: SCPINVAR:sch 1 WhileLEnd{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } : ( F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),F3(),F2())))) = 0 & P1[ Initialize (IExec ((while<0 (F5(),F6(),F4())),F3(),F2()))] ) provided A2: for t being 0 -started State of SCMPDS st P1[t] holds ( F1(t) = 0 iff t . (DataLoc ((F2() . F5()),F6())) >= 0 ) and A3: P1[F2()] and A4: for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) < 0 holds ( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] ) proofend; set a1 = intpos 1; set a2 = intpos 2; set a3 = intpos 3; begin :: sum=Sum=x1+x2+...+xn definition let n, p0 be Element of NAT ; func sum (n,p0) -> Program of SCMPDS equals :: SCPINVAR:def 1 ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))) ';' (while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))); coherence ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))) ';' (while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))) is Program of SCMPDS ; end; :: deftheorem defines sum SCPINVAR:def_1_:_ for n, p0 being Element of NAT holds sum (n,p0) = ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- n))) ';' ((intpos 3) := (p0 + 1))) ';' (while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))); definition let ff be Function of (product (the_Values_of SCMPDS)),NAT; let s be State of SCMPDS; :: original:. redefine funcff . s -> Element of NAT ; coherence ff . s is Element of NAT by ORDINAL1:def_12; end; theorem Th8: :: SCPINVAR:4 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free shiftable Program of SCMPDS for a, b, c being Int_position for n, i, p0 being Element of NAT for f being FinSequence of INT st f is_FinSequence_on s,p0 & len f = n & s . b = 0 & s . a = 0 & s . (intpos i) = - n & s . c = p0 + 1 & ( for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st ex g being FinSequence of INT st ( g is_FinSequence_on s,p0 & len g = (t . (intpos i)) + n & t . b = Sum g & t . c = (p0 + 1) + (len g) ) & t . a = 0 & t . (intpos i) < 0 & ( for i being Element of NAT st i > p0 holds t . (intpos i) = s . (intpos i) ) holds ( (IExec (I,Q,t)) . a = 0 & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) + 1 & ex g being FinSequence of INT st ( g is_FinSequence_on s,p0 & len g = ((t . (intpos i)) + n) + 1 & (IExec (I,Q,t)) . c = (p0 + 1) + (len g) & (IExec (I,Q,t)) . b = Sum g ) & ( for i being Element of NAT st i > p0 holds (IExec (I,Q,t)) . (intpos i) = s . (intpos i) ) ) ) holds ( (IExec ((while<0 (a,i,I)),P,s)) . b = Sum f & while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P ) proofend; set j1 = AddTo (GBP,1,(intpos 3),0); set j2 = AddTo (GBP,2,1); set j3 = AddTo (GBP,3,1); set WB = ((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)); set WH = while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))); Lm1: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for m being Element of NAT st s . GBP = 0 & s . (intpos 3) = m holds ( (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP = 0 & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = (s . (intpos 1)) + (s . (intpos m)) & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = (s . (intpos 2)) + 1 & (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = m + 1 & ( for i being Element of NAT st i > 3 holds (IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) ) proofend; Lm3: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for n, p0 being Element of NAT for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n & s . (intpos 1) = 0 & s . GBP = 0 & s . (intpos 2) = - n & s . (intpos 3) = p0 + 1 holds ( (IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),P,(Initialize s))) . (intpos 1) = Sum f & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_closed_on s,P & while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is_halting_on s,P ) proofend; Lm4: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for n, p0 being Element of NAT for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds ( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is_halting_on s,P ) proofend; theorem :: SCPINVAR:5 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for n, p0 being Element of NAT for f being FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f = n holds ( (IExec ((sum (n,p0)),P,s)) . (intpos 1) = Sum f & sum (n,p0) is parahalting ) proofend; begin scheme :: SCPINVAR:sch 2 WhileGEnd{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } : ( F1((Initialize (IExec ((while>0 (F5(),F6(),F4())),F3(),F2())))) = 0 & P1[ Initialize (IExec ((while>0 (F5(),F6(),F4())),F3(),F2()))] ) provided A2: for t being 0 -started State of SCMPDS st P1[t] holds ( F1(t) = 0 iff t . (DataLoc ((F2() . F5()),F6())) <= 0 ) and A3: P1[F2()] and A4: for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) > 0 holds ( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] ) proofend; begin definition let n be Element of NAT ; func Fib-macro n -> Program of SCMPDS equals :: SCPINVAR:def 2 ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)) ';' (while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))); coherence ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)) ';' (while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))) is Program of SCMPDS ; end; :: deftheorem defines Fib-macro SCPINVAR:def_2_:_ for n being Element of NAT holds Fib-macro n = ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)) ';' (while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))); theorem Th10: :: SCPINVAR:6 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free shiftable Program of SCMPDS for a, f0, f1 being Int_position for n, i being Element of NAT st s . a = 0 & s . f0 = 0 & s . f1 = 1 & s . (intpos i) = n & ( for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS for k being Element of NAT st n = (t . (intpos i)) + k & t . f0 = Fib k & t . f1 = Fib (k + 1) & t . a = 0 & t . (intpos i) > 0 holds ( (IExec (I,Q,t)) . a = 0 & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (intpos i) = (t . (intpos i)) - 1 & (IExec (I,Q,t)) . f0 = Fib (k + 1) & (IExec (I,Q,t)) . f1 = Fib ((k + 1) + 1) ) ) holds ( (IExec ((while>0 (a,i,I)),P,s)) . f0 = Fib n & (IExec ((while>0 (a,i,I)),P,s)) . f1 = Fib (n + 1) & while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) proofend; set j1 = (GBP,4) := (GBP,2); set j2 = AddTo (GBP,2,GBP,1); set j3 = (GBP,1) := (GBP,4); set j4 = AddTo (GBP,3,(- 1)); set WB = ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))); set WH = while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))); Lm5: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS st s . GBP = 0 holds ( (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . GBP = 0 & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 1) = s . (intpos 2) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 2) = (s . (intpos 1)) + (s . (intpos 2)) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),P,s)) . (intpos 3) = (s . (intpos 3)) - 1 ) proofend; Lm7: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for n being Element of NAT st s . GBP = 0 & s . (intpos 1) = 0 & s . (intpos 2) = 1 & s . (intpos 3) = n holds ( (IExec ((while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))),P,s)) . (intpos 1) = Fib n & (IExec ((while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))),P,s)) . (intpos 2) = Fib (n + 1) & while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))) is_closed_on s,P & while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))) is_halting_on s,P ) proofend; Lm8: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for n being Element of NAT holds ( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s,P ) proofend; theorem :: SCPINVAR:7 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for n being Element of NAT holds ( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is parahalting ) proofend; begin :: while (a,i)<>0 do I definition let a be Int_position; let i be Integer; let I be Program of SCMPDS; func while<>0 (a,i,I) -> Program of SCMPDS equals :: SCPINVAR:def 3 ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (goto (- ((card I) + 2))); coherence ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (goto (- ((card I) + 2))) is Program of SCMPDS ; end; :: deftheorem defines while<>0 SCPINVAR:def_3_:_ for a being Int_position for i being Integer for I being Program of SCMPDS holds while<>0 (a,i,I) = ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (goto (- ((card I) + 2))); begin theorem Th12: :: SCPINVAR:8 for a being Int_position for i being Integer for I being Program of SCMPDS holds card (while<>0 (a,i,I)) = (card I) + 3 proofend; Lm9: for a being Int_position for i being Integer for I being Program of SCMPDS holds card (stop (while<>0 (a,i,I))) = (card I) + 4 proofend; theorem Th13: :: SCPINVAR:9 for a being Int_position for i being Integer for m being Element of NAT for I being Program of SCMPDS holds ( m < (card I) + 3 iff m in dom (while<>0 (a,i,I)) ) proofend; theorem Th14: :: SCPINVAR:10 for a being Int_position for i being Integer for I being Program of SCMPDS holds ( 0 in dom (while<>0 (a,i,I)) & 1 in dom (while<>0 (a,i,I)) ) proofend; theorem Th15: :: SCPINVAR:11 for a being Int_position for i being Integer for I being Program of SCMPDS holds ( (while<>0 (a,i,I)) . 0 = (a,i) <>0_goto 2 & (while<>0 (a,i,I)) . 1 = goto ((card I) + 2) & (while<>0 (a,i,I)) . ((card I) + 2) = goto (- ((card I) + 2)) ) proofend; Lm10: for a being Int_position for i being Integer for I being Program of SCMPDS holds while<>0 (a,i,I) = ((a,i) <>0_goto 2) ';' (((goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 2)))) proofend; theorem Th16: :: SCPINVAR:12 for P being Instruction-Sequence of SCMPDS for s being State of SCMPDS for I being Program of SCMPDS for a being Int_position for i being Integer st s . (DataLoc ((s . a),i)) = 0 holds ( while<>0 (a,i,I) is_closed_on s,P & while<>0 (a,i,I) is_halting_on s,P ) proofend; theorem Th17: :: SCPINVAR:13 for P being Instruction-Sequence of SCMPDS for s being State of SCMPDS for I being Program of SCMPDS for a, c being Int_position for i being Integer st s . (DataLoc ((s . a),i)) = 0 holds IExec ((while<>0 (a,i,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 3),SCMPDS)) proofend; theorem :: SCPINVAR:14 for P being Instruction-Sequence of SCMPDS for s being State of SCMPDS for I being Program of SCMPDS for a being Int_position for i being Integer st s . (DataLoc ((s . a),i)) = 0 holds IC (IExec ((while<>0 (a,i,I)),P,(Initialize s))) = (card I) + 3 proofend; theorem Th19: :: SCPINVAR:15 for P being Instruction-Sequence of SCMPDS for s being State of SCMPDS for I being Program of SCMPDS for a, b being Int_position for i being Integer st s . (DataLoc ((s . a),i)) = 0 holds (IExec ((while<>0 (a,i,I)),P,(Initialize s))) . b = s . b proofend; Lm11: for I being Program of SCMPDS for a being Int_position for i being Integer holds Shift (I,2) c= while<>0 (a,i,I) proofend; registration let I be shiftable Program of SCMPDS; let a be Int_position; let i be Integer; cluster while<>0 (a,i,I) -> shiftable ; correctness coherence while<>0 (a,i,I) is shiftable ; proofend; end; registration let I be halt-free Program of SCMPDS; let a be Int_position; let i be Integer; cluster while<>0 (a,i,I) -> halt-free ; correctness coherence while<>0 (a,i,I) is halt-free ; proofend; end; begin scheme :: SCPINVAR:sch 3 WhileNHalt{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } : ( while<>0 (F5(),F6(),F4()) is_closed_on F2(),F3() & while<>0 (F5(),F6(),F4()) is_halting_on F2(),F3() ) provided A2: for t being 0 -started State of SCMPDS st P1[t] & F1(t) = 0 holds t . (DataLoc ((F2() . F5()),F6())) = 0 and A3: P1[F2()] and A4: for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) <> 0 holds ( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] ) proofend; scheme :: SCPINVAR:sch 4 WhileNExec{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } : IExec ((while<>0 (F5(),F6(),F4())),F3(),F2()) = IExec ((while<>0 (F5(),F6(),F4())),F3(),(Initialize (IExec (F4(),F3(),F2())))) provided A2: F2() . (DataLoc ((F2() . F5()),F6())) <> 0 and A3: for t being 0 -started State of SCMPDS st P1[t] & F1(t) = 0 holds t . (DataLoc ((F2() . F5()),F6())) = 0 and A4: P1[F2()] and A5: for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) <> 0 holds ( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] ) proofend; scheme :: SCPINVAR:sch 5 WhileNEnd{ F1( State of SCMPDS) -> Element of NAT , F2() -> 0 -started State of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> halt-free shiftable Program of SCMPDS, F5() -> Int_position, F6() -> Integer, P1[ set ] } : ( F1((Initialize (IExec ((while<>0 (F5(),F6(),F4())),F3(),F2())))) = 0 & P1[ Initialize (IExec ((while<>0 (F5(),F6(),F4())),F3(),F2()))] ) provided A2: for t being 0 -started State of SCMPDS st P1[t] holds ( F1(t) = 0 iff t . (DataLoc ((F2() . F5()),F6())) = 0 ) and A3: P1[F2()] and A4: for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) <> 0 holds ( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & F1((Initialize (IExec (F4(),Q,t)))) < F1(t) & P1[ Initialize (IExec (F4(),Q,t))] ) proofend; theorem Th20: :: SCPINVAR:16 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free shiftable Program of SCMPDS for a, b, c being Int_position for i, d being Integer st card I > 0 & s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc (d,i)) = (t . b) - (t . c) & t . b <> t . c holds ( (IExec (I,Q,t)) . a = d & I is_closed_on t,Q & I is_halting_on t,Q & ( t . b > t . c implies ( (IExec (I,Q,t)) . b = (t . b) - (t . c) & (IExec (I,Q,t)) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec (I,Q,t)) . c = (t . c) - (t . b) & (IExec (I,Q,t)) . b = t . b ) ) & (IExec (I,Q,t)) . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) ) ) holds ( while<>0 (a,i,I) is_closed_on s,P & while<>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) <> 0 implies IExec ((while<>0 (a,i,I)),P,s) = IExec ((while<>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) ) proofend; begin :: by loop-invariant :: gcd(x,y) < x=(GBP,1) y=(GBP,2),(GBP,3)=x-y > :: while x<>y do :: if x>y then x=x-y else y=y-x definition func GCD-Algorithm -> Program of SCMPDS equals :: SCPINVAR:def 4 (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))); coherence (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))) is Program of SCMPDS ; end; :: deftheorem defines GCD-Algorithm SCPINVAR:def_4_:_ GCD-Algorithm = (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))); theorem Th21: :: SCPINVAR:17 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free shiftable Program of SCMPDS for a, b, c being Int_position for i, d being Integer st s . a = d & s . b > 0 & s . c > 0 & s . (DataLoc (d,i)) = (s . b) - (s . c) & ( for t being 0 -started State of SCMPDS for Q being Instruction-Sequence of SCMPDS st t . b > 0 & t . c > 0 & t . a = d & t . (DataLoc (d,i)) = (t . b) - (t . c) & t . b <> t . c holds ( (IExec (I,Q,t)) . a = d & I is_closed_on t,Q & I is_halting_on t,Q & ( t . b > t . c implies ( (IExec (I,Q,t)) . b = (t . b) - (t . c) & (IExec (I,Q,t)) . c = t . c ) ) & ( t . b <= t . c implies ( (IExec (I,Q,t)) . c = (t . c) - (t . b) & (IExec (I,Q,t)) . b = t . b ) ) & (IExec (I,Q,t)) . (DataLoc (d,i)) = ((IExec (I,Q,t)) . b) - ((IExec (I,Q,t)) . c) ) ) holds ( (IExec ((while<>0 (a,i,I)),P,s)) . b = (s . b) gcd (s . c) & (IExec ((while<>0 (a,i,I)),P,s)) . c = (s . b) gcd (s . c) ) proofend; set i1 = GBP := 0; set i2 = (GBP,3) := (GBP,1); set i3 = SubFrom (GBP,3,GBP,2); set j1 = Load (SubFrom (GBP,1,GBP,2)); set j2 = Load (SubFrom (GBP,2,GBP,1)); set IF = if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1)))); set k1 = (GBP,3) := (GBP,1); set k2 = SubFrom (GBP,3,GBP,2); set WB = ((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2)); set WH = while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2)))); Lm12: card (((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) = 6 proofend; Lm13: card (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))) = 9 proofend; theorem :: SCPINVAR:18 card GCD-Algorithm = 12 proofend; Lm14: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS st s . GBP = 0 holds ( ( s . (intpos 3) > 0 implies ( (IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1) = (s . (intpos 1)) - (s . (intpos 2)) & (IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2) = s . (intpos 2) ) ) & ( s . (intpos 3) <= 0 implies ( (IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2) = (s . (intpos 2)) - (s . (intpos 1)) & (IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1) = s . (intpos 1) ) ) & (IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . GBP = 0 & (IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 3) = ((IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 1)) - ((IExec ((((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))),P,s)) . (intpos 2)) ) proofend; Lm15: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS st s . GBP = 0 & s . (intpos 1) > 0 & s . (intpos 2) > 0 & s . (intpos 3) = (s . (intpos 1)) - (s . (intpos 2)) holds ( (IExec ((while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))),P,s)) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) & (IExec ((while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))),P,s)) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) & while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2)))) is_closed_on s,P & while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2)))) is_halting_on s,P ) proofend; set GA = (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))); Lm16: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS st s . (intpos 1) > 0 & s . (intpos 2) > 0 holds ( (IExec (((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2)))))),P,s)) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) & (IExec (((((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2)))))),P,s)) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) & (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))) is_closed_on s,P & (((GBP := 0) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) ';' (while<>0 (GBP,3,(((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))))) is_halting_on s,P ) proofend; theorem :: SCPINVAR:19 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for x, y being Integer st s . (intpos 1) = x & s . (intpos 2) = y & x > 0 & y > 0 holds ( (IExec (GCD-Algorithm,P,s)) . (intpos 1) = x gcd y & (IExec (GCD-Algorithm,P,s)) . (intpos 2) = x gcd y & GCD-Algorithm is_closed_on s,P & GCD-Algorithm is_halting_on s,P ) by Lm16;