let P be Instruction-Sequence of SCMPDS; for s being State of SCMPDS st GCD-Algorithm c= P & IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= 0 holds
ex n being Nat st
( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )
let s be State of SCMPDS; ( GCD-Algorithm c= P & IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= 0 implies ex n being Nat st
( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) ) )
set GA = GCD-Algorithm ;
set x = s . (DataLoc ((s . SBP),2));
set y = s . (DataLoc ((s . SBP),3));
set yy = s . (DataLoc ((s . SBP),3));
assume that
A1:
GCD-Algorithm c= P
and
A2:
IC s = 5
and
A3:
s . SBP > 0
and
A4:
s . GBP = 0
and
A5:
s . (DataLoc ((s . SBP),3)) >= 0
and
A6:
s . (DataLoc ((s . SBP),2)) >= 0
; ex n being Nat st
( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )
per cases
( s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) or s . (DataLoc ((s . SBP),2)) < s . (DataLoc ((s . SBP),3)) )
;
suppose
s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3))
;
ex n being Nat st
( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )hence
ex
n being
Nat st
(
CurInstr (
P,
(Comput (P,s,n)))
= return SBP &
s . SBP = (Comput (P,s,n)) . SBP &
(Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for
j being
Nat st 1
< j &
j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )
by A2, A3, A4, A5, Th12, A1;
verum end; suppose
s . (DataLoc ((s . SBP),2)) < s . (DataLoc ((s . SBP),3))
;
ex n being Nat st
( CurInstr (P,(Comput (P,s,n))) = return SBP & s . SBP = (Comput (P,s,n)) . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )then A7:
s . (DataLoc ((s . SBP),3)) > 0
by A6;
reconsider y =
s . (DataLoc ((s . SBP),3)) as
Element of
NAT by A5, INT_1:3;
reconsider pn =
s . SBP as
Element of
NAT by A3, INT_1:3;
A8:
pn = s . SBP
;
then A9:
IC (Comput (P,s,7)) = 5
+ 7
by A2, A4, A7, Lm4, A1;
A10:
Comput (
P,
s,8)
= Exec (
(goto (- 7)),
(Comput (P,s,7)))
by A2, A4, A7, A8, Lm4, A1;
A11:
(Comput (P,s,7)) . SBP = pn + 4
by A2, A4, A7, Lm4, A1;
A12:
(Comput (P,s,7)) . GBP = 0
by A2, A4, A7, A8, Lm4, A1;
A13:
(Comput (P,s,7)) . (intpos (pn + 7)) = (s . (DataLoc ((s . SBP),2))) mod y
by A2, A4, A7, Lm4, A1;
A14:
(Comput (P,s,7)) . (intpos (pn + 6)) = y
by A2, A4, A7, Lm4, A1;
A15:
(Comput (P,s,7)) . (intpos (pn + 4)) = pn
by A2, A4, A7, Lm4, A1;
A16:
(Comput (P,s,7)) . (intpos (pn + 5)) = 11
by A2, A4, A7, Lm4, A1;
set s8 =
Comput (
P,
s,8);
A17:
IC (Comput (P,s,8)) =
ICplusConst (
(Comput (P,s,7)),
(- 7))
by A10, SCMPDS_2:54
.=
5
by A9, Th2
;
A18:
(Comput (P,s,8)) . SBP = pn + 4
by A10, A11, SCMPDS_2:54;
A19:
4
<= pn + 4
by NAT_1:11;
A20:
(Comput (P,s,8)) . SBP > 0
by A18;
A21:
(Comput (P,s,8)) . GBP = 0
by A10, A12, SCMPDS_2:54;
set x1 =
(Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2));
set y1 =
(Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3));
A22:
(Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2)) =
(Comput (P,s,8)) . (intpos ((pn + 4) + 2))
by A18, Th1
.=
y
by A10, A14, SCMPDS_2:54
;
A23:
(Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) =
(Comput (P,s,8)) . (intpos ((pn + 4) + 3))
by A18, Th1
.=
(s . (DataLoc ((s . SBP),2))) mod y
by A10, A13, SCMPDS_2:54
;
then
(Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) < y
by A7, NEWTON:65;
then consider m being
Nat such that A24:
CurInstr (
P,
(Comput (P,(Comput (P,s,8)),m)))
= return SBP
and A25:
(Comput (P,s,8)) . SBP = (Comput (P,(Comput (P,s,8)),m)) . SBP
and A26:
(Comput (P,(Comput (P,s,8)),m)) . (DataLoc (((Comput (P,s,8)) . SBP),2)) = ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2))) gcd ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)))
and A27:
for
j being
Nat st 1
< j &
j <= ((Comput (P,s,8)) . SBP) + 1 holds
(Comput (P,s,8)) . (intpos j) = (Comput (P,(Comput (P,s,8)),m)) . (intpos j)
by A17, A20, A21, A22, A23, Th12, A1, NEWTON:64;
set s9 =
Comput (
P,
s,
(m + 8));
A28:
(Comput (P,s,8)) . SBP = (Comput (P,s,(m + 8))) . SBP
by A25, EXTPRO_1:4;
A29:
Comput (
P,
s,
(m + 8))
= Comput (
P,
(Comput (P,s,8)),
m)
by EXTPRO_1:4;
A30:
Comput (
P,
s,
(m + (8 + 1))) =
Comput (
P,
s,
((m + 8) + 1))
.=
Following (
P,
(Comput (P,s,(m + 8))))
by EXTPRO_1:3
.=
Exec (
(return SBP),
(Comput (P,s,(m + 8))))
by A24, A29
;
A31:
1
< pn + 4
by A19, XXREAL_0:2;
pn + 4
< ((Comput (P,s,8)) . SBP) + 1
by A18, XREAL_1:29;
then A32:
(Comput (P,s,8)) . (intpos (pn + 4)) =
(Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 4))
by A27, A31
.=
(Comput (P,s,(m + 8))) . (intpos (pn + 4))
by EXTPRO_1:4
;
5
<= pn + 5
by NAT_1:11;
then A33:
1
< pn + 5
by XXREAL_0:2;
A34: 11 =
(Comput (P,s,8)) . (intpos (pn + 5))
by A10, A16, SCMPDS_2:54
.=
(Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 5))
by A18, A27, A33
.=
(Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 1))
by EXTPRO_1:4
.=
(Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,(m + 8))) . SBP),RetIC))
by A18, A28, Th1, SCMPDS_I:def 14
;
A35:
P /. (IC (Comput (P,s,(m + 9)))) = P . (IC (Comput (P,s,(m + 9))))
by PBOOLE:143;
A36:
IC (Comput (P,s,(m + 9))) =
|.((Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,(m + 8))) . SBP),RetIC))).| + 2
by A30, SCMPDS_2:58
.=
11
+ 2
by A34, ABSVALUE:29
;
then A37:
CurInstr (
P,
(Comput (P,s,(m + 9)))) =
P . 13
by A35
.=
(
SBP,2)
:= (
SBP,6)
by Lm1, A1
;
A38:
Comput (
P,
s,
(m + (9 + 1))) =
Comput (
P,
s,
((m + 9) + 1))
.=
Following (
P,
(Comput (P,s,(m + 9))))
by EXTPRO_1:3
.=
Exec (
((SBP,2) := (SBP,6)),
(Comput (P,s,(m + 9))))
by A37
;
A39:
(Comput (P,s,(m + 9))) . SBP =
(Comput (P,s,(m + 8))) . (DataLoc ((pn + 4),RetSP))
by A18, A28, A30, SCMPDS_2:58
.=
(Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 0))
by Th1, SCMPDS_I:def 13
.=
pn
by A10, A15, A32, SCMPDS_2:54
;
A40:
(Comput (P,s,(m + 9))) . (intpos (pn + 6)) =
(Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 2))
by A30, Lm3, SCMPDS_2:58
.=
(Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,8)) . SBP),2))
by A18, Th1
.=
((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2))) gcd ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)))
by A26, EXTPRO_1:4
;
A41:
P /. (IC (Comput (P,s,(m + 10)))) = P . (IC (Comput (P,s,(m + 10))))
by PBOOLE:143;
IC (Comput (P,s,(m + 10))) =
(IC (Comput (P,s,(m + 9)))) + 1
by A38, SCMPDS_2:47
.=
13
+ 1
by A36
;
then A42:
CurInstr (
P,
(Comput (P,s,(m + 10)))) =
P . 14
by A41
.=
return SBP
by Lm1, A1
;
hereby verum
reconsider n =
m + 10 as
Nat ;
take n =
n;
( CurInstr (P,(Comput (P,s,n))) = return SBP & (Comput (P,s,n)) . SBP = s . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )thus
CurInstr (
P,
(Comput (P,s,n)))
= return SBP
by A42;
( (Comput (P,s,n)) . SBP = s . SBP & (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )A43:
DataLoc (
((Comput (P,s,(m + 9))) . SBP),2)
= intpos (pn + 2)
by A39, Th1;
hence
(Comput (P,s,n)) . SBP = s . SBP
by A38, A39, Lm3, SCMPDS_2:47;
( (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) & ( for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )thus (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) =
(Comput (P,s,(m + 9))) . (DataLoc (pn,6))
by A38, A39, SCMPDS_2:47
.=
(s . (DataLoc ((s . SBP),3))) gcd ((s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3))))
by A22, A23, A40, Th1
.=
(s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3)))
by A6, A7, NAT_D:30
;
for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j)hereby verum
let j be
Nat;
( 1 < j & j <= (s . SBP) + 1 implies s . (intpos j) = (Comput (P,s,n)) . (intpos j) )assume that A44:
1
< j
and A45:
j <= (s . SBP) + 1
;
s . (intpos j) = (Comput (P,s,n)) . (intpos j)
s . SBP <= (Comput (P,s,8)) . SBP
by A18, NAT_1:11;
then
(s . SBP) + 1
<= ((Comput (P,s,8)) . SBP) + 1
by XREAL_1:6;
then A46:
j <= ((Comput (P,s,8)) . SBP) + 1
by A45, XXREAL_0:2;
A47:
(Comput (P,s,(m + 9))) . (intpos j) =
(Comput (P,s,(m + 8))) . (intpos j)
by A30, A44, AMI_3:10, SCMPDS_2:58
.=
(Comput (P,(Comput (P,s,8)),m)) . (intpos j)
by EXTPRO_1:4
.=
(Comput (P,s,8)) . (intpos j)
by A27, A44, A46
;
A48:
pn + 1
< pn + 2
by XREAL_1:6;
(Comput (P,s,7)) . (intpos j) = s . (intpos j)
by A2, A4, A7, A8, A44, A45, Lm5, A1;
hence s . (intpos j) =
(Comput (P,s,8)) . (intpos j)
by A10, SCMPDS_2:54
.=
(Comput (P,s,n)) . (intpos j)
by A38, A43, A45, A47, A48, AMI_3:10, SCMPDS_2:47
;
verum
end;
end; end; end;