:: Formal Verification of a Generic Iterative Algorithm
:: by Artur Korni{\l}owicz
::
:: Received July 20, 2026
:: Copyright (c) 2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies NUMBERS, CARD_1, XXREAL_0, RELAT_1, FINSEQ_1, ARYTM_3, ARYTM_1,
NAT_1, AMI_3, AFINSQ_1, AMI_1, ORDINAL4, GRAPHSP, SCM_1, MSUALG_1,
FUNCT_1, FSM_1, EXTPRO_1, TARSKI, FINSET_1, ORDINAL1, XCMPLX_0, COMPOS_1,
INT_1, SUBSET_1, REALSET1, PARTFUN1, FUNCOP_1, TURING_1, AMI_2, FRECHET,
CIRCUIT2, FOMODEL1, PBOOLE, EUCLID_3, FUNCT_4, MEMSTR_0, XBOOLE_0,
STRUCT_0, SCMFSA6C, AMI_8;
notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, PROOFS_1, XCMPLX_0, ORDINAL1,
NUMBERS, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, XXREAL_0, XREAL_0, INT_1,
NAT_D, FINSET_1, FUNCOP_1, FUNCT_4, PBOOLE, AFINSQ_1, STRUCT_0, MEMSTR_0,
COMPOS_1, EXTPRO_1, SCM_1, AMI_2, AMI_3, NEWTON, NUMPOLY1, AMISTD_1;
constructors SCM_1, DOMAIN_1, NEWTON, PROOFS_1, NUMPOLY1, AMISTD_1, NAT_D,
RELSET_1, PRE_POLY;
registrations XREAL_0, INT_1, AMI_3, ORDINAL1, AFINSQ_1, SCM_1, COMPOS_0,
NAT_1, EXTPRO_1, FUNCOP_1, STRUCT_0, AMI_6, PBOOLE, NUMPOLY1, RELSET_1,
XXREAL_0, FINSET_1, MEMSTR_0, FUNCT_4, FUNCT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
definitions TARSKI, COMPOS_1, EXTPRO_1, MEMSTR_0, SCM_1;
equalities FUNCOP_1, MEMSTR_0, AFINSQ_1, XCMPLX_0, FUNCT_4, AMI_3, EXTPRO_1;
expansions MEMSTR_0;
theorems NAT_1, SCM_1, AMI_3, XREAL_1, XXREAL_0, EXTPRO_1, ENUMSET1, MEMSTR_0,
AFINSQ_1, TARSKI, CARD_1, GRFUNC_1, INT_1, NEWTON, XCMPLX_1, ORDINAL1,
PBOOLE, FUNCT_4, RELAT_1, FUNCT_1, PARTFUN1, XTUPLE_0, RELSET_1,
XBOOLE_1, AMI_5, AMI_2, ZFMISC_1, AMISTD_1, PROOFS_1, NUMBER02, XREAL_0,
NUMPOLY1;
schemes NAT_1, FUNCT_1, RELSET_1, NAT_D;
begin :: Preliminaries
reserve x1,x2,x3,x4,x5,x6 for object;
reserve f for Function;
reserve j,k,m,n for Nat;
reserve i,i1,i2,i3 for Integer;
Lm1: 2 in {0,1,2,3,4,5} by ENUMSET1:def 4;
Lm2: 0 in {0} by TARSKI:def 1;
registration
let a,b,c,x,y,z be object;
cluster (a,b,c) --> (x,y,z) -> finite;
coherence;
end;
theorem Th1:
dom <%x1,x2,x3,x4%> = {0,1,2,3}
proof
A1: len <%x1,x2,x3%> = 3 by AFINSQ_1:39;
thus dom <%x1,x2,x3,x4%> = len <%x1,x2,x3%> + len <%x4%> by AFINSQ_1:def 3
.= 3+1 by A1,AFINSQ_1:34
.= {0,1,2,3} by CARD_1:52;
end;
theorem
len <%x1,x2,x3,x4%> = 4 by Th1,CARD_1:52;
theorem Th3:
for f,g being Function, w,x,y,z being object st dom f = dom g &
f.w = g.w & f.x = g.x & f.y = g.y & f.z = g.z holds f|{w,x,y,z} = g|{w,x,y,z}
proof
let f,g be Function, w,x,y,z be object;
assume dom f = dom g & f.w = g.w & f.x = g.x & f.y = g.y & f.z = g.z;
then
A1: f|{w,x,y} = g|{w,x,y} & f|{z} = g|{z} by GRFUNC_1:29,31;
{w,x,y,z} = {w,x,y} \/ {z} by ENUMSET1:6;
hence thesis by A1,RELAT_1:150;
end;
begin :: Sequences
definition
let x1,x2,x3,x4,x5;
func <%x1,x2,x3,x4,x5%> -> set equals
<%x1,x2,x3,x4%>^<%x5%>;
coherence;
end;
registration
let x1,x2,x3,x4,x5;
cluster <%x1,x2,x3,x4,x5%> -> Function-like Relation-like;
coherence;
end;
registration
let x1,x2,x3,x4,x5;
cluster <%x1,x2,x3,x4,x5%> -> finite Sequence-like;
coherence;
end;
theorem Th4:
dom <%x1,x2,x3,x4,x5%> = {0,1,2,3,4}
proof
A1: len <%x1,x2,x3,x4%> = 4 by Th1,CARD_1:52;
thus dom <%x1,x2,x3,x4,x5%> = len <%x1,x2,x3,x4%> + len <%x5%>
by AFINSQ_1:def 3
.= 4+1 by A1,AFINSQ_1:34
.= {0,1,2,3,4} by CARD_1:53;
end;
theorem
len <%x1,x2,x3,x4,x5%> = 5 by Th4,CARD_1:53;
registration
let x1,x2,x3,x4,x5;
A1: dom <%x1,x2,x3,x4%> = {0,1,2,3} by Th1;
reduce <%x1,x2,x3,x4,x5%>.0 to x1;
reducibility
proof
0 in dom <%x1,x2,x3,x4%> by A1,ENUMSET1:def 2;
hence <%x1,x2,x3,x4,x5%>.0 = <%x1,x2,x3,x4%>.0 by AFINSQ_1:def 3
.= x1;
end;
reduce <%x1,x2,x3,x4,x5%>.1 to x2;
reducibility
proof
1 in dom <%x1,x2,x3,x4%> by A1,ENUMSET1:def 2;
hence <%x1,x2,x3,x4,x5%>.1 = <%x1,x2,x3,x4%>.1 by AFINSQ_1:def 3
.= x2;
end;
reduce <%x1,x2,x3,x4,x5%>.2 to x3;
reducibility
proof
2 in dom <%x1,x2,x3,x4%> by A1,ENUMSET1:def 2;
hence <%x1,x2,x3,x4,x5%>.2 = <%x1,x2,x3,x4%>.2 by AFINSQ_1:def 3
.= x3;
end;
reduce <%x1,x2,x3,x4,x5%>.3 to x4;
reducibility
proof
3 in dom <%x1,x2,x3,x4%> by A1,ENUMSET1:def 2;
hence <%x1,x2,x3,x4,x5%>.3 = <%x1,x2,x3,x4%>.3 by AFINSQ_1:def 3
.= x4;
end;
reduce <%x1,x2,x3,x4,x5%>.4 to x5;
reducibility
proof
A2: len <%x1,x2,x3,x4%> = 4 by Th1,CARD_1:52;
A3: dom <%x5%> = {0};
thus <%x1,x2,x3,x4,x5%>.4 = (<%x1,x2,x3,x4%>^<%x5%>).(4+0)
.= <%x5%>.0 by A2,A3,Lm2,AFINSQ_1:def 3
.= x5;
end;
end;
definition
let x1,x2,x3,x4,x5,x6;
func <%x1,x2,x3,x4,x5,x6%> -> set equals
<%x1,x2,x3,x4,x5%>^<%x6%>;
coherence;
end;
registration
let x1,x2,x3,x4,x5,x6;
cluster <%x1,x2,x3,x4,x5,x6%> -> Function-like Relation-like;
coherence;
end;
registration
let x1,x2,x3,x4,x5,x6;
cluster <%x1,x2,x3,x4,x5,x6%> -> finite Sequence-like;
coherence;
end;
theorem Th6:
dom <%x1,x2,x3,x4,x5,x6%> = {0,1,2,3,4,5}
proof
A1: len <%x1,x2,x3,x4,x5%> = 5 by Th4,CARD_1:53;
thus dom <%x1,x2,x3,x4,x5,x6%> = len <%x1,x2,x3,x4,x5%> + len <%x6%>
by AFINSQ_1:def 3
.= 5+1 by A1,AFINSQ_1:34
.= {0,1,2,3,4,5} by CARD_1:54;
end;
theorem
len <%x1,x2,x3,x4,x5,x6%> = 6 by Th6,CARD_1:54;
registration
let x1,x2,x3,x4,x5,x6;
A1: dom <%x1,x2,x3,x4,x5%> = {0,1,2,3,4} by Th4;
reduce <%x1,x2,x3,x4,x5,x6%>.0 to x1;
reducibility
proof
0 in dom <%x1,x2,x3,x4,x5%> by A1,ENUMSET1:def 3;
hence <%x1,x2,x3,x4,x5,x6%>.0 = <%x1,x2,x3,x4,x5%>.0 by AFINSQ_1:def 3
.= x1;
end;
reduce <%x1,x2,x3,x4,x5,x6%>.1 to x2;
reducibility
proof
1 in dom <%x1,x2,x3,x4,x5%> by A1,ENUMSET1:def 3;
hence <%x1,x2,x3,x4,x5,x6%>.1 = <%x1,x2,x3,x4,x5%>.1 by AFINSQ_1:def 3
.= x2;
end;
reduce <%x1,x2,x3,x4,x5,x6%>.2 to x3;
reducibility
proof
2 in dom <%x1,x2,x3,x4,x5%> by A1,ENUMSET1:def 3;
hence <%x1,x2,x3,x4,x5,x6%>.2 = <%x1,x2,x3,x4,x5%>.2 by AFINSQ_1:def 3
.= x3;
end;
reduce <%x1,x2,x3,x4,x5,x6%>.3 to x4;
reducibility
proof
3 in dom <%x1,x2,x3,x4,x5%> by A1,ENUMSET1:def 3;
hence <%x1,x2,x3,x4,x5,x6%>.3 = <%x1,x2,x3,x4,x5%>.3 by AFINSQ_1:def 3
.= x4;
end;
reduce <%x1,x2,x3,x4,x5,x6%>.4 to x5;
reducibility
proof
4 in dom <%x1,x2,x3,x4,x5%> by A1,ENUMSET1:def 3;
hence <%x1,x2,x3,x4,x5,x6%>.4 = <%x1,x2,x3,x4,x5%>.4 by AFINSQ_1:def 3
.= x5;
end;
reduce <%x1,x2,x3,x4,x5,x6%>.5 to x6;
reducibility
proof
A2: len <%x1,x2,x3,x4,x5%> = 5 by Th4,CARD_1:53;
A3: dom <%x6%> = {0};
thus <%x1,x2,x3,x4,x5,x6%>.5 = (<%x1,x2,x3,x4,x5%>^<%x6%>).(5+0)
.= <%x6%>.0 by A2,A3,Lm2,AFINSQ_1:def 3
.= x6;
end;
end;
theorem Th8:
<%x1,x2,x3,x4,x5,x6%> c= f implies
f.0 = x1 & f.1 = x2 & f.2 = x3 & f.3 = x4 & f.4 = x5 & f.5 = x6
proof
set g = <%x1,x2,x3,x4,x5,x6%>;
dom g = {0,1,2,3,4,5} by Th6;
then
A1: 0 in dom g & 1 in dom g & 2 in dom g & 3 in dom g & 4 in dom g & 5 in dom g
by ENUMSET1:def 4;
g.0 = x1 & g.1 = x2 & g.2 = x3 & g.3 = x4 & g.4 = x5 & g.5 = x6;
hence thesis by A1,GRFUNC_1:2;
end;
begin :: General theory of SCM
reserve s for State of SCM;
reserve I for Instruction of SCM;
reserve P for Instruction-Sequence of SCM;
reserve X for XFinSequence of the InstructionsF of SCM;
set a = dl.0, b = dl.1, c = dl.2;
theorem
for d being Data-Location holds i in (the_Values_of SCM).d
proof
let d be Data-Location;
d in SCM-Data-Loc by AMI_2:def 16;
then (SCM-VAL*SCM-OK).d = INT by AMI_2:8;
hence thesis by INT_1:def 2;
end;
registration
let la be Data-Location;
let a be Integer;
cluster la .--> a -> (the_Values_of SCM)-compatible;
coherence;
end;
registration
let la,lb be Data-Location;
let a,b be Integer;
cluster (la,lb) --> (a,b) -> (the_Values_of SCM)-compatible;
coherence;
end;
registration
let la,lb,lc be Data-Location;
let a,b,c be Integer;
cluster (la,lb,lc) --> (a,b,c) -> (the_Values_of SCM)-compatible;
coherence;
end;
registration
let d be Data-Location, i be Integer;
cluster d .--> i -> data-only for PartState of SCM;
coherence by ZFMISC_1:11,AMI_5:2;
end;
registration
let p, q be data-only FinPartState of SCM;
cluster p +* q -> data-only;
coherence
proof
A1: dom(p) misses {IC SCM} & dom(q) misses {IC SCM} by MEMSTR_0:def 9;
dom(p+*q) = dom p \/ dom q by FUNCT_4:def 1;
hence dom(p+*q) misses {IC SCM} by A1,XBOOLE_1:70;
end;
end;
registration
let la,lb be Data-Location;
let a,b be Integer;
cluster (la,lb) --> (a,b) -> data-only for FinPartState of SCM;
coherence;
end;
registration
let la,lb,lc be Data-Location;
let a,b,c be Integer;
cluster (la,lb,lc) --> (a,b,c) -> data-only for FinPartState of SCM;
coherence;
end;
definition
let n,I;
attr I is n-dl.constant means
for P being Instruction-Sequence of SCM
for s being State of SCM
for k being Nat st CurInstr(P,Comput(P,s,k)) = I holds
Comput(P,s,k+1).dl.n = Comput(P,s,k).dl.n;
end;
theorem Th10:
m <> j implies AddTo(dl.m,dl.n) is j-dl.constant
proof
assume
A1: m <> j;
let P,s,k;
Comput(P,s,k+1) = Following(P,Comput(P,s,k)) by EXTPRO_1:3;
hence thesis by A1,AMI_3:3,10;
end;
theorem Th11:
m <> j implies SubFrom(dl.m,dl.n) is j-dl.constant
proof
assume
A1: m <> j;
let P,s,k;
Comput(P,s,k+1) = Following(P,Comput(P,s,k)) by EXTPRO_1:3;
hence thesis by A1,AMI_3:4,10;
end;
theorem Th12:
m <> j implies MultBy(dl.m,dl.n) is j-dl.constant
proof
assume
A1: m <> j;
let P,s,k;
Comput(P,s,k+1) = Following(P,Comput(P,s,k)) by EXTPRO_1:3;
hence thesis by A1,AMI_3:5,10;
end;
registration
let m;
let n be non zero Nat;
cluster AddTo(dl.(m+n),dl.m) -> m-dl.constant;
coherence
proof
m+n <> m+0;
hence thesis by Th10;
end;
cluster SubFrom(dl.(m+n),dl.m) -> m-dl.constant;
coherence
proof
m+n <> m+0;
hence thesis by Th11;
end;
cluster MultBy(dl.(m+n),dl.m) -> m-dl.constant;
coherence
proof
m+n <> m+0;
hence thesis by Th12;
end;
end;
registration
cluster AddTo(dl.2,dl.1) -> 0-dl.constant;
coherence by Th10;
cluster SubFrom(dl.2,dl.1) -> 0-dl.constant;
coherence by Th11;
cluster MultBy(dl.2,dl.1) -> 0-dl.constant;
coherence by Th12;
end;
registration
let n;
cluster sequential n-dl.constant for Instruction of SCM;
existence
proof
take AddTo(dl.(n+1),dl.n);
thus thesis;
end;
end;
theorem Th13:
for I being sequential Instruction of SCM
st CurInstr(P,Comput(P,s,n)) = I & IC Comput(P,s,n) in dom P
holds IC Comput(P,s,n+1) = IC Comput(P,s,n) + 1
proof
let I be sequential Instruction of SCM;
set t = Comput(P,s,n);
assume
A1: CurInstr(P,t) = I;
assume IC t in dom P;
then
A2: P.IC t = I by A1,PARTFUN1:def 6;
Comput(P,s,n+1) = Following(P,t) by EXTPRO_1:3;
hence IC Comput(P,s,n+1) = Exec(P.IC t,t).IC SCM by EXTPRO_1:28
.= IC t+1 by A2,AMISTD_1:def 8;
end;
theorem Th14:
for s being n-started State-consisting of <%i1,i2,i3%>
holds s.dl.0 = i1 & s.dl.1 = i2 & s.dl.2 = i3
proof
let s be n-started State-consisting of <%i1,i2,i3%>;
set D = <%i1,i2,i3%>;
A1: len D = 3 by AFINSQ_1:39;
D.0 = i1 & D.1 = i2 & D.2 = i3;
hence thesis by A1,SCM_1:def 1;
end;
registration
let X;
cluster X-extending for Instruction-Sequence of SCM;
existence
proof
consider s being the InstructionsF of SCM-valued ManySortedSet of NAT
such that
A1: X c= s by PBOOLE:145;
take s;
thus thesis by A1,PROOFS_1:def 12;
end;
end;
set SA = Start-At(0,SCM);
theorem Th15:
for s being State of SCM st Initialize ((dl.0,dl.1,dl.2) --> (i1,i2,i3)) c= s
holds s is State-consisting of <%i1,i2,i3%>
proof
set x = (a,b,c) --> (i1,i2,i3);
let s be State of SCM such that
A1: Initialize x c= s;
set D = <%i1,i2,i3%>;
let k be Nat such that
A2: k < len D;
len D = 2+1 by AFINSQ_1:39;
then k <= 2 by A2,NAT_1:13;
then
A3: k = 0 or ... or k = 2;
A4: a <> b & a <> c by AMI_3:10;
A5: dom x = {a,b,c} by FUNCT_4:128;
A6: dom x c= dom(x+*SA) by FUNCT_4:10;
A7: a in {a,b,c} by ENUMSET1:def 1;
a <> IC SCM by AMI_5:2;
then not a in dom SA by TARSKI:def 1;
then
A8: (x+*SA).a = x.a by FUNCT_4:11
.= i1 by A4,FUNCT_4:134;
A9: b in {a,b,c} by ENUMSET1:def 1;
b <> IC SCM by AMI_5:2;
then not b in dom SA by TARSKI:def 1;
then
A10: (x+*SA).b = x.b by FUNCT_4:11
.= i2 by AMI_3:10,FUNCT_4:135;
A11: c in {a,b,c} by ENUMSET1:def 1;
c <> IC SCM by AMI_5:2;
then not c in dom SA by TARSKI:def 1;
then (x+*SA).c = x.c by FUNCT_4:11
.= i3 by FUNCT_4:135;
hence s.dl.k = D.k by A1,A3,A5,A6,A7,A8,A9,A10,A11,GRFUNC_1:2;
end;
begin :: Correctness of algorithms computing operations on one previous element
:: dl.0 - a, dl.1 - b, dl.2 - c
:: a := 1 - for step
:: b - input
:: c - output
:: 0) if b > 0 then goto 2
:: 1) halt
:: 2) I (e.g., c := c+b or c := c*b)
:: 3) b := b-a
:: 4) if b = 0 then goto 1
:: 5) goto 2
definition
let OPER be Instruction of SCM;
func IterativeAlgorithm(OPER) -> XFinSequence of the InstructionsF of SCM
equals
<% dl.1 >0_goto 2,
halt SCM,
OPER,
SubFrom(dl.1,dl.0),
dl.1 =0_goto 1,
SCM-goto 2
%>;
coherence;
end;
theorem Th16:
IterativeAlgorithm(I) c= P implies
for k st IC Comput(P,s,k) = 0 holds
(Comput(P,s,k).dl.1 > 0 implies IC Comput(P,s,k+1) = 2) &
(Comput(P,s,k).dl.1 <= 0 implies IC Comput(P,s,k+1) = 1) &
for j holds Comput(P,s,k+1).dl.j = Comput(P,s,k).dl.j
proof
assume
A1: IterativeAlgorithm(I) c= P;
let k such that
A2: IC Comput(P,s,k) = 0;
A3: Comput(P,s,k+1) = Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(b >0_goto 2,Comput(P,s,k)) by A1,A2,Th8;
hence Comput(P,s,k).dl.1 > 0 implies IC Comput(P,s,k+1) = 2 by AMI_3:9;
thus Comput(P,s,k).dl.1 <= 0 implies IC Comput(P,s,k+1) = 1
proof
assume Comput(P,s,k).b <= 0;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by A3,AMI_3:9
.= 1 by A2;
end;
thus thesis by A3,AMI_3:9;
end;
theorem Th17:
IterativeAlgorithm(I) c= P implies P halts_at 1
proof
assume IterativeAlgorithm(I) c= P;
hence P.1 = halt SCM by Th8;
end;
theorem Th18:
IterativeAlgorithm(I) c= P implies
for k,j st IC Comput(P,s,k) = 1 holds Comput(P,s,k+j) = Comput(P,s,k)
proof
assume
A1: IterativeAlgorithm(I) c= P;
let k,j;
assume IC Comput(P,s,k) = 1;
then P halts_at IC Comput(P,s,k) by A1,Th17;
hence thesis by EXTPRO_1:20,NAT_1:11;
end;
theorem Th19:
IterativeAlgorithm(AddTo(dl.m,dl.n)) c= P implies
for k st IC Comput(P,s,k) = 2 holds
IC Comput(P,s,k+1) = 3 &
Comput(P,s,k+1).dl.m = Comput(P,s,k).dl.m + Comput(P,s,k).dl.n &
for j st j <> m holds Comput(P,s,k+1).dl.j = Comput(P,s,k).dl.j
proof
set c = dl.m, b = dl.n;
assume
A1: IterativeAlgorithm(AddTo(c,b)) c= P;
let k such that
A2: IC Comput(P,s,k) = 2;
A3: Comput(P,s,k+1) = Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(AddTo(c,b),Comput(P,s,k)) by A1,A2,Th8;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by AMI_3:3
.= 3 by A2;
thus Comput(P,s,k+1).c = Comput(P,s,k).c + Comput(P,s,k).b by A3,AMI_3:3;
thus thesis by A3,AMI_3:3,10;
end;
theorem Th20:
IterativeAlgorithm(SubFrom(dl.m,dl.n)) c= P implies
for k st IC Comput(P,s,k) = 2 holds
IC Comput(P,s,k+1) = 3 &
Comput(P,s,k+1).dl.m = Comput(P,s,k).dl.m - Comput(P,s,k).dl.n &
for j st j <> m holds Comput(P,s,k+1).dl.j = Comput(P,s,k).dl.j
proof
set c = dl.m, b = dl.n;
assume
A1: IterativeAlgorithm(SubFrom(c,b)) c= P;
let k such that
A2: IC Comput(P,s,k) = 2;
A3: Comput(P,s,k+1) = Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(SubFrom(c,b),Comput(P,s,k)) by A1,A2,Th8;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by AMI_3:4
.= 3 by A2;
thus Comput(P,s,k+1).c = Comput(P,s,k).c - Comput(P,s,k).b by A3,AMI_3:4;
thus thesis by A3,AMI_3:4,10;
end;
theorem Th21:
IterativeAlgorithm(MultBy(dl.m,dl.n)) c= P implies
for k st IC Comput(P,s,k) = 2 holds
IC Comput(P,s,k+1) = 3 &
Comput(P,s,k+1).dl.m = Comput(P,s,k).dl.m * Comput(P,s,k).dl.n &
for j st j <> m holds Comput(P,s,k+1).dl.j = Comput(P,s,k).dl.j
proof
set c = dl.m, b = dl.n;
assume
A1: IterativeAlgorithm(MultBy(c,b)) c= P;
let k such that
A2: IC Comput(P,s,k) = 2;
A3: Comput(P,s,k+1) = Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(MultBy(c,b),Comput(P,s,k)) by A1,A2,Th8;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by AMI_3:5
.= 3 by A2;
thus Comput(P,s,k+1).c = Comput(P,s,k).c * Comput(P,s,k).b by A3,AMI_3:5;
thus thesis by A3,AMI_3:5,10;
end;
theorem Th22:
IterativeAlgorithm(I) c= P implies
for k st IC Comput(P,s,k) = 3 holds
IC Comput(P,s,k+1) = 4 &
Comput(P,s,k+1).dl.1 = Comput(P,s,k).dl.1 - Comput(P,s,k).dl.0 &
for j st j <> 1 holds Comput(P,s,k+1).dl.j = Comput(P,s,k).dl.j
proof
assume
A1: IterativeAlgorithm(I) c= P;
let k such that
A2: IC Comput(P,s,k) = 3;
A3: Comput(P,s,k+1) = Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(SubFrom(b,a),Comput(P,s,k)) by A1,A2,Th8;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by AMI_3:4
.= 4 by A2;
thus Comput(P,s,k+1).b = Comput(P,s,k).b - Comput(P,s,k).a by A3,AMI_3:4;
thus thesis by A3,AMI_3:4,10;
end;
theorem Th23:
IterativeAlgorithm(I) c= P implies
for k st IC Comput(P,s,k) = 4 holds
(Comput(P,s,k).dl.1 = 0 implies IC Comput(P,s,k+1) = 1) &
(Comput(P,s,k).dl.1 <> 0 implies IC Comput(P,s,k+1) = 5) &
for j holds Comput(P,s,k+1).dl.j = Comput(P,s,k).dl.j
proof
assume
A1: IterativeAlgorithm(I) c= P;
let k such that
A2: IC Comput(P,s,k) = 4;
A3: Comput(P,s,k+1) = Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(b =0_goto 1,Comput(P,s,k)) by A1,A2,Th8;
hence Comput(P,s,k).dl.1 = 0 implies IC Comput(P,s,k+1) = 1 by AMI_3:8;
thus Comput(P,s,k).dl.1 <> 0 implies IC Comput(P,s,k+1) = 5
proof
assume Comput(P,s,k).b <> 0;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by A3,AMI_3:8
.= 5 by A2;
end;
thus thesis by A3,AMI_3:8;
end;
theorem Th24:
IterativeAlgorithm(I) c= P implies
for k st IC Comput(P,s,k) = 5 holds
IC Comput(P,s,k+1) = 2 &
for j holds Comput(P,s,k+1).dl.j = Comput(P,s,k).dl.j
proof
assume
A1: IterativeAlgorithm(I) c= P;
let k such that
A2: IC Comput(P,s,k) = 5;
A3: Comput(P,s,k+1) = Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(SCM-goto 2,Comput(P,s,k)) by A1,A2,Th8;
hence IC Comput(P,s,k+1) = 2 by AMI_3:7;
thus thesis by A3,AMI_3:7;
end;
registration
let I;
cluster IterativeAlgorithm(I) -> (the InstructionsF of SCM)-valued;
coherence;
end;
registration
let I;
cluster IterativeAlgorithm(I) -> non halt-free;
coherence
proof
take 1;
dom IterativeAlgorithm(I) = {0,1,2,3,4,5} by Th6;
hence 1 in dom IterativeAlgorithm(I) by ENUMSET1:def 4;
thus IterativeAlgorithm(I).1 = halt SCM;
end;
end;
theorem Th25:
I is sequential & IterativeAlgorithm(I) c= P & IC Comput(P,s,0) = 0 implies
IC Comput(P,s,k) in {0,1,2,3,4,5}
proof
set F = IterativeAlgorithm(I);
assume that
A1: I is sequential and
A2: F c= P and
A3: IC Comput(P,s,0) = 0;
defpred P[Nat] means IC Comput(P,s,$1) in {0,1,2,3,4,5};
A4: P[0] by A3,ENUMSET1:def 4;
A5: for j st P[j] holds P[j+1]
proof
let j;
set t = Comput(P,s,j);
set t1 = Comput(P,s,j+1);
assume P[j];
then per cases by ENUMSET1:def 4;
suppose
A6: IC t = 0;
t.b > 0 or t.b <= 0;
then IC t1 = 1 or IC t1 = 2 by A2,A6,Th16;
hence thesis by ENUMSET1:def 4;
end;
suppose IC t = 1;
then IC t1 = 1 by A2,Th18;
hence thesis by ENUMSET1:def 4;
end;
suppose
A7: IC t = 2;
then
A8: I = P.IC t by A2,Th8;
IC t1 = IC Following(P,t) by EXTPRO_1:3
.= Exec(I,t).IC SCM by A8,EXTPRO_1:28
.= 2+1 by A7,A1,AMISTD_1:def 8;
hence thesis by ENUMSET1:def 4;
end;
suppose IC t = 3;
then IC t1 = 4 by A2,Th22;
hence thesis by ENUMSET1:def 4;
end;
suppose
A9: IC t = 4;
t.b = 0 or t.b <> 0;
then IC t1 = 1 or IC t1 = 5 by A2,A9,Th23;
hence thesis by ENUMSET1:def 4;
end;
suppose IC t = 5;
then IC t1 = 2 by A2,Th24;
hence thesis by ENUMSET1:def 4;
end;
end;
for j holds P[j] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem Th26:
I is sequential & I is 0-dl.constant & IterativeAlgorithm(I) c= P implies
for s being 0-started State-consisting of <%i,i1,i2%> holds
Comput(P,s,k).dl.0 = i
proof
assume that
A1: I is sequential and
A2: I is 0-dl.constant and
A3: IterativeAlgorithm(I) c= P;
let s be 0-started State-consisting of <%i,i1,i2%>;
defpred P[Nat] means Comput(P,s,$1).a = i;
A4: IC Comput(P,s,0) = 0 by MEMSTR_0:def 12;
A5: P[0] by Th14;
A6: for k st P[k] holds P[k+1]
proof
let k such that
A7: P[k];
set s1 = Comput(P,s,k);
IC s1 in {0,1,2,3,4,5} by A1,A3,A4,Th25;
then per cases by ENUMSET1:def 4;
suppose IC s1 = 0 or IC s1 = 1 or IC s1 = 3 or IC s1 = 4 or IC s1 = 5;
hence Comput(P,s,k+1).a = i by A3,A7,Th16,Th18,Th22,Th23,Th24;
end;
suppose
A8: IC s1 = 2;
A9: dom IterativeAlgorithm(I) = {0,1,2,3,4,5} by Th6;
dom IterativeAlgorithm(I) c= dom P by A3,GRFUNC_1:2;
then CurInstr(P,Comput(P,s,k)) = P.2 by A8,A9,Lm1,PARTFUN1:def 6
.= I by A3,Th8;
hence Comput(P,s,k+1).a = i by A7,A2;
end;
end;
for k holds P[k] from NAT_1:sch 2(A5,A6);
hence thesis;
end;
theorem Th27:
I is sequential 0-dl.constant implies
for P being Instruction-Sequence of SCM st IterativeAlgorithm(I) c= P holds
for s being 0-started State-consisting of <%i1,0,i2%> holds
IC Comput(P,s,0) = 0 &
(for k being Nat st k >= 1 holds IC Comput(P,s,k) = 1) &
(for k being Nat holds
Comput(P,s,k).dl.0 = i1 & Comput(P,s,k).dl.1 = 0 & Comput(P,s,k).dl.2 = i2)
& LifeSpan(P,s) = 1
proof
assume
A1: I is sequential 0-dl.constant;
let P be Instruction-Sequence of SCM;
assume
A2: IterativeAlgorithm(I) c= P;
let s be 0-started State-consisting of <%i1,0,i2%>;
thus IC Comput(P,s,0) = 0 by MEMSTR_0:def 12;
set s0 = Comput(P,s,0);
set s1 = Comput(P,s,0+1);
A3: IC s0 = 0 by MEMSTR_0:def 12;
A4: s0.b = 0 by Th14;
A5: s0.c = i2 by Th14;
A6: IC s1 = 1 by A2,A3,A4,Th16;
hereby
let k be Nat;
assume k >= 1;
then reconsider z = k-1 as Element of NAT by INT_1:3;
Comput(P,s,1+z) = s1 by A2,A6,Th18;
hence IC Comput(P,s,k) = 1 by A2,A3,A4,Th16;
end;
hereby
let k be Nat;
thus Comput(P,s,k).a = i1 by A1,A2,Th26;
per cases by NAT_1:6;
suppose k = 0;
hence Comput(P,s,k).b = 0 & Comput(P,s,k).c = i2 by Th14;
end;
suppose ex z being Nat st k = z + 1;
then consider z being Nat such that
A7: k = z+1;
s1.b = s0.b & s1.c = s0.c by A2,A3,Th16;
hence Comput(P,s,k).b = 0 & Comput(P,s,k).c = i2
by A2,A4,A5,A6,A7,Th18;
end;
end;
P.1 = halt SCM by A2,Th8;
hence LifeSpan(P,s) = 1 by A3,A6,EXTPRO_1:33;
end;
theorem
for A being Integer, N being Nat
for P being Instruction-Sequence of SCM
st IterativeAlgorithm(I) c= P & I is sequential 0-dl.constant holds
for s being 0-started State-consisting of <%1,N,A%> st
Comput(P,s,2).dl.1 = Comput(P,s,1).dl.1 &
(for k being Nat holds Comput(P,s,4*k+6).dl.1 = Comput(P,s,4*k+5).dl.1)
holds
P halts_on s & IC Comput(P,s,0) = 0 & Comput(P,s,1).dl.2 = A &
(for k being Nat st 0 < k < N holds IC Comput(P,s,4*k) = 5) &
(for k being Nat st k < N holds
IC Comput(P,s,4*k+1) = 2 & IC Comput(P,s,4*k+2) = 3 &
IC Comput(P,s,4*k+3) = 4 &
Comput(P,s,4*k+1).dl.1 = N-k & Comput(P,s,4*k+2).dl.1 = N-k &
Comput(P,s,4*k+3).dl.1 = N-k-1 & Comput(P,s,4*k+4).dl.1 = N-k-1 &
Comput(P,s,4*k).dl.1 > 0 & Comput(P,s,4*k+1).dl.1 > 0 &
Comput(P,s,4*k+2).dl.1 > 0
) &
(N <> 0 implies LifeSpan(P,s) = 4*N &
for k,j being Nat st k >= N holds
IC Comput(P,s,4*k+j) = 1 & Comput(P,s,4*k+1+j).dl.1 = 0)
proof
let A be Integer, N be Nat;
let P be Instruction-Sequence of SCM such that
A1: IterativeAlgorithm(I) c= P and
A2: I is sequential and
A3: I is 0-dl.constant;
let s be 0-started State-consisting of <%1,N,A%>;
A4: P.1 = halt SCM by A1,Th8;
set s0 = Comput(P,s,0);
set s1 = Comput(P,s,0+1);
set s2 = Comput(P,s,1+1);
set s3 = Comput(P,s,2+1);
set s4 = Comput(P,s,3+1);
set s5 = Comput(P,s,4+1);
assume that
A5: Comput(P,s,2).b = Comput(P,s,1).b and
A6: for k being Nat holds Comput(P,s,4*k+6).b = Comput(P,s,4*k+5).b;
A7: IC s0 = 0 by MEMSTR_0:def 12;
A8: s0.b = N by Th14;
A9: s0.c = A by Th14;
A10: s1.b = s0.b by A1,A7,Th16;
A11: s1.c = s0.c by A1,A7,Th16;
per cases by NAT_1:6;
suppose
A12: N = 0;
then P.IC s1 = halt SCM by A4,A1,A7,A8,Th16;
hence P halts_on s by EXTPRO_1:30;
thus IC Comput(P,s,0) = 0 by MEMSTR_0:def 12;
thus Comput(P,s,1).c = A by A9,A11;
thus thesis by A12;
end;
suppose ex K being Nat st N = K+1;
then consider K being Nat such that
A13: N = K+1;
A14: IC s1 = 2 by A1,A7,A8,A13,Th16;
A15: dom IterativeAlgorithm(I) = {0,1,2,3,4,5} by Th6;
A16: dom IterativeAlgorithm(I) c= dom P by A1,GRFUNC_1:2;
A17: IC s1 in dom P by A14,A15,A16,Lm1;
CurInstr(P,s1) = P.IC s1 by A17,PARTFUN1:def 6
.= I by A1,A14,Th8;
then
A18: IC s2 = 2+1 by A14,A2,A17,Th13;
A19: s2.a = 1 by A1,A2,A3,Th26;
A20: IC s3 = 4 by A1,A18,Th22;
A21: s3.b = s2.b-s2.a by A1,A18,Th22;
A22: s4.b = s3.b by A1,A20,Th23;
defpred P[Nat] means ($1 < N implies
(for u being State of SCM st u = Comput(P,s,4*$1+3) holds
u.b = N-$1-1 & IC u = 4) &
IC Comput(P,s,4*$1+1) = 2 & IC Comput(P,s,4*$1+2) = 3 &
(0 < $1 implies IC Comput(P,s,4*$1) = 5) &
(Comput(P,s,4*$1).b > 0 & Comput(P,s,4*$1+1).b > 0 &
Comput(P,s,4*$1+2).b > 0) &
Comput(P,s,4*$1+1).b = N-$1 & Comput(P,s,4*$1+2).b = N-$1 &
Comput(P,s,4*$1+4).b = N-$1-1
) &
(N <> 0 implies
for j being Nat st $1 >= N holds Comput(P,s,4*$1+1+j).b = 0) &
(N <> 0 & $1 >= N implies for j being Nat holds IC Comput(P,s,4*$1+j) = 1);
A23: P[0]
proof
hereby
assume
A24: 0 < N;
thus
A25: for u being State of SCM st u = Comput(P,s,4*0+3) holds
u.b = N-0-1 & IC u = 4 by A8,A10,A19,A5,A20,A21;
thus IC Comput(P,s,4*0+1) = 2 by A14;
thus IC Comput(P,s,4*0+2) = 3 by A18;
thus 0 > 0 implies IC Comput(P,s,4*0) = 5;
thus Comput(P,s,4*0).b > 0 &
Comput(P,s,4*0+1).b > 0 & Comput(P,s,4*0+2).b > 0 by A8,A10,A5,A24;
thus Comput(P,s,4*0+1).b = N-0 by A8,A10;
thus Comput(P,s,4*0+2).b = N-0 by A8,A10,A5;
thus Comput(P,s,4*0+4).b = N-0-1 by A22,A25;
end;
thus N <> 0 implies
for j being Nat st 0 >= N holds Comput(P,s,4*0+1+j).b = 0;
thus N <> 0 & 0 >= N implies
for j being Nat holds IC Comput(P,s,4*0+j) = 1;
end;
A26: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A27: (k < N implies (for u being State of SCM st u = Comput(P,s,4*k+3)
holds u.b = N-k-1 & IC u = 4) &
IC Comput(P,s,4*k+1) = 2 & IC Comput(P,s,4*k+2) = 3 &
(0 < k implies IC Comput(P,s,4*k) = 5) &
(Comput(P,s,4*k).b > 0 & Comput(P,s,4*k+1).b > 0 &
Comput(P,s,4*k+2).b > 0) &
Comput(P,s,4*k+1).b = N-k & Comput(P,s,4*k+2).b = N-k &
Comput(P,s,4*k+4).b = N-k-1
) &
(N <> 0 implies
for j being Nat st k >= N holds Comput(P,s,4*k+1+j).b = 0) &
(N <> 0 & k >= N implies
for j being Nat holds IC Comput(P,s,4*k+j) = 1);
set S = 4*k+3;
set s3 = Comput(P,s,S);
set s4 = Comput(P,s,S+1);
set s5 = Comput(P,s,S+1+1);
set s6 = Comput(P,s,S+2+1);
set s7 = Comput(P,s,S+3+1);
set s8 = Comput(P,s,S+4+1);
hereby
assume
A28: k+1 < N;
A29: k < N by A28,XXREAL_0:2,NAT_1:16;
A30: N-(k+1) > k+1-(k+1) by A28,XREAL_1:9;
A31: IC s3 = 4 by A27,A29;
A32: s3.b = N-k-1 by A27,A29;
then
A33: IC s4 = 5 by A1,A30,A31,Th23;
then
A34: IC s5 = 2 by A1,Th24;
A35: s4.b = s3.b by A1,A31,Th23;
A36: s5.b = s4.b by A1,A33,Th24;
Comput(P,s,4*k+6).b = Comput(P,s,4*k+5).b by A6;
then
A37: s6.b = s5.b;
A38: IC s5 in dom P by A34,A15,A16,Lm1;
CurInstr(P,s5) = P.IC s5 by A38,PARTFUN1:def 6
.= I by A1,A34,Th8;
then
A39: IC s6 = 2+1 by A34,A2,A38,Th13;
A40: s7.b = s6.b-s6.a by A1,A39,Th22;
A41: IC s7 = 4 by A1,A39,Th22;
then
A42: s8.b = s7.b by A1,Th23;
s6.a = 1 by A1,A2,A3,Th26;
hence
A43: for u being State of SCM st u = Comput(P,s,4*(k+1)+3)
holds u.b = N-(k+1)-1 & IC u = 4 by A32,A40,A41,A37,A36,A35;
thus IC Comput(P,s,4*(k+1)+1) = 2 by A34;
thus IC Comput(P,s,4*(k+1)+2) = 3 by A39;
thus 0 < k+1 implies IC Comput(P,s,4*(k+1)) = 5 by A33;
thus Comput(P,s,4*(k+1)).b > 0 by A30,A32,A35;
thus Comput(P,s,4*(k+1)+1).b > 0 by A30,A32,A35,A36;
thus Comput(P,s,4*(k+1)+2).b > 0 by A30,A32,A35,A36,A37;
thus Comput(P,s,4*(k+1)+1).b = N-(k+1) by A32,A35,A36;
thus Comput(P,s,4*(k+1)+2).b = N-(k+1) by A32,A35,A36,A37;
thus Comput(P,s,4*(k+1)+4).b = N-(k+1)-1 by A42,A43;
end;
hereby
assume
A44: N <> 0;
let j be Nat;
assume k+1 >= N;
then per cases by XXREAL_0:1;
suppose
A45: N = k+1;
then IC s3 = 4 & s3.b = 0 by A27,NAT_1:16;
then IC s4 = 1 by A1,Th23;
then Comput(P,s,4*k+4) = Comput(P,s,4*k+4+(1+j)) by A1,Th18;
hence Comput(P,s,4*(k+1)+1+j).b = 0 by A27,A45,NAT_1:16;
end;
suppose N < k+1;
then Comput(P,s,4*k+1+(4+j)).b = 0 by A27,A44,NAT_1:13;
hence Comput(P,s,4*(k+1)+1+j).b = 0;
end;
end;
assume that
A46: N <> 0 and
A47: k+1 >= N;
let j be Nat;
per cases by A47,XXREAL_0:1;
suppose k+1 > N;
then IC Comput(P,s,4*k+(4+j)) = 1 by A27,A46,NAT_1:13;
hence IC Comput(P,s,4*(k+1)+j) = 1;
end;
suppose k+1 = N;
then IC s3 = 4 & s3.b = 0 by A27,NAT_1:16;
then IC s4 = 1 by A1,Th23;
hence IC Comput(P,s,4*(k+1)+j) = 1 by A1,Th18;
end;
end;
A48: for k being Nat holds P[k] from NAT_1:sch 2(A23,A26);
set t = Comput(P,s,4*K+3);
set t1 = Comput(P,s,4*K+3+1);
A49: K < N by A13,NAT_1:13;
then
A50: IC t = 4 by A48;
t.b = N-K-1 by A48,A49
.= 0 by A13;
then
A51: IC t1 = 1 by A1,A50,Th23;
hence P halts_on s by A4,EXTPRO_1:30;
thus IC Comput(P,s,0) = 0 by A7;
thus Comput(P,s,1).c = A by A9,A11;
thus for k being Nat st 0 < k < N holds IC Comput(P,s,4*k) = 5 by A48;
thus for k being Nat st k < N holds
IC Comput(P,s,4*k+1) = 2 & IC Comput(P,s,4*k+2) = 3 &
IC Comput(P,s,4*k+3) = 4 &
Comput(P,s,4*k+1).b = N-k & Comput(P,s,4*k+2).b = N-k &
Comput(P,s,4*k+3).b = N-k-1 & Comput(P,s,4*k+4).b = N-k-1 &
Comput(P,s,4*k).b > 0 & Comput(P,s,4*k+1).b > 0 &
Comput(P,s,4*k+2).b > 0 by A48;
assume
A52: N <> 0;
thus LifeSpan(P,s) = 4*N by A4,A13,A50,A51,EXTPRO_1:33;
thus thesis by A48,A52;
end;
end;
theorem Th29:
for A being Integer, N being Nat
for P being Instruction-Sequence of SCM
st (I = AddTo(dl.2,dl.1) or I = SubFrom(dl.2,dl.1) or I = MultBy(dl.2,dl.1))
& IterativeAlgorithm(I) c= P holds
for s being 0-started State-consisting of <%1,N,A%> holds
P halts_on s & Comput(P,s,1).dl.2 = A &
(for k being Nat st 0 < k < N holds IC Comput(P,s,4*k) = 5) &
(for k being Nat st k < N holds
IC Comput(P,s,4*k+1) = 2 & IC Comput(P,s,4*k+2) = 3 &
IC Comput(P,s,4*k+3) = 4 &
Comput(P,s,4*k+1).dl.1 = N-k & Comput(P,s,4*k+2).dl.1 = N-k &
Comput(P,s,4*k+3).dl.1 = N-k-1 & Comput(P,s,4*k+4).dl.1 = N-k-1 &
Comput(P,s,4*k).dl.1 > 0 & Comput(P,s,4*k+1).dl.1 > 0 &
Comput(P,s,4*k+2).dl.1 > 0
) &
(N <> 0 implies LifeSpan(P,s) = 4*N &
for k,j being Nat st k >= N holds
IC Comput(P,s,4*k+j) = 1 & Comput(P,s,4*k+1+j).dl.1 = 0)
proof
let A be Integer, N be Nat;
let P be Instruction-Sequence of SCM such that
A1: I = AddTo(c,b) or I = SubFrom(c,b) or I = MultBy(c,b)
and
A2: IterativeAlgorithm(I) c= P;
let s be 0-started State-consisting of <%1,N,A%>;
A3: P.1 = halt SCM by A2,Th8;
set s0 = Comput(P,s,0);
set s1 = Comput(P,s,0+1);
set s2 = Comput(P,s,1+1);
set s3 = Comput(P,s,2+1);
set s4 = Comput(P,s,3+1);
set s5 = Comput(P,s,4+1);
A4: IC s0 = 0 by MEMSTR_0:def 12;
A5: s0.a = 1 by Th14;
A6: s0.b = N by Th14;
A7: s0.c = A by Th14;
A8: s1.a = s0.a by A2,A4,Th16;
A9: s1.b = s0.b by A2,A4,Th16;
A10: s1.c = s0.c by A2,A4,Th16;
per cases by NAT_1:6;
suppose
A11: N = 0;
then P.IC s1 = halt SCM by A3,A2,A4,A6,Th16;
hence P halts_on s by EXTPRO_1:30;
thus Comput(P,s,1).c = A by A7,A10;
thus thesis by A11;
end;
suppose ex K being Nat st N = K+1;
then consider K being Nat such that
A12: N = K+1;
A13: IC s1 = 2 by A2,A4,A6,A12,Th16;
A14: IC s2 = 3 by A1,A2,A13,Th19,Th20,Th21;
A15: s2.a = s1.a by A1,A2,A13,Th19,Th20,Th21;
A16: s2.b = s1.b by A1,A2,A13,Th19,Th20,Th21;
A17: IC s3 = 4 by A2,A14,Th22;
A18: s3.a = s2.a by A2,A14,Th22;
A19: s3.b = s2.b-s2.a by A2,A14,Th22;
A20: s4.b = s3.b by A2,A17,Th23;
defpred P[Nat] means ($1 < N implies
(for u being State of SCM st u = Comput(P,s,4*$1+3) holds
u.a = 1 & u.b = N-$1-1 & IC u = 4) &
IC Comput(P,s,4*$1+1) = 2 & IC Comput(P,s,4*$1+2) = 3 &
(0 < $1 implies IC Comput(P,s,4*$1) = 5) &
(Comput(P,s,4*$1).b > 0 & Comput(P,s,4*$1+1).b > 0 &
Comput(P,s,4*$1+2).b > 0) &
Comput(P,s,4*$1+1).b = N-$1 & Comput(P,s,4*$1+2).b = N-$1 &
Comput(P,s,4*$1+4).b = N-$1-1
) &
(N <> 0 implies
for j being Nat st $1 >= N holds Comput(P,s,4*$1+1+j).b = 0) &
(N <> 0 & $1 >= N implies for j being Nat holds IC Comput(P,s,4*$1+j) = 1);
A21: P[0]
proof
hereby
assume
A22: 0 < N;
thus
A23: for u being State of SCM st u = Comput(P,s,4*0+3) holds
u.a = 1 & u.b = N-0-1 & IC u = 4 by A5,A6,A8,A9,A15,A16,A17,A18,A19;
thus IC Comput(P,s,4*0+1) = 2 by A13;
thus IC Comput(P,s,4*0+2) = 3 by A14;
thus 0 > 0 implies IC Comput(P,s,4*0) = 5;
thus Comput(P,s,4*0).b > 0 &
Comput(P,s,4*0+1).b > 0 & Comput(P,s,4*0+2).b > 0 by A6,A9,A16,A22;
thus Comput(P,s,4*0+1).b = N-0 by A6,A9;
thus Comput(P,s,4*0+2).b = N-0 by A6,A9,A16;
thus Comput(P,s,4*0+4).b = N-0-1 by A20,A23;
end;
thus N <> 0 implies
for j being Nat st 0 >= N holds Comput(P,s,4*0+1+j).b = 0;
thus N <> 0 & 0 >= N implies
for j being Nat holds IC Comput(P,s,4*0+j) = 1;
end;
A24: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A25: (k < N implies (for u being State of SCM st u = Comput(P,s,4*k+3)
holds
u.a = 1 & u.b = N-k-1 & IC u = 4) &
IC Comput(P,s,4*k+1) = 2 & IC Comput(P,s,4*k+2) = 3 &
(0 < k implies IC Comput(P,s,4*k) = 5) &
(Comput(P,s,4*k).b > 0 & Comput(P,s,4*k+1).b > 0 &
Comput(P,s,4*k+2).b > 0) &
Comput(P,s,4*k+1).b = N-k & Comput(P,s,4*k+2).b = N-k &
Comput(P,s,4*k+4).b = N-k-1
) &
(N <> 0 implies
for j being Nat st k >= N holds Comput(P,s,4*k+1+j).b = 0) &
(N <> 0 & k >= N implies
for j being Nat holds IC Comput(P,s,4*k+j) = 1);
set S = 4*k+3;
set s3 = Comput(P,s,S);
set s4 = Comput(P,s,S+1);
set s5 = Comput(P,s,S+1+1);
set s6 = Comput(P,s,S+2+1);
set s7 = Comput(P,s,S+3+1);
set s8 = Comput(P,s,S+4+1);
hereby
assume
A26: k+1 < N;
A27: k < N by A26,XXREAL_0:2,NAT_1:16;
A28: N-(k+1) > k+1-(k+1) by A26,XREAL_1:9;
A29: s3.a = 1 by A25,A27;
A30: IC s3 = 4 by A25,A27;
A31: s3.b = N-k-1 by A25,A27;
then
A32: IC s4 = 5 by A2,A28,A30,Th23;
then
A33: IC s5 = 2 by A2,Th24;
A34: s4.a = s3.a by A2,A30,Th23;
A35: s4.b = s3.b by A2,A30,Th23;
A36: s5.b = s4.b by A2,A32,Th24;
A37: s6.b = s5.b by A1,A2,A33,Th19,Th20,Th21;
A38: IC s6 = 3 by A1,A2,A33,Th19,Th20,Th21;
A39: s7.b = s6.b-s6.a by A2,A38,Th22;
A40: IC s7 = 4 by A2,A38,Th22;
then
A41: s8.b = s7.b by A2,Th23;
A42: s5.a = s4.a by A2,A32,Th24;
A43: s6.a = s5.a by A1,A2,A33,Th19,Th20,Th21;
A44: s7.a = s6.a by A2,A38,Th22;
thus
A45: for u being State of SCM st u = Comput(P,s,4*(k+1)+3) holds
u.a = 1 & u.b = N-(k+1)-1 & IC u = 4
by A29,A31,A34,A35,A36,A37,A39,A40,A42,A43,A44;
thus IC Comput(P,s,4*(k+1)+1) = 2 by A33;
thus IC Comput(P,s,4*(k+1)+2) = 3 by A38;
thus 0 < k+1 implies IC Comput(P,s,4*(k+1)) = 5 by A32;
thus Comput(P,s,4*(k+1)).b > 0 by A28,A31,A35;
thus Comput(P,s,4*(k+1)+1).b > 0 by A28,A31,A35,A36;
thus Comput(P,s,4*(k+1)+2).b > 0 by A28,A31,A35,A36,A37;
thus Comput(P,s,4*(k+1)+1).b = N-(k+1) by A31,A35,A36;
thus Comput(P,s,4*(k+1)+2).b = N-(k+1) by A31,A35,A36,A37;
thus Comput(P,s,4*(k+1)+4).b = N-(k+1)-1 by A41,A45;
end;
hereby
assume
A46: N <> 0;
let j be Nat;
assume k+1 >= N;
then per cases by XXREAL_0:1;
suppose
A47: N = k+1;
then IC s3 = 4 & s3.b = 0 by A25,NAT_1:16;
then IC s4 = 1 by A2,Th23;
then Comput(P,s,4*k+4) = Comput(P,s,4*k+4+(1+j)) by A2,Th18;
hence Comput(P,s,4*(k+1)+1+j).b = 0 by A25,A47,NAT_1:16;
end;
suppose N < k+1;
then Comput(P,s,4*k+1+(4+j)).b = 0 by A25,A46,NAT_1:13;
hence Comput(P,s,4*(k+1)+1+j).b = 0;
end;
end;
assume that
A48: N <> 0 and
A49: k+1 >= N;
let j be Nat;
per cases by A49,XXREAL_0:1;
suppose k+1 > N;
then IC Comput(P,s,4*k+(4+j)) = 1 by A25,A48,NAT_1:13;
hence IC Comput(P,s,4*(k+1)+j) = 1;
end;
suppose k+1 = N;
then IC s3 = 4 & s3.b = 0 by A25,NAT_1:16;
then IC s4 = 1 by A2,Th23;
hence IC Comput(P,s,4*(k+1)+j) = 1 by A2,Th18;
end;
end;
A50: for k being Nat holds P[k] from NAT_1:sch 2(A21,A24);
set t = Comput(P,s,4*K+3);
set t1 = Comput(P,s,4*K+3+1);
A51: K < N by A12,NAT_1:13;
then
A52: IC t = 4 by A50;
t.b = N-K-1 by A50,A51
.= 0 by A12;
then
A53: IC t1 = 1 by A2,A52,Th23;
hence P halts_on s by A3,EXTPRO_1:30;
thus Comput(P,s,1).c = A by A7,A10;
thus for k being Nat st 0 < k < N holds IC Comput(P,s,4*k) = 5 by A50;
thus for k being Nat st k < N holds
IC Comput(P,s,4*k+1) = 2 & IC Comput(P,s,4*k+2) = 3 &
IC Comput(P,s,4*k+3) = 4 &
Comput(P,s,4*k+1).b = N-k & Comput(P,s,4*k+2).b = N-k &
Comput(P,s,4*k+3).b = N-k-1 & Comput(P,s,4*k+4).b = N-k-1 &
Comput(P,s,4*k).b > 0 & Comput(P,s,4*k+1).b > 0 &
Comput(P,s,4*k+2).b > 0 by A50;
assume
A54: N <> 0;
thus LifeSpan(P,s) = 4*N by A3,A12,A52,A53,EXTPRO_1:33;
thus thesis by A50,A54;
end;
end;
:::$T+
now
let A be Integer;
set N = 0;
let P be Instruction-Sequence of SCM such that
A1: IterativeAlgorithm(MultBy(dl.2,dl.1)) c= P;
let s be 0-started State-consisting of <%1,N,A%>;
:: IC Comput(P,s,x)
IC Comput(P,s,0) = 0 by MEMSTR_0:def 12;
IC Comput(P,s,1) = 1 by A1,Th27;
IC Comput(P,s,2) = 1 by A1,Th27;
IC Comput(P,s,3) = 1 by A1,Th27;
IC Comput(P,s,4) = 1 by A1,Th27;
IC Comput(P,s,5) = 1 by A1,Th27;
:: Comput(P,s,x).a
for x being Nat holds Comput(P,s,x).a = 1 by A1,Th26;
:: Comput(P,s,x).b
Comput(P,s,0).b = 0 by Th14;
Comput(P,s,1).b = 0 by A1,Th27;
Comput(P,s,2).b = 0 by A1,Th27;
Comput(P,s,3).b = 0 by A1,Th27;
Comput(P,s,4).b = 0 by A1,Th27;
Comput(P,s,5).b = 0 by A1,Th27;
Comput(P,s,100).b = 0 by A1,Th27;
end;
now
let A be Integer;
set N = 1;
let P be Instruction-Sequence of SCM such that
A1: IterativeAlgorithm(MultBy(dl.2,dl.1)) c= P;
let s be 0-started State-consisting of <%1,N,A%>;
:: IC Comput(P,s,x)
IC Comput(P,s,0) = 0 by MEMSTR_0:def 12;
IC Comput(P,s,4*0+1) = 2 by A1,Th29;
IC Comput(P,s,4*0+2) = 3 by A1,Th29;
IC Comput(P,s,4*0+3) = 4 by A1,Th29;
IC Comput(P,s,4*1+0) = 1 by A1,Th29;
IC Comput(P,s,4*1+1) = 1 by A1,Th29;
IC Comput(P,s,4*1+2) = 1 by A1,Th29;
IC Comput(P,s,4*1+3) = 1 by A1,Th29;
IC Comput(P,s,4*1+7) = 1 by A1,Th29;
IC Comput(P,s,4*5+0) = 1 by A1,Th29;
IC Comput(P,s,4*5+1) = 1 by A1,Th29;
IC Comput(P,s,4*6+0) = 1 by A1,Th29;
IC Comput(P,s,4*22+0) = 1 by A1,Th29;
IC Comput(P,s,4*22+1) = 1 by A1,Th29;
IC Comput(P,s,4*22+2) = 1 by A1,Th29;
IC Comput(P,s,4*22+3) = 1 by A1,Th29;
IC Comput(P,s,4*22+4) = 1 by A1,Th29;
IC Comput(P,s,4*22+5) = 1 by A1,Th29;
:: Comput(P,s,x).a
for x being Nat holds Comput(P,s,x).a = 1 by A1,Th26;
:: Comput(P,s,x).b
Comput(P,s,0).b = 1 by Th14;
Comput(P,s,4*0+1).b = 1-0 by A1,Th29;
Comput(P,s,4*0+2).b = 1-0 by A1,Th29;
Comput(P,s,4*0+3).b = 1-0-1 by A1,Th29;
Comput(P,s,4*0+4).b = 1-0-1 by A1,Th29;
Comput(P,s,4*1+1+0).b = 0 by A1,Th29;
Comput(P,s,4*1+1+1).b = 0 by A1,Th29;
Comput(P,s,4*1+1+2).b = 0 by A1,Th29;
Comput(P,s,4*1+1+3).b = 0 by A1,Th29;
Comput(P,s,4*2+1+0).b = 0 by A1,Th29;
Comput(P,s,4*2+1+1).b = 0 by A1,Th29;
Comput(P,s,4*2+1+2).b = 0 by A1,Th29;
Comput(P,s,4*2+1+3).b = 0 by A1,Th29;
Comput(P,s,4*5+1+0).b = 0 by A1,Th29;
Comput(P,s,4*5+1+1).b = 0 by A1,Th29;
Comput(P,s,4*21+1+3).b = 0 by A1,Th29;
Comput(P,s,4*21+1+4).b = 0 by A1,Th29;
Comput(P,s,4*21+1+5).b = 0 by A1,Th29;
Comput(P,s,4*21+1+6).b = 0 by A1,Th29;
Comput(P,s,4*21+1+7).b = 0 by A1,Th29;
Comput(P,s,4*21+1+8).b = 0 by A1,Th29;
end;
now
let A be Integer;
set N = 5;
let P be Instruction-Sequence of SCM such that
A1: IterativeAlgorithm(MultBy(dl.2,dl.1)) c= P;
let s be 0-started State-consisting of <%1,N,A%>;
:: IC Comput(P,s,x)
IC Comput(P,s,0) = 0 by MEMSTR_0:def 12;
IC Comput(P,s,4*0+1) = 2 by A1,Th29;
IC Comput(P,s,4*0+2) = 3 by A1,Th29;
IC Comput(P,s,4*0+3) = 4 by A1,Th29;
IC Comput(P,s,4*1) = 5 by A1,Th29;
IC Comput(P,s,4*1+1) = 2 by A1,Th29;
IC Comput(P,s,4*1+2) = 3 by A1,Th29;
IC Comput(P,s,4*1+3) = 4 by A1,Th29;
IC Comput(P,s,4*2) = 5 by A1,Th29;
IC Comput(P,s,4*2+1) = 2 by A1,Th29;
IC Comput(P,s,4*2+2) = 3 by A1,Th29;
IC Comput(P,s,4*2+3) = 4 by A1,Th29;
IC Comput(P,s,4*3) = 5 by A1,Th29;
IC Comput(P,s,4*3+1) = 2 by A1,Th29;
IC Comput(P,s,4*3+2) = 3 by A1,Th29;
IC Comput(P,s,4*3+3) = 4 by A1,Th29;
IC Comput(P,s,4*4) = 5 by A1,Th29;
IC Comput(P,s,4*4+1) = 2 by A1,Th29;
IC Comput(P,s,4*4+2) = 3 by A1,Th29;
IC Comput(P,s,4*4+3) = 4 by A1,Th29;
IC Comput(P,s,4*5+0) = 1 by A1,Th29;
IC Comput(P,s,4*5+1) = 1 by A1,Th29;
IC Comput(P,s,4*6+0) = 1 by A1,Th29;
IC Comput(P,s,4*22+0) = 1 by A1,Th29;
IC Comput(P,s,4*22+1) = 1 by A1,Th29;
IC Comput(P,s,4*22+2) = 1 by A1,Th29;
IC Comput(P,s,4*22+3) = 1 by A1,Th29;
IC Comput(P,s,4*22+4) = 1 by A1,Th29;
IC Comput(P,s,4*22+5) = 1 by A1,Th29;
:: Comput(P,s,x).a
for x being Nat holds Comput(P,s,x).a = 1 by A1,Th26;
:: Comput(P,s,x).b
Comput(P,s,0).b = 5 by Th14;
Comput(P,s,4*0+1).b = 5-0 by A1,Th29;
Comput(P,s,4*0+2).b = 5-0 by A1,Th29;
Comput(P,s,4*0+3).b = 5-0-1 by A1,Th29;
Comput(P,s,4*0+4).b = 5-0-1 by A1,Th29;
Comput(P,s,4*1+1).b = 5-1 by A1,Th29;
Comput(P,s,4*1+2).b = 5-1 by A1,Th29;
Comput(P,s,4*1+3).b = 5-1-1 by A1,Th29;
Comput(P,s,4*1+4).b = 5-1-1 by A1,Th29;
Comput(P,s,4*2+1).b = 5-2 by A1,Th29;
Comput(P,s,4*2+2).b = 5-2 by A1,Th29;
Comput(P,s,4*2+3).b = 5-2-1 by A1,Th29;
Comput(P,s,4*2+4).b = 5-2-1 by A1,Th29;
Comput(P,s,4*3+1).b = 5-3 by A1,Th29;
Comput(P,s,4*3+2).b = 5-3 by A1,Th29;
Comput(P,s,4*3+3).b = 5-3-1 by A1,Th29;
Comput(P,s,4*3+4).b = 5-3-1 by A1,Th29;
Comput(P,s,4*4+1).b = 5-4 by A1,Th29;
Comput(P,s,4*4+2).b = 5-4 by A1,Th29;
Comput(P,s,4*4+3).b = 5-4-1 by A1,Th29;
Comput(P,s,4*4+4).b = 5-4-1 by A1,Th29;
Comput(P,s,4*5+1+0).b = 0 by A1,Th29;
Comput(P,s,4*5+1+1).b = 0 by A1,Th29;
Comput(P,s,4*21+1+3).b = 0 by A1,Th29;
Comput(P,s,4*21+1+4).b = 0 by A1,Th29;
Comput(P,s,4*21+1+5).b = 0 by A1,Th29;
Comput(P,s,4*21+1+6).b = 0 by A1,Th29;
Comput(P,s,4*21+1+7).b = 0 by A1,Th29;
Comput(P,s,4*21+1+8).b = 0 by A1,Th29;
end;
:::$T-
registration
let i1,i2,k,n;
let s be 0-started State-consisting of <%n,i1,i2%>;
let I be sequential 0-dl.constant Instruction of SCM;
let P be IterativeAlgorithm(I)-extending Instruction-Sequence of SCM;
cluster Comput(P,s,k).dl.0 -> natural;
coherence by Th26,PROOFS_1:def 12;
end;
theorem Th30:
(I = AddTo(dl.2,dl.1) or I = SubFrom(dl.2,dl.1) or I = MultBy(dl.2,dl.1))
implies
for s being 0-started State-consisting of <%1,n,i%>
for P being IterativeAlgorithm(I)-extending Instruction-Sequence of SCM holds
Comput(P,s,k).dl.1 is natural
proof
assume
A1: I = AddTo(c,b) or I = SubFrom(c,b) or I = MultBy(c,b);
let s be 0-started State-consisting of <%1,n,i%>;
let P be IterativeAlgorithm(I)-extending Instruction-Sequence of SCM;
A2: IterativeAlgorithm(I) c= P by PROOFS_1:def 12;
per cases;
suppose n = 0;
hence thesis by A1,A2,Th27;
end;
suppose
A3: n <> 0;
consider z being Nat such that
A4: k = 4*z or k = 4*z+1 or k = 4*z+2 or k = 4*z+3 by NUMBER02:24;
A5: now
defpred Q[Nat] means Comput(P,s,4*$1).b is natural;
A6: Q[0] by Th14;
A7: for q being Nat st Q[q] holds Q[q+1]
proof
let q be Nat such that Q[q];
per cases;
suppose
A8: q < n;
then q+1 <= n by NAT_1:13;
then
A9: n-(q+1) in NAT by INT_1:5;
Comput(P,s,4*q+4).b = n-q-1 by A1,A2,A8,Th29;
hence Comput(P,s,4*(q+1)).b is natural by A9;
end;
suppose q >= n;
then Comput(P,s,4*q+1+3).b is natural by A1,A2,A3,Th29;
hence Comput(P,s,4*(q+1)).b is natural;
end;
end;
thus for s being Nat holds Q[s] from NAT_1:sch 2(A6,A7);
end;
per cases;
suppose
A10: z < n;
then z+1 <= n by NAT_1:13;
then
A11: n-(z+1) in NAT by INT_1:5;
per cases by A4;
suppose k = 4*z;
hence thesis by A5;
end;
suppose
A12: k = 4*z+1 or k = 4*z+2;
n-z in NAT by A10,INT_1:5;
hence thesis by A1,A2,A10,A12,Th29;
end;
suppose
A13: k = 4*z+3;
n-z-1 = n-(z+1);
hence thesis by A1,A2,A10,A11,A13,Th29;
end;
end;
suppose
A14: z >= n;
per cases by A4;
suppose k = 4*z;
hence thesis by A5;
end;
suppose k = 4*z+1+0 or k = 4*z+1+1 or k = 4*z+1+2;
hence thesis by A2,A3,A14,A1,Th29;
end;
end;
end;
end;
registration
let i,k,n;
let s be 0-started State-consisting of <%1,n,i%>;
let P be IterativeAlgorithm(AddTo(dl.2,dl.1))-extending
Instruction-Sequence of SCM;
cluster Comput(P,s,k).dl.1 -> natural;
coherence by Th30;
end;
registration
let i,k,n;
let s be 0-started State-consisting of <%1,n,i%>;
let P be IterativeAlgorithm(MultBy(dl.2,dl.1))-extending
Instruction-Sequence of SCM;
cluster Comput(P,s,k).dl.1 -> natural;
coherence by Th30;
end;
scheme AddOfOneSch
{ A() -> Integer, N() -> Nat, F(object) -> Integer } :
for P being IterativeAlgorithm(AddTo(dl.2,dl.1))-extending
Instruction-Sequence of SCM
for s being 0-started State-consisting of <%1,N(),A()%> holds
(for k being Nat st k < N() holds
Comput(P,s,4*k+1).dl.2 = A() + (F(N()) - F(Comput(P,s,4*k+1).dl.1)) &
Comput(P,s,4*k+2).dl.2 = A() + (F(N()) - F(Comput(P,s,4*k+2).dl.1-'1)) &
Comput(P,s,4*k+3).dl.2 = Comput(P,s,4*k+2).dl.2 &
Comput(P,s,4*k+4).dl.2 = Comput(P,s,4*k+3).dl.2
) &
(for k,j being Nat st k >= N() holds Comput(P,s,4*k+1+j).dl.2 = F(N())) &
(Result(P,s)).dl.2 = F(N())
provided
A1: F(0) = A() and
A2: for n being Nat holds F(n+1) = (n+1) + F(n)
proof
let P be IterativeAlgorithm(AddTo(c,b))-extending
Instruction-Sequence of SCM;
A3: IterativeAlgorithm(AddTo(c,b)) c= P by PROOFS_1:def 12;
let s be 0-started State-consisting of <%1,N(),A()%>;
A4: P.1 = halt SCM by A3,Th8;
set s0 = Comput(P,s,0);
set s1 = Comput(P,s,0+1);
set s2 = Comput(P,s,1+1);
set s3 = Comput(P,s,2+1);
set s4 = Comput(P,s,3+1);
set s5 = Comput(P,s,4+1);
A5: IC s0 = 0 by MEMSTR_0:def 12;
A6: s0.b = N() by Th14;
A7: s0.c = A() by Th14;
A8: s1.b = s0.b by A3,A5,Th16;
A9: s1.c = s0.c by A3,A5,Th16;
per cases by NAT_1:6;
suppose
A10: N() = 0;
then
A11: P.IC s1 = halt SCM by A4,A3,A5,A6,Th16;
thus for k being Nat st k < N() holds
Comput(P,s,4*k+1).c = A() + (F(N()) - F(Comput(P,s,4*k+1).b)) &
Comput(P,s,4*k+2).c = A() + (F(N()) - F(Comput(P,s,4*k+2).b-'1)) &
Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c &
Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c
by A10;
defpred Q[Nat] means
for j st $1 >= N() holds Comput(P,s,4*$1+1+j).c = F(N());
A12: Q[0]
proof
let j such that
A13: 0 >= N();
A14: N() = 0 by A13;
defpred R[Nat] means Comput(P,s,4*0+1+$1).c = F(N());
A15: R[0] by A1,A7,A9,A13;
A16: for h being Nat st R[h] holds R[h+1]
proof
let h be Nat such that
A17: R[h];
1 <= h+1 by NAT_1:11;
then IC Comput(P,s,h+1) = 1 by A3,A14,Th27;
hence Comput(P,s,4*0+1+(h+1)).c = F(N()) by A3,A17,Th18;
end;
for h being Nat holds R[h] from NAT_1:sch 2(A15,A16);
hence thesis;
end;
A18: for z being Nat st Q[z] holds Q[z+1]
proof
let z be Nat such that
A19: Q[z];
let j;
assume z+1 >= N();
Comput(P,s,4*z+1+(j+4)).c = F(N()) by A10,A19;
hence Comput(P,s,4*(z+1)+1+j).c = F(N());
end;
for z being Nat holds Q[z] from NAT_1:sch 2(A12,A18);
hence for k,j being Nat st k >= N() holds Comput(P,s,4*k+1+j).c = F(N());
thus (Result(P,s)).c = F(N()) by A1,A7,A9,A10,A11,EXTPRO_1:7;
end;
suppose ex K being Nat st N() = K+1;
then consider K being Nat such that
A20: N() = K+1;
A21: IC s1 = 2 by A3,A5,A6,A20,Th16;
A22: IC s2 = 3 by A3,A21,Th19;
A23: s2.c = s1.c+s1.b by A3,A21,Th19;
A24: IC s3 = 4 by A3,A22,Th22;
A25: s3.c = s2.c by A3,A22,Th22;
A26: s4.c = s3.c by A3,A24,Th23;
defpred P[Nat] means ($1 < N() implies
Comput(P,s,4*$1+1).c = A() + (F(N()) - F(Comput(P,s,4*$1+1).b)) &
Comput(P,s,4*$1+2).c = A() + (F(N()) - F(Comput(P,s,4*$1+2).b-'1)) &
Comput(P,s,4*$1+3).c = Comput(P,s,4*$1+2).c &
Comput(P,s,4*$1+4).c = Comput(P,s,4*$1+3).c) &
for j being Nat st $1 >= N() holds Comput(P,s,4*$1+1+j).c = F(N());
A27: P[0]
proof
hereby
assume 0 < N();
then consider k such that
A28: N() = k+1 by NAT_1:6;
A29: F(k+1) = (k+1) + F(k) by A2;
thus Comput(P,s,4*0+1).c = A() + (F(N()) - F(Comput(P,s,4*0+1).b))
by A6,A7,A8,A9;
A30: Comput(P,s,4*0+2).b = N()-0 by A3,A28,Th29;
then 0+1 <= Comput(P,s,4*0+2).b by A28,NAT_1:13;
then Comput(P,s,4*0+2).b-'1 = Comput(P,s,4*0+2).b-1 by XREAL_1:233;
hence Comput(P,s,4*0+2).c = A() + (F(N()) - F(Comput(P,s,4*0+2).b-'1))
by A6,A7,A28,A8,A9,A23,A29,A30;
thus Comput(P,s,4*0+3).c = Comput(P,s,4*0+2).c by A25;
thus Comput(P,s,4*0+4).c = Comput(P,s,4*0+3).c by A26;
end;
thus for j being Nat st 0 >= N() holds Comput(P,s,4*0+1+j).c = F(N())
by A20;
end;
A31: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A32: (k < N() implies
Comput(P,s,4*k+1).c = A() + (F(N()) - F(Comput(P,s,4*k+1).b)) &
Comput(P,s,4*k+2).c = A() + (F(N()) - F(Comput(P,s,4*k+2).b-'1)) &
Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c &
Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c) &
for j being Nat st k >= N() holds Comput(P,s,4*k+1+j).c = F(N());
set t = Comput(P,s,4*k+2);
set S = 4*k+3;
set s3 = Comput(P,s,S);
set s4 = Comput(P,s,S+1);
set s5 = Comput(P,s,S+1+1);
set s6 = Comput(P,s,S+2+1);
set s7 = Comput(P,s,S+3+1);
set s8 = Comput(P,s,S+4+1);
hereby
assume
A33: k+1 < N();
then
A34: k < N() by XXREAL_0:2,NAT_1:16;
A35: N()-(k+1) > k+1-(k+1) by A33,XREAL_1:9;
A36: IC s3 = 4 by A3,A34,Th29;
A37: s3.b = N()-k-1 by A3,A34,Th29;
then
A38: IC s4 = 5 by A3,A35,A36,Th23;
then
A39: IC s5 = 2 by A3,Th24;
A40: s4.b = s3.b by A3,A36,Th23;
A41: s5.b = s4.b by A3,A38,Th24;
A42: IC s6 = 3 by A3,A39,Th19;
A43: s3.c = A() + (F(N()) - F(t.b-'1)) by A32,A34;
A44: s4.c = s3.c by A3,A36,Th23;
A45: s5.c = s4.c by A3,A38,Th24;
A46: s6.c = s5.c+s5.b by A3,A39,Th19;
A47: s7.c = s6.c by A3,A42,Th22;
A48: N()-k-1-1 >= 0 by A35,INT_1:52;
then reconsider W = N()-k-2 as Element of NAT by INT_1:3;
A49: F(W+1) = (W+1) + F(W) by A2;
A50: N()-k-1-'1 = N()-k-1-1 by A48,XREAL_0:def 2;
A51: t.b = N()-k by A3,A34,Th29;
then 0+1 <= t.b by A34,NAT_1:13,XREAL_1:50;
then
A52: t.b-'1 = t.b-1 by XREAL_1:233;
thus Comput(P,s,4*(k+1)+1).c
= A() + (F(N()) - F(Comput(P,s,4*(k+1)+1).b))
by A40,A41,A37,A32,A34,A45,A51,A52;
A53: Comput(P,s,4*(k+1)+2).b = N()-(k+1) by A3,A33,Th29;
thus Comput(P,s,4*(k+1)+2).c
= A() + (F(N()) - F(Comput(P,s,4*(k+1)+2).b-'1))
by A37,A43,A40,A41,A44,A45,A46,A53,A50,A52,A49,A51;
thus Comput(P,s,4*(k+1)+3).c = Comput(P,s,4*(k+1)+2).c by A47;
A54: 4*(k+1)+3+1 = 4*(k+1)+4;
IC Comput(P,s,4*(k+1)+3) = 4 by A3,A33,Th29;
hence Comput(P,s,4*(k+1)+4).c = Comput(P,s,4*(k+1)+3).c
by A3,A54,Th23;
end;
let j be Nat;
assume k+1 >= N();
then per cases by XXREAL_0:1;
suppose
A55: k+1 = N();
A56: k < k+1 by NAT_1:16;
then
A57: t.b = N()-k by A3,A55,Th29
.= 1 by A55;
then t.b-'1 = t.b-1 by XREAL_1:233;
then
A58: s3.c = F(N()) by A1,A32,A55,A56,A57;
A59: IC s3 = 4 by A3,A55,A56,Th29;
s3.b = N()-k-1 by A3,A55,A56,Th29
.= 0 by A55;
then IC s4 = 1 by A3,A59,Th23;
then Comput(P,s,4*k+4+(j+1)) = s4 by A3,Th18;
hence Comput(P,s,4*(k+1)+1+j).c = F(N()) by A58,A3,A59,Th23;
end;
suppose k+1 > N();
then Comput(P,s,4*k+1+(j+4)).c = F(N()) by A32,NAT_1:13;
hence Comput(P,s,4*(k+1)+1+j).c = F(N());
end;
end;
A60: for k being Nat holds P[k] from NAT_1:sch 2(A27,A31);
set t2 = Comput(P,s,4*K+2);
set t3 = Comput(P,s,4*K+3);
set t4 = Comput(P,s,4*K+3+1);
A61: K < N() by A20,NAT_1:13;
then
A62: IC t3 = 4 by A3,Th29;
t3.b = N()-K-1 by A3,A61,Th29
.= 0 by A20;
then
A63: IC t4 = 1 by A3,A62,Th23;
A64: t2.b = N()-K by A3,A61,Th29;
then
A65: t2.b-'1 = t2.b-1 by A20,XREAL_1:233;
A66: t3.c = Comput(P,s,4*K+2).c by A60,A61
.= A() + (F(N()) - F(t2.b-'1)) by A60,A61
.= F(K+1) by A1,A20,A64,A65;
A67: P.IC t4 = halt SCM by A4,A63;
thus for k being Nat st k < N() holds
Comput(P,s,4*k+1).c = A() + (F(N()) - F(Comput(P,s,4*k+1).b)) &
Comput(P,s,4*k+2).c = A() + (F(N()) - F(Comput(P,s,4*k+2).b-'1)) &
Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c &
Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c
by A60;
thus for k,j being Nat st k >= N() holds Comput(P,s,4*k+1+j).c = F(N())
by A60;
t4.c = t3.c by A3,A62,Th23;
hence (Result(P,s)).c = F(N()) by A20,A66,A67,EXTPRO_1:7;
end;
end;
scheme MultOfOneSch
{ A() -> Integer, N() -> Nat, F(object) -> Integer } :
for P being IterativeAlgorithm(MultBy(dl.2,dl.1))-extending
Instruction-Sequence of SCM
for s being 0-started State-consisting of <%1,N(),A()%> holds
(for k being Nat st k < N() holds
Comput(P,s,4*k+1).dl.2 = A() * (F(N()) / F(Comput(P,s,4*k+1).dl.1)) &
Comput(P,s,4*k+2).dl.2 = A() * (F(N()) / F(Comput(P,s,4*k+2).dl.1-'1)) &
Comput(P,s,4*k+3).dl.2 = Comput(P,s,4*k+2).dl.2 &
Comput(P,s,4*k+4).dl.2 = Comput(P,s,4*k+3).dl.2
) &
(for k,j being Nat st k >= N() holds Comput(P,s,4*k+1+j).dl.2 = F(N())) &
(Result(P,s)).dl.2 = F(N())
provided
A1: F(0) = A() and
A2: A() <> 0 and
A3: for n being Nat holds F(n+1) = (n+1) * F(n)
proof
let P be IterativeAlgorithm(MultBy(c,b))-extending
Instruction-Sequence of SCM;
A4: IterativeAlgorithm(MultBy(c,b)) c= P by PROOFS_1:def 12;
let s be 0-started State-consisting of <%1,N(),A()%>;
A5: P.1 = halt SCM by A4,Th8;
set s0 = Comput(P,s,0);
set s1 = Comput(P,s,0+1);
set s2 = Comput(P,s,1+1);
set s3 = Comput(P,s,2+1);
set s4 = Comput(P,s,3+1);
set s5 = Comput(P,s,4+1);
A6: IC s0 = 0 by MEMSTR_0:def 12;
A7: s0.b = N() by Th14;
A8: s0.c = A() by Th14;
A9: s1.b = s0.b by A4,A6,Th16;
A10: s1.c = s0.c by A4,A6,Th16;
per cases by NAT_1:6;
suppose
A11: N() = 0;
then
A12: P.IC s1 = halt SCM by A5,A4,A6,A7,Th16;
thus for k being Nat st k < N() holds
Comput(P,s,4*k+1).c = A() * (F(N()) / F(Comput(P,s,4*k+1).b)) &
Comput(P,s,4*k+2).c = A() * (F(N()) / F(Comput(P,s,4*k+2).b-'1)) &
Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c &
Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c
by A11;
defpred Q[Nat] means
for j st $1 >= N() holds Comput(P,s,4*$1+1+j).c = F(N());
A13: Q[0]
proof
let j such that
A14: 0 >= N();
A15: N() = 0 by A14;
defpred R[Nat] means Comput(P,s,4*0+1+$1).c = F(N());
A16: R[0] by A1,A8,A10,A14;
A17: for h being Nat st R[h] holds R[h+1]
proof
let h be Nat such that
A18: R[h];
1 <= h+1 by NAT_1:11;
then IC Comput(P,s,h+1) = 1 by A4,A15,Th27;
hence Comput(P,s,4*0+1+(h+1)).c = F(N()) by A4,A18,Th18;
end;
for h being Nat holds R[h] from NAT_1:sch 2(A16,A17);
hence thesis;
end;
A19: for z being Nat st Q[z] holds Q[z+1]
proof
let z be Nat such that
A20: Q[z];
let j;
assume z+1 >= N();
Comput(P,s,4*z+1+(j+4)).c = F(N()) by A11,A20;
hence Comput(P,s,4*(z+1)+1+j).c = F(N());
end;
for z being Nat holds Q[z] from NAT_1:sch 2(A13,A19);
hence for k,j being Nat st k >= N() holds Comput(P,s,4*k+1+j).c = F(N());
thus (Result(P,s)).c = F(N()) by A1,A8,A10,A11,A12,EXTPRO_1:7;
end;
suppose ex K being Nat st N() = K+1;
then consider K being Nat such that
A21: N() = K+1;
A22: IC s1 = 2 by A4,A6,A7,A21,Th16;
A23: IC s2 = 3 by A4,A22,Th21;
A24: s2.c = s1.c*s1.b by A4,A22,Th21;
A25: IC s3 = 4 by A4,A23,Th22;
A26: s3.c = s2.c by A4,A23,Th22;
A27: s4.c = s3.c by A4,A25,Th23;
defpred P[Nat] means ($1 < N() implies
Comput(P,s,4*$1+1).c = A() * (F(N()) / F(Comput(P,s,4*$1+1).b)) &
Comput(P,s,4*$1+2).c = A() * (F(N()) / F(Comput(P,s,4*$1+2).b-'1)) &
Comput(P,s,4*$1+3).c = Comput(P,s,4*$1+2).c &
Comput(P,s,4*$1+4).c = Comput(P,s,4*$1+3).c) &
for j being Nat st $1 >= N() holds Comput(P,s,4*$1+1+j).c = F(N());
A28: P[0]
proof
hereby
assume 0 < N();
then consider k such that
A29: N() = k+1 by NAT_1:6;
A30: F(k+1) = (k+1) * F(k) by A3;
A31: for n being Nat holds F(n) <> 0
proof
defpred Q[Nat] means F($1) <> 0;
A32: Q[0] by A1,A2;
A33: for z being Nat st Q[z] holds Q[z+1]
proof
let z be Nat;
F(z+1) = (z+1) * F(z) by A3;
hence thesis by XCMPLX_1:6;
end;
for z being Nat holds Q[z] from NAT_1:sch 2(A32,A33);
hence thesis;
end;
thus Comput(P,s,4*0+1).c = A() * (F(N()) / F(Comput(P,s,4*0+1).b))
by A7,A8,A9,A10,A31,XCMPLX_1:88;
A34: Comput(P,s,4*0+2).b = N()-0 by A4,A29,Th29;
then 0+1 <= Comput(P,s,4*0+2).b by A29,NAT_1:13;
then Comput(P,s,4*0+2).b-'1 = Comput(P,s,4*0+2).b-1 by XREAL_1:233;
hence Comput(P,s,4*0+2).c = A() * (F(N()) / F(Comput(P,s,4*0+2).b-'1))
by A7,A8,A29,A9,A10,A24,A30,A31,A34,XCMPLX_1:89;
thus Comput(P,s,4*0+3).c = Comput(P,s,4*0+2).c by A26;
thus Comput(P,s,4*0+4).c = Comput(P,s,4*0+3).c by A27;
end;
thus for j being Nat st 0 >= N() holds Comput(P,s,4*0+1+j).c = F(N())
by A21;
end;
A35: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A36: (k < N() implies
Comput(P,s,4*k+1).c = A() * (F(N()) / F(Comput(P,s,4*k+1).b)) &
Comput(P,s,4*k+2).c = A() * (F(N()) / F(Comput(P,s,4*k+2).b-'1)) &
Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c &
Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c) &
for j being Nat st k >= N() holds Comput(P,s,4*k+1+j).c = F(N());
set t = Comput(P,s,4*k+2);
set S = 4*k+3;
set s3 = Comput(P,s,S);
set s4 = Comput(P,s,S+1);
set s5 = Comput(P,s,S+1+1);
set s6 = Comput(P,s,S+2+1);
set s7 = Comput(P,s,S+3+1);
set s8 = Comput(P,s,S+4+1);
hereby
assume
A37: k+1 < N();
then
A38: k < N() by XXREAL_0:2,NAT_1:16;
A39: N()-(k+1) > k+1-(k+1) by A37,XREAL_1:9;
A40: IC s3 = 4 by A4,A38,Th29;
A41: s3.b = N()-k-1 by A4,A38,Th29;
then
A42: IC s4 = 5 by A4,A39,A40,Th23;
then
A43: IC s5 = 2 by A4,Th24;
A44: s4.b = s3.b by A4,A40,Th23;
A45: s5.b = s4.b by A4,A42,Th24;
A46: IC s6 = 3 by A4,A43,Th21;
A47: s3.c = A() * (F(N()) / F(t.b-'1)) by A36,A38;
A48: s4.c = s3.c by A4,A40,Th23;
A49: s5.c = s4.c by A4,A42,Th24;
A50: s6.c = s5.c*s5.b by A4,A43,Th21;
A51: s7.c = s6.c by A4,A46,Th22;
N()-k-1-1 >= 0 by A39,INT_1:52;
then reconsider W = N()-k-2 as Element of NAT by INT_1:3;
F(W+1) = (W+1) * F(W) by A3;
then
A52: F(N()) / F(W) = F(N()) / (F(N()-k-1) / (N()-k-1)) by XCMPLX_1:89
.= F(N()) * (N()-k-1) / (F(N()-k-1)) by XCMPLX_1:77;
A53: t.b = N()-k by A4,A38,Th29;
then 0+1 <= t.b by A38,NAT_1:13,XREAL_1:50;
then
A54: t.b-'1 = t.b-1 by XREAL_1:233;
hence Comput(P,s,4*(k+1)+1).c
= A() * (F(N()) / F(Comput(P,s,4*(k+1)+1).b))
by A44,A45,A41,A36,A38,A49,A53;
A55: Comput(P,s,4*(k+1)+2).b = N()-(k+1) by A4,A37,Th29;
then 0+1 <= s6.b by A39,NAT_1:13;
then s6.b-'1 = s6.b-1 by XREAL_1:233;
then
A56: (F(N()) / F(t.b-1)) * (N()-k-1)
= (F(N()) / F(Comput(P,s,4*(k+1)+2).b-'1)) by A52,A53,A55;
thus Comput(P,s,4*(k+1)+2).c
= A() * (F(N()) / F(Comput(P,s,4*(k+1)+2).b-'1))
by A41,A47,A44,A45,A48,A49,A50,A54,A56;
thus Comput(P,s,4*(k+1)+3).c = Comput(P,s,4*(k+1)+2).c by A51;
A57: 4*(k+1)+3+1 = 4*(k+1)+4;
IC Comput(P,s,4*(k+1)+3) = 4 by A4,A37,Th29;
hence Comput(P,s,4*(k+1)+4).c = Comput(P,s,4*(k+1)+3).c
by A4,A57,Th23;
end;
let j be Nat;
assume k+1 >= N();
then per cases by XXREAL_0:1;
suppose
A58: k+1 = N();
A59: k < k+1 by NAT_1:16;
then
A60: t.b = N()-k by A4,A58,Th29
.= 1 by A58;
then t.b-'1 = t.b-1 by XREAL_1:233;
then
A61: s3.c = A() * F(N()) / A() by A1,A36,A58,A59,A60
.= F(N()) by A2,XCMPLX_1:89;
A62: IC s3 = 4 by A4,A58,A59,Th29;
s3.b = N()-k-1 by A4,A58,A59,Th29
.= 0 by A58;
then IC s4 = 1 by A4,A62,Th23;
then Comput(P,s,4*k+4+(j+1)) = s4 by A4,Th18;
hence Comput(P,s,4*(k+1)+1+j).c = F(N()) by A61,A4,A62,Th23;
end;
suppose k+1 > N();
then Comput(P,s,4*k+1+(j+4)).c = F(N()) by A36,NAT_1:13;
hence Comput(P,s,4*(k+1)+1+j).c = F(N());
end;
end;
A63: for k being Nat holds P[k] from NAT_1:sch 2(A28,A35);
set t2 = Comput(P,s,4*K+2);
set t3 = Comput(P,s,4*K+3);
set t4 = Comput(P,s,4*K+3+1);
A64: K < N() by A21,NAT_1:13;
then
A65: IC t3 = 4 by A4,Th29;
t3.b = N()-K-1 by A4,A64,Th29
.= 0 by A21;
then
A66: IC t4 = 1 by A4,A65,Th23;
A67: t2.b = N()-K by A4,A64,Th29;
then
A68: t2.b-'1 = t2.b-1 by A21,XREAL_1:233;
A69: t3.c = Comput(P,s,4*K+2).c by A63,A64
.= A() * (F(N()) / F(t2.b-'1)) by A63,A64
.= F(K+1) by A1,A2,A21,A67,A68,XCMPLX_1:87;
thus for k being Nat st k < N() holds
Comput(P,s,4*k+1).c = A() * (F(N()) / F(Comput(P,s,4*k+1).b)) &
Comput(P,s,4*k+2).c = A() * (F(N()) / F(Comput(P,s,4*k+2).b-'1)) &
Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c &
Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c
by A63;
thus for k,j being Nat st k >= N() holds Comput(P,s,4*k+1+j).c = F(N())
by A63;
t4.c = t3.c by A4,A65,Th23;
hence (Result(P,s)).c = F(N()) by A5,A21,A69,A66,EXTPRO_1:7;
end;
end;
deffunc T(Nat) = Triangle $1;
theorem Th31:
for P being IterativeAlgorithm(AddTo(dl.2,dl.1))-extending
Instruction-Sequence of SCM
for s being 0-started State-consisting of <%1,n,0%> holds
(for k being Nat st k < n holds
Comput(P,s,4*k+1).dl.2 = (Triangle n) - Triangle(Comput(P,s,4*k+1).dl.1) &
Comput(P,s,4*k+2).dl.2
= (Triangle n) - Triangle(Comput(P,s,4*k+2).dl.1-'1) &
Comput(P,s,4*k+3).dl.2 = Comput(P,s,4*k+2).dl.2 &
Comput(P,s,4*k+4).dl.2 = Comput(P,s,4*k+3).dl.2
) &
(for k,j being Nat st k >= n holds Comput(P,s,4*k+1+j).dl.2 = Triangle n) &
(Result(P,s)).dl.2 = Triangle n
proof
let P be IterativeAlgorithm(AddTo(c,b))-extending
Instruction-Sequence of SCM;
let s be 0-started State-consisting of <%1,n,0%>;
A1: T(0) = 0;
A2: for n being Nat holds T(n+1) = (n+1) + T(n) by NUMPOLY1:10;
A3: for P being IterativeAlgorithm(AddTo(dl.2,dl.1))-extending
Instruction-Sequence of SCM
for s being 0-started State-consisting of <%1,n,0%> holds
(for k being Nat st k < n holds
Comput(P,s,4*k+1).dl.2 = 0 + (T(n) - T(Comput(P,s,4*k+1).dl.1)) &
Comput(P,s,4*k+2).dl.2 = 0 + (T(n) - T(Comput(P,s,4*k+2).dl.1-'1)) &
Comput(P,s,4*k+3).dl.2 = Comput(P,s,4*k+2).dl.2 &
Comput(P,s,4*k+4).dl.2 = Comput(P,s,4*k+3).dl.2
) &
(for k,j being Nat st k >= n holds Comput(P,s,4*k+1+j).dl.2 = T(n)) &
(Result(P,s)).dl.2 = T(n) from AddOfOneSch(A1,A2);
hereby
let k be Nat;
assume
A4: k < n;
thus Comput(P,s,4*k+1).c = 0 + (T(n)-T(Comput(P,s,4*k+1).b)) by A3,A4
.= T(n) - T(Comput(P,s,4*k+1).b);
thus Comput(P,s,4*k+2).c = 0 + (T(n)-T(Comput(P,s,4*k+2).b-'1)) by A3,A4
.= T(n) - T(Comput(P,s,4*k+2).b-'1);
thus Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c by A3,A4;
thus Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c by A3,A4;
end;
thus thesis by A3;
end;
deffunc F(Nat) = $1!;
theorem Th32:
for P being IterativeAlgorithm(MultBy(dl.2,dl.1))-extending
Instruction-Sequence of SCM
for s being 0-started State-consisting of <%1,n,1%> holds
(for k being Nat st k < n holds
Comput(P,s,4*k+1).dl.2 = n! / ((Comput(P,s,4*k+1).dl.1)!) &
Comput(P,s,4*k+2).dl.2 = n! / ((Comput(P,s,4*k+2).dl.1-'1)!) &
Comput(P,s,4*k+3).dl.2 = Comput(P,s,4*k+2).dl.2 &
Comput(P,s,4*k+4).dl.2 = Comput(P,s,4*k+3).dl.2
) &
(for k,j being Nat st k >= n holds Comput(P,s,4*k+1+j).dl.2 = n!) &
(Result(P,s)).dl.2 = n!
proof
let P be IterativeAlgorithm(MultBy(c,b))-extending
Instruction-Sequence of SCM;
let s be 0-started State-consisting of <%1,n,1%>;
A1: F(0) = 1 by NEWTON:12;
A2: 1 <> 0;
A3: for n being Nat holds F(n+1) = (n+1) * F(n) by NEWTON:15;
A4: for P being IterativeAlgorithm(MultBy(c,b))-extending
Instruction-Sequence of SCM
for s being 0-started State-consisting of <%1,n,1%> holds
(for k being Nat st k < n holds
Comput(P,s,4*k+1).c = 1 * (F(n) / F(Comput(P,s,4*k+1).b)) &
Comput(P,s,4*k+2).c = 1 * (F(n) / F(Comput(P,s,4*k+2).b-'1)) &
Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c &
Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c
) &
(for k,j being Nat st k >= n holds Comput(P,s,4*k+1+j).dl.2 = F(n)) &
(Result(P,s)).c = F(n) from MultOfOneSch(A1,A2,A3);
hereby
let k be Nat;
assume
A5: k < n;
thus Comput(P,s,4*k+1).c = 1 * (F(n)/F(Comput(P,s,4*k+1).b)) by A4,A5
.= F(n) / F(Comput(P,s,4*k+1).b);
thus Comput(P,s,4*k+2).c = 1 * (F(n)/F(Comput(P,s,4*k+2).b-'1)) by A4,A5
.= F(n) / F(Comput(P,s,4*k+2).b-'1);
thus Comput(P,s,4*k+3).c = Comput(P,s,4*k+2).c by A4,A5;
thus Comput(P,s,4*k+4).c = Comput(P,s,4*k+3).c by A4,A5;
end;
thus thesis by A4;
end;
begin :: Examples
scheme PartFuncFinPartStEx { i1,i2() -> Integer, F(object) -> Integer }:
ex f being PartFunc of FinPartSt SCM, FinPartSt SCM st
for p,q being FinPartState of SCM holds [p,q] in f iff
ex n being Nat st p = (dl.0,dl.1,dl.2) --> (i1(),n,i2()) & q = dl.2 .--> F(n)
proof
defpred P[object,object] means
ex n being Nat st $1 = (a,b,c) --> (i1(),n,i2()) & $2 = c .--> F(n);
A1: for p,q1,q2 being object st P[p,q1] & P[p,q2] holds q1 = q2
proof
let p,q1,q2 be object;
given n1 being Nat such that
A2: p = (a,b,c) --> (i1(),n1,i2()) and
A3: q1 = c .--> F(n1);
given n2 being Nat such that
A4: p = (a,b,c) --> (i1(),n2,i2()) and
A5: q2 = c .--> F(n2);
n1 = ((a,b,c) --> (i1(),n1,i2())).b by FUNCT_4:135,AMI_3:10
.= n2 by A2,A4,FUNCT_4:135,AMI_3:10;
hence thesis by A3,A5;
end;
consider f being Function such that
A6: for p,q being object holds [p,q] in f iff p in FinPartSt SCM & P[p,q]
from FUNCT_1:sch 1(A1);
A7: rng f c= FinPartSt SCM
proof
let q be object;
assume q in rng f;
then consider p being object such that
A8: [p,q] in f by XTUPLE_0:def 13;
ex n being Nat st p = (a,b,c) --> (i1(),n,i2()) & q = c .--> F(n)
by A6,A8;
hence thesis by MEMSTR_0:75;
end;
dom f c= FinPartSt SCM
proof
let e be object;
assume e in dom f;
then [e,f.e] in f by FUNCT_1:1;
hence thesis by A6;
end;
then reconsider f as PartFunc of FinPartSt SCM, FinPartSt SCM
by A7,RELSET_1:4;
take f;
let p,q be FinPartState of SCM;
thus [p,q] in f implies ex n being Nat st p = (a,b,c) --> (i1(),n,i2()) &
q = c .--> F(n) by A6;
thus thesis by A6,MEMSTR_0:75;
end;
scheme PartFuncFinPartStUn { i1,i2() -> Integer, F(object) -> Integer } :
for f1, f2 being PartFunc of FinPartSt SCM, FinPartSt SCM st
(for p,q being FinPartState of SCM holds [p,q] in f1 iff
ex n being Nat st
p = (dl.0,dl.1,dl.2) --> (i1(),n,i2()) & q = dl.2 .--> F(n)) &
(for p,q being FinPartState of SCM holds [p,q] in f2 iff
ex n being Nat st
p = (dl.0,dl.1,dl.2) --> (i1(),n,i2()) & q = dl.2 .--> F(n))
holds f1 = f2
proof
defpred P[object,object] means
ex n being Nat st $1 = (a,b,c) --> (i1(),n,i2()) & $2 = c .--> F(n);
let f1,f2 be PartFunc of FinPartSt SCM, FinPartSt SCM such that
A1: for p,q being FinPartState of SCM holds [p,q] in f1 iff P[p,q] and
A2: for p,q being FinPartState of SCM holds [p,q] in f2 iff P[p,q];
A3: for p,q being Element of FinPartSt SCM holds [p,q] in f2 iff P[p,q]
proof
let p,q being Element of FinPartSt SCM;
thus [p,q] in f2 implies P[p,q]
proof
assume
A4: [p,q] in f2;
reconsider p,q as FinPartState of SCM by MEMSTR_0:76;
P[p,q] by A2,A4;
hence thesis;
end;
thus thesis by A2;
end;
A5: for p,q being Element of FinPartSt SCM holds [p,q] in f1 iff P[p,q]
proof
let p,q being Element of FinPartSt SCM;
thus [p,q] in f1 implies P[p,q]
proof
assume
A6: [p,q] in f1;
reconsider p,q as FinPartState of SCM by MEMSTR_0:76;
P[p,q] by A1,A6;
hence thesis;
end;
thus thesis by A1;
end;
thus f1 = f2 from RELSET_1:sch 4(A5,A3);
end;
definition
func powerSCMFunction -> PartFunc of FinPartSt SCM, FinPartSt SCM means :Def5
:
for p,q being FinPartState of SCM holds [p,q] in it iff
ex n being Nat st p = (dl.0,dl.1,dl.2) --> (1,n,1) & q = dl.2 .--> (n!);
existence from PartFuncFinPartStEx;
uniqueness from PartFuncFinPartStUn;
end;
set pf = powerSCMFunction;
theorem Th33:
for p being object holds p in dom powerSCMFunction iff
ex n being Nat st p = (dl.0,dl.1,dl.2) --> (1,n,1)
proof
let p be object;
A1: p in dom pf iff [p,pf.p] in pf by FUNCT_1:1;
hereby
assume
A2: p in dom pf;
then pf.p in FinPartSt SCM by PARTFUN1:4;
then
A3: pf.p is FinPartState of SCM by MEMSTR_0:76;
p is FinPartState of SCM by A2,MEMSTR_0:76;
then ex n being Nat st p = (a,b,c) --> (1,n,1) & pf.p = c .--> F(n)
by A1,A2,A3,Def5;
hence ex n being Nat st p = (a,b,c) --> (1,n,1);
end;
given n being Nat such that
A4: p = (a,b,c) --> (1,n,1);
[p,c.-->F(n)] in pf by A4,Def5;
hence thesis by FUNCT_1:1;
end;
set q = IterativeAlgorithm(MultBy(c,b));
theorem Th34:
powerSCMFunction.((dl.0,dl.1,dl.2) --> (1,n,1)) = dl.2 .--> (n!)
proof
[ (a,b,c) --> (1,n,1), c.-->F(n) ] in pf by Def5;
hence thesis by FUNCT_1:1;
end;
scheme AutonomicSch
{ f() -> PartFunc of FinPartSt SCM, FinPartSt SCM,
I() -> Instruction of SCM,
F(object) -> Nat }:
for x being FinPartState of SCM st x in dom f() holds
Initialize x is IterativeAlgorithm(I())-autonomic
provided
A1: I() = AddTo(dl.2,dl.1) or I() = SubFrom(dl.2,dl.1) or
I() = MultBy(dl.2,dl.1) and
A2: for x being object st x in dom f()
ex n being Nat st x = (dl.0,dl.1,dl.2) --> (1,n,F(n)) and
A3: for P,Q being Instruction-Sequence of SCM st
IterativeAlgorithm(I()) c= P & IterativeAlgorithm(I()) c= Q
for x being FinPartState of SCM st x in dom f()
for s1,s2 being State of SCM st Initialize x c= s1 & Initialize x c= s2
for k being Nat holds Comput(P,s1,k).dl.2 = Comput(Q,s2,k).dl.2
proof
set q = IterativeAlgorithm(I());
let x be FinPartState of SCM;
assume
A4: x in dom f();
then consider n being Nat such that
A5: x = (a,b,c) --> (1,n,F(n)) by A2;
let P,Q be Instruction-Sequence of SCM such that
A6: q c= P and
A7: q c= Q;
reconsider P1 = P as q-extending Instruction-Sequence of SCM
by A6,PROOFS_1:def 12;
reconsider Q1 = Q as q-extending Instruction-Sequence of SCM
by A7,PROOFS_1:def 12;
let s1,s2 be State of SCM such that
A8: Initialize x c= s1 and
A9: Initialize x c= s2;
let k be Nat;
defpred P[Nat] means
IC Comput(P,s1,$1) = IC Comput(Q,s2,$1) &
Comput(P,s1,$1).a = Comput(Q,s2,$1).a &
Comput(P,s1,$1).b = Comput(Q,s2,$1).b &
Comput(P,s1,$1).c = Comput(Q,s2,$1).c;
A10: s1 is 0-started by A8,MEMSTR_0:17;
A11: s1 is State-consisting of <%1,n,F(n)%> by A5,A8,Th15;
reconsider S1 = s1 as 0-started State-consisting of <%1,n,F(n)%>
by A5,A8,Th15,MEMSTR_0:17;
A12: dom(Comput(P,s1,k)) = the carrier of SCM by PARTFUN1:def 2
.= dom(Comput(Q,s2,k)) by PARTFUN1:def 2;
A13: s2 is 0-started by A9,MEMSTR_0:17;
A14: s2 is State-consisting of <%1,n,F(n)%> by A5,A9,Th15;
reconsider S2 = s2 as 0-started State-consisting of <%1,n,F(n)%>
by A5,A9,Th15,MEMSTR_0:17;
A15: P[0]
proof
thus IC Comput(P,s1,0) = IC Comput(Q,s2,0) by A10,A13;
thus Comput(P,s1,0).a = 1 by A10,A11,Th14
.= Comput(Q,s2,0).a by A13,A14,Th14;
thus Comput(P,s1,0).b = n by A10,A11,Th14
.= Comput(Q,s2,0).b by A13,A14,Th14;
thus Comput(P,s1,0).c = F(n) by A10,A11,Th14
.= Comput(Q,s2,0).c by A13,A14,Th14;
end;
A16: for i,j being Nat st P[4*i] & j <> 0 & j <= 4 holds P[4*i+j]
proof
let i,j be Nat;
set tp = Comput(P,s1,4*i);
set tq = Comput(Q,s2,4*i);
assume that
A17: IC tp = IC tq and
tp.a = tq.a and
A18: tp.b = tq.b and
A19: tp.c = tq.c;
assume that
A20: j <> 0 and
A21: j <= 4;
A22: j = 0 or ... or j = 4 by A21;
A23: now
let z,j be Nat;
thus Comput(P,s1,z).a = 1 by A1,A6,A10,A11,Th26
.= Comput(Q,s2,4*i+j).a by A1,A7,A13,A14,Th26;
end;
per cases by A20,A22;
suppose that
A24: n = 0 and
A25: j = 1 or j = 2 or j = 3 or j = 4;
A26: 4*i+1 <= 4*i+1+1 by NAT_1:11;
4*i+2 <= 4*i+2+1 by NAT_1:11;
then
A27: 1 <= 4*i+3 by NAT_1:11;
4*i+3 <= 4*i+3+1 by NAT_1:11;
then
A28: 1 <= 4*i+j by A25,A26,A27,NAT_1:11;
hence IC Comput(P,s1,4*i+j) = 1 by A1,A6,A10,A11,A24,Th27
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A24,A28,Th27;
thus Comput(P,s1,4*i+j).a = Comput(Q,s2,4*i+j).a by A23;
thus Comput(P,s1,4*i+j).b = 0 by A1,A6,A10,A11,A24,Th27
.= Comput(Q,s2,4*i+j).b by A1,A7,A13,A14,A24,Th27;
thus Comput(P,s1,4*i+j).c = F(n) by A1,A6,A10,A11,A24,Th27
.= Comput(Q,s2,4*i+j).c by A1,A7,A13,A14,A24,Th27;
end;
suppose
A29: n <> 0;
A30: now
defpred Q[Nat] means IC Comput(P,s1,4*$1) = IC Comput(Q,s2,4*$1);
A31: Q[0] by A10,A13;
A32: for z being Nat st Q[z] holds Q[z+1]
proof
let z be Nat such that Q[z];
per cases;
suppose
A33: z+1 < n;
thus IC Comput(P,s1,4*(z+1)) = 5 by A1,A6,A10,A11,A33,Th29
.= IC Comput(Q,s2,4*(z+1)) by A1,A7,A13,A14,A33,Th29;
end;
suppose
A34: z+1 >= n;
A35: 4*(z+1) = 4*(z+1)+0;
thus IC Comput(P,s1,4*(z+1)) = IC Comput(P,s1,4*(z+1)+0)
.= 1 by A1,A6,A10,A11,A34,A29,Th29
.= IC Comput(Q,s2,4*(z+1)) by A1,A7,A13,A14,A34,A35,A29,Th29;
end;
end;
thus for z being Nat holds Q[z] from NAT_1:sch 2(A31,A32);
end;
per cases;
suppose
A36: i = 0;
A37: now
let j such that
A38: j = 2;
thus IC Comput(P,s1,4*i+j) = 3 by A1,A6,A10,A11,A38,A29,A36,Th29
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A38,A29,A36,Th29;
thus Comput(P,s1,4*i+j).a = Comput(Q,s2,4*i+j).a by A23;
thus Comput(P,s1,4*i+j).b = n-i by A1,A6,A10,A11,A38,A29,A36,Th29
.= Comput(Q,s2,4*i+j).b by A1,A7,A13,A14,A38,A29,A36,Th29;
thus Comput(P,s1,4*i+j).c = Comput(Q,s2,4*i+j).c
by A3,A4,A6,A7,A8,A9;
end;
A39: now
let j such that
A40: j = 3;
thus IC Comput(P,s1,4*i+j) = 4 by A1,A6,A10,A11,A40,A29,A36,Th29
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A40,A29,A36,Th29;
thus Comput(P,s1,4*i+j).a = Comput(Q,s2,4*i+j).a by A23;
thus Comput(P,s1,4*i+j).b = n-i-1 by A1,A6,A10,A11,A40,A29,A36,Th29
.= Comput(Q,s2,4*i+j).b by A1,A7,A13,A14,A40,A29,A36,Th29;
thus Comput(P,s1,4*i+j).c = Comput(Q,s2,4*i+j).c
by A3,A4,A6,A7,A8,A9;
end;
per cases by A20,A22;
suppose
A41: j = 1;
thus IC Comput(P,s1,4*i+j) = 2 by A1,A6,A10,A11,A41,A29,A36,Th29
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A41,A29,A36,Th29;
thus Comput(P,s1,4*i+j).a = Comput(Q,s2,4*i+j).a by A23;
thus Comput(P,s1,4*i+j).b = Comput(P,s1,4*i).b by A6,A10,A36,A41,Th16
.= Comput(Q,s2,4*i+j).b by A7,A10,A17,A18,A36,A41,Th16;
thus Comput(P,s1,4*i+j).c = Comput(P,s1,4*i).c by A6,A10,A36,A41,Th16
.= Comput(Q,s2,4*i+j).c by A7,A10,A17,A19,A36,A41,Th16;
end;
suppose j = 2;
hence thesis by A37;
end;
suppose j = 3;
hence thesis by A39;
end;
suppose
A42: j = 4;
4*i+j = 4*(i+1) by A42;
hence IC Comput(P,s1,4*i+j) = IC Comput(Q,s2,4*i+j) by A30;
thus Comput(P,s1,4*i+j).a = Comput(Q,s2,4*i+j).a by A23;
thus Comput(P,s1,4*i+j).b = n-i-1 by A1,A6,A10,A11,A42,A29,A36,Th29
.= Comput(Q,s2,4*i+j).b by A1,A7,A13,A14,A42,A29,A36,Th29;
thus Comput(P,s1,4*i+j).c = Comput(Q,s2,4*i+j).c by A3,A4,A6,A7,A8,A9;
end;
end;
suppose
A43: 0 < i < n;
now
per cases by A20,A22;
suppose
A44: j = 1;
hence IC Comput(P,s1,4*i+j) = 2 by A1,A6,A10,A11,A43,Th29
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A43,A44,Th29;
end;
suppose
A45: j = 2;
hence IC Comput(P,s1,4*i+j) = 3 by A1,A6,A10,A11,A43,Th29
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A43,A45,Th29;
end;
suppose
A46: j = 3;
hence IC Comput(P,s1,4*i+j) = 4 by A1,A6,A10,A11,A43,Th29
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A43,A46,Th29;
end;
suppose
A47: j = 4;
4*i+4 = 4*(i+1);
hence IC Comput(P,s1,4*i+j) = IC Comput(Q,s2,4*i+j) by A47,A30;
end;
end;
hence IC Comput(P,s1,4*i+j) = IC Comput(Q,s2,4*i+j);
thus Comput(P,s1,4*i+j).a = Comput(Q,s2,4*i+j).a by A23;
A48: now
thus Comput(P,s1,4*i+1).b = n-i by A1,A6,A10,A11,A43,Th29
.= Comput(Q,s2,4*i+1).b by A1,A7,A13,A14,A43,Th29;
end;
A49: now
thus Comput(P,s1,4*i+2).b = n-i by A1,A6,A10,A11,A43,Th29
.= Comput(Q,s2,4*i+2).b by A1,A7,A13,A14,A43,Th29;
end;
now
per cases by A20,A22;
suppose j = 1;
hence Comput(P,s1,4*i+j).b = Comput(Q,s2,4*i+j).b by A48;
end;
suppose j = 2;
hence Comput(P,s1,4*i+j).b = Comput(Q,s2,4*i+j).b by A49;
end;
suppose
A50: j = 3;
hence Comput(P,s1,4*i+j).b = n-i-1 by A1,A6,A10,A11,A43,Th29
.= Comput(Q,s2,4*i+j).b by A1,A7,A13,A14,A43,A50,Th29;
end;
suppose
A51: j = 4;
hence Comput(P,s1,4*i+j).b = n-i-1 by A1,A6,A10,A11,A43,Th29
.= Comput(Q,s2,4*i+j).b by A1,A7,A13,A14,A43,A51,Th29;
end;
end;
hence Comput(P,s1,4*i+j).b = Comput(Q,s2,4*i+j).b;
thus Comput(P,s1,4*i+j).c = Comput(Q,s2,4*i+j).c by A3,A4,A6,A7,A8,A9;
end;
suppose
A52: n <= i;
hence IC Comput(P,s1,4*i+j) = 1 by A1,A6,A10,A11,A29,Th29
.= IC Comput(Q,s2,4*i+j) by A1,A7,A13,A14,A52,A29,Th29;
thus Comput(P,s1,4*i+j).a = 1 by A1,A6,A10,A11,Th26
.= Comput(Q,s2,4*i+j).a by A1,A7,A13,A14,Th26;
consider z being Nat such that
A53: j = z+1 by A20,NAT_1:6;
thus Comput(P,s1,4*i+j).b = Comput(P,s1,4*i+1+z).b by A53
.= 0 by A1,A6,A10,A11,A52,A29,Th29
.= Comput(Q,s2,4*i+1+z).b by A1,A7,A13,A14,A52,A29,Th29
.= Comput(Q,s2,4*i+j).b by A53;
thus Comput(P,s1,4*i+j).c = Comput(Q,s2,4*i+j).c by A3,A4,A6,A7,A8,A9;
end;
end;
end;
A54: 4 > 0;
A55: dom x = {a,b,c} by A5,FUNCT_4:128;
A56: dom (Initialize x) = dom SA \/ dom x by FUNCT_4:def 1
.= { IC SCM, a,b,c } by A55,ENUMSET1:4;
reconsider k as Element of NAT by ORDINAL1:def 12;
P[k] from NAT_D:sch 2(A15,A54,A16);
hence thesis by A12,A56,Th3;
end;
scheme HaltedSch
{ f() -> PartFunc of FinPartSt SCM, FinPartSt SCM,
I() -> Instruction of SCM,
F(object) -> Nat }:
for x being FinPartState of SCM st x in dom f() holds
Initialize x is IterativeAlgorithm(I())-halted
provided
A1: I() = AddTo(dl.2,dl.1) or I() = SubFrom(dl.2,dl.1) or
I() = MultBy(dl.2,dl.1) and
A2: for x being object st x in dom f()
ex n being Nat st x = (dl.0,dl.1,dl.2) --> (1,n,F(n))
proof
let x be FinPartState of SCM;
assume x in dom f();
then consider n being Nat such that
A3: x = (a,b,c) --> (1,n,F(n)) by A2;
let s be State of SCM such that
A4: Initialize x c= s;
set q = IterativeAlgorithm(I());
let P be Instruction-Sequence of SCM such that
A5: q c= P;
A6: s is 0-started by A4,MEMSTR_0:17;
s is State-consisting of <%1,n,F(n)%> by A3,A4,Th15;
hence P halts_on s by A1,A5,A6,Th29;
end;
scheme AutonomySch
{ f() -> PartFunc of FinPartSt SCM, FinPartSt SCM,
I() -> Instruction of SCM,
F(object) -> Nat }:
for x being FinPartState of SCM st x in dom f() holds
Initialize x is Autonomy of IterativeAlgorithm(I())
provided
A1: I() = AddTo(dl.2,dl.1) or I() = SubFrom(dl.2,dl.1) or
I() = MultBy(dl.2,dl.1) and
A2: for x being object st x in dom f()
ex n being Nat st x = (dl.0,dl.1,dl.2) --> (1,n,F(n)) and
A3: for P,Q being Instruction-Sequence of SCM st
IterativeAlgorithm(I()) c= P & IterativeAlgorithm(I()) c= Q
for x being FinPartState of SCM st x in dom f()
for s1,s2 being State of SCM st Initialize x c= s1 & Initialize x c= s2
for k being Nat holds Comput(P,s1,k).dl.2 = Comput(Q,s2,k).dl.2
proof
let x be FinPartState of SCM such that
A4: x in dom f();
for x being FinPartState of SCM st x in dom f() holds
Initialize x is IterativeAlgorithm(I())-autonomic
from AutonomicSch(A1,A2,A3);
hence Initialize x is IterativeAlgorithm(I())-autonomic by A4;
for x being FinPartState of SCM st x in dom f() holds
Initialize x is IterativeAlgorithm(I())-halted from HaltedSch(A1,A2);
hence thesis by A4;
end;
theorem Th35:
for x being FinPartState of SCM st x in dom powerSCMFunction holds
Initialize x is Autonomy of IterativeAlgorithm(MultBy(dl.2,dl.1))
proof
let x be FinPartState of SCM such that
A1: x in dom pf;
set I = MultBy(c,b);
A2: I = AddTo(c,b) or I = SubFrom(c,b) or I = MultBy(c,b);
deffunc F(Nat) = 1;
A3: for x being object st x in dom pf
ex n being Nat st x = (a,b,c) --> (1,n,F(n)) by Th33;
A4: for P,Q being Instruction-Sequence of SCM st
IterativeAlgorithm(I) c= P & IterativeAlgorithm(I) c= Q
for x being FinPartState of SCM st x in dom pf
for s1,s2 being State of SCM st Initialize x c= s1 & Initialize x c= s2
for k being Nat holds Comput(P,s1,k).c = Comput(Q,s2,k).c
proof
let P,Q be Instruction-Sequence of SCM such that
A5: IterativeAlgorithm(I) c= P and
A6: IterativeAlgorithm(I) c= Q;
let x be FinPartState of SCM such that
A7: x in dom pf;
let s1,s2 be State of SCM such that
A8: Initialize x c= s1 and
A9: Initialize x c= s2;
consider n being Nat such that
A10: x = (a,b,c) --> (1,n,F(n)) by A7,Th33;
let k be Nat;
reconsider P as IterativeAlgorithm(I)-extending
Instruction-Sequence of SCM by A5,PROOFS_1:def 12;
reconsider Q as IterativeAlgorithm(I)-extending
Instruction-Sequence of SCM by A6,PROOFS_1:def 12;
reconsider s1 as 0-started State-consisting of <%1,n,F(n)%>
by A10,A8,Th15,MEMSTR_0:17;
reconsider s2 as 0-started State-consisting of <%1,n,F(n)%>
by A10,A9,Th15,MEMSTR_0:17;
defpred P[Nat] means Comput(P,s1,$1).c = Comput(Q,s2,$1).c;
Comput(P,s1,0).c = F(n) by Th14
.= Comput(Q,s2,0).c by Th14;
then
A11: P[0];
A12: 4 > 0;
A13: for i,j being Nat st P[4*i] & j <> 0 & j <= 4 holds P[4*i+j]
proof
let i,j be Nat such that P[4*i] and
A14: j <> 0 and
A15: j <= 4;
reconsider j1 = j-1 as Nat by A14;
per cases;
suppose
A16: i >= n;
Comput(P,s1,4*i+j).c = Comput(P,s1,4*i+1+j1).c
.= n! by A16,Th32
.= Comput(Q,s2,4*i+1+j1).c by A16,Th32
.= Comput(Q,s2,4*i+j).c;
hence thesis;
end;
suppose
A17: i < n;
Comput(P,s1,4*i+2).b = n-i by A5,A17,Th29
.= Comput(Q,s2,4*i+2).b by A6,A17,Th29;
then
A18: Comput(Q,s2,4*i+2).c = n!/((Comput(P,s1,4*i+2).b-'1)!) by A17,Th32
.= Comput(P,s1,4*i+2).c by A17,Th32;
A19: Comput(Q,s2,4*i+3).c = Comput(Q,s2,4*i+2).c by A17,Th32
.= Comput(P,s1,4*i+3).c by A17,A18,Th32;
j = 0 or ... or j = 4 by A15;
then per cases by A14;
suppose
A20: j = 1;
Comput(P,s1,4*i+1).b = n-i by A5,A17,Th29
.= Comput(Q,s2,4*i+1).b by A6,A17,Th29;
then Comput(Q,s2,4*i+1).c = n!/((Comput(P,s1,4*i+1).b)!) by A17,Th32
.= Comput(P,s1,4*i+1).c by A17,Th32;
hence thesis by A20;
end;
suppose j = 2;
hence thesis by A18;
end;
suppose j = 3;
hence thesis by A19;
end;
suppose
A21: j = 4;
Comput(Q,s2,4*i+4).c = Comput(Q,s2,4*i+3).c by A17,Th32
.= Comput(P,s1,4*i+4).c by A17,A19,Th32;
hence thesis by A21;
end;
end;
end;
reconsider k as Element of NAT by ORDINAL1:def 12;
P[k] from NAT_D:sch 2(A11,A12,A13);
hence thesis;
end;
for x being FinPartState of SCM st x in dom pf holds
Initialize x is Autonomy of IterativeAlgorithm(I)
from AutonomySch(A2,A3,A4);
hence thesis by A1;
end;
theorem
IterativeAlgorithm(MultBy(dl.2,dl.1)), Start-At(0,SCM) computes
powerSCMFunction
proof
let x be set;
assume
A1: x in dom pf;
then consider n being Nat such that
A2: x = (a,b,c) --> (1,n,1) by Th33;
reconsider d = x as FinPartState of SCM by A2;
consider s being State of SCM such that
A3: Initialize d c= s by PBOOLE:141;
consider P being Instruction-Sequence of SCM such that
A4: q c= P by PBOOLE:145;
A5: P is IterativeAlgorithm(MultBy(c,b))-extending Instruction-Sequence of SCM
by A4,PROOFS_1:def 12;
take d;
thus x = d;
A6: Initialize d = SA+*d by A2,MEMSTR_0:82;
hence SA+*d is Autonomy of q by A1,Th35;
then
A7: Result(q,SA+*d) = Result(P,s)|dom(SA+*d) by A3,A4,A6,EXTPRO_1:def 13;
A8: pf.d = c .--> F(n) by A2,Th34;
A9: s is 0-started State-consisting of <%1,n,1%> by A2,A3,Th15,MEMSTR_0:17;
set f = Result(P,s)|dom(SA+*d);
A10: dom d c= dom(SA+*d) by FUNCT_4:10;
c in the carrier of SCM;
then
A11: c in dom Result(P,s) by PARTFUN1:def 2;
c in {a,b,c} by ENUMSET1:def 1;
then c in dom d by A2,FUNCT_4:128;
then
A12: c in dom f by A10,A11,RELAT_1:57;
then f.c = (Result(P,s)).c by FUNCT_1:47
.= F(n) by A5,A9,Th32;
hence thesis by A7,A8,A12,FUNCT_4:85;
end;
definition
func sumSCMFunction -> PartFunc of FinPartSt SCM, FinPartSt SCM means :Def6:
for p,q being FinPartState of SCM holds [p,q] in it iff
ex n being Nat st p = (dl.0,dl.1,dl.2) --> (1,n,0) &
q = dl.2 .--> Triangle n;
existence from PartFuncFinPartStEx;
uniqueness from PartFuncFinPartStUn;
end;
set pf = sumSCMFunction;
theorem Th37:
for p being object holds p in dom sumSCMFunction iff
ex n being Nat st p = (dl.0,dl.1,dl.2) --> (1,n,0)
proof
let p be object;
A1: p in dom pf iff [p,pf.p] in pf by FUNCT_1:1;
hereby
assume
A2: p in dom pf;
then pf.p in FinPartSt SCM by PARTFUN1:4;
then
A3: pf.p is FinPartState of SCM by MEMSTR_0:76;
p is FinPartState of SCM by A2,MEMSTR_0:76;
then ex n being Nat st p = (a,b,c) --> (1,n,0) & pf.p = c .--> T(n)
by A1,A2,A3,Def6;
hence ex n being Nat st p = (a,b,c) --> (1,n,0);
end;
given n being Nat such that
A4: p = (a,b,c) --> (1,n,0);
[p,c.-->T(n)] in pf by A4,Def6;
hence thesis by FUNCT_1:1;
end;
set q = IterativeAlgorithm(AddTo(c,b));
theorem Th38:
sumSCMFunction.((dl.0,dl.1,dl.2) --> (1,n,0)) = dl.2 .--> Triangle n
proof
[ (a,b,c) --> (1,n,0), c.-->T(n) ] in pf by Def6;
hence thesis by FUNCT_1:1;
end;
theorem Th39:
for x being FinPartState of SCM st x in dom sumSCMFunction holds
Initialize x is Autonomy of IterativeAlgorithm(AddTo(dl.2,dl.1))
proof
let x be FinPartState of SCM such that
A1: x in dom pf;
set I = AddTo(c,b);
A2: I = AddTo(c,b) or I = SubFrom(c,b) or I = MultBy(c,b);
deffunc F(Nat) = 0;
A3: for x being object st x in dom pf
ex n being Nat st x = (a,b,c) --> (1,n,F(n)) by Th37;
A4: for P,Q being Instruction-Sequence of SCM st
IterativeAlgorithm(I) c= P & IterativeAlgorithm(I) c= Q
for x being FinPartState of SCM st x in dom pf
for s1,s2 being State of SCM st Initialize x c= s1 & Initialize x c= s2
for k being Nat holds Comput(P,s1,k).c = Comput(Q,s2,k).c
proof
let P,Q be Instruction-Sequence of SCM such that
A5: IterativeAlgorithm(I) c= P and
A6: IterativeAlgorithm(I) c= Q;
let x be FinPartState of SCM such that
A7: x in dom pf;
let s1,s2 be State of SCM such that
A8: Initialize x c= s1 and
A9: Initialize x c= s2;
consider n being Nat such that
A10: x = (a,b,c) --> (1,n,F(n)) by A7,Th37;
let k be Nat;
reconsider P as IterativeAlgorithm(I)-extending
Instruction-Sequence of SCM by A5,PROOFS_1:def 12;
reconsider Q as IterativeAlgorithm(I)-extending
Instruction-Sequence of SCM by A6,PROOFS_1:def 12;
reconsider s1 as 0-started State-consisting of <%1,n,F(n)%>
by A10,A8,Th15,MEMSTR_0:17;
reconsider s2 as 0-started State-consisting of <%1,n,F(n)%>
by A10,A9,Th15,MEMSTR_0:17;
defpred P[Nat] means Comput(P,s1,$1).c = Comput(Q,s2,$1).c;
Comput(P,s1,0).c = F(n) by Th14
.= Comput(Q,s2,0).c by Th14;
then
A11: P[0];
A12: 4 > 0;
A13: for i,j being Nat st P[4*i] & j <> 0 & j <= 4 holds P[4*i+j]
proof
let i,j be Nat such that P[4*i] and
A14: j <> 0 and
A15: j <= 4;
reconsider j1 = j-1 as Nat by A14;
per cases;
suppose
A16: i >= n;
Comput(P,s1,4*i+j).c = Comput(P,s1,4*i+1+j1).c
.= T(n) by A16,Th31
.= Comput(Q,s2,4*i+1+j1).c by A16,Th31
.= Comput(Q,s2,4*i+j).c;
hence thesis;
end;
suppose
A17: i < n;
Comput(P,s1,4*i+2).b = n-i by A5,A17,Th29
.= Comput(Q,s2,4*i+2).b by A6,A17,Th29;
then
A18: Comput(Q,s2,4*i+2).c
= T(n) - T(Comput(P,s1,4*i+2).b-'1) by A17,Th31
.= Comput(P,s1,4*i+2).c by A17,Th31;
A19: Comput(Q,s2,4*i+3).c = Comput(Q,s2,4*i+2).c by A17,Th31
.= Comput(P,s1,4*i+3).c by A17,A18,Th31;
j = 0 or ... or j = 4 by A15;
then per cases by A14;
suppose
A20: j = 1;
Comput(P,s1,4*i+1).b = n-i by A5,A17,Th29
.= Comput(Q,s2,4*i+1).b by A6,A17,Th29;
then Comput(Q,s2,4*i+1).c
= T(n) - T(Comput(P,s1,4*i+1).b) by A17,Th31
.= Comput(P,s1,4*i+1).c by A17,Th31;
hence thesis by A20;
end;
suppose j = 2;
hence thesis by A18;
end;
suppose j = 3;
hence thesis by A19;
end;
suppose
A21: j = 4;
Comput(Q,s2,4*i+4).c = Comput(Q,s2,4*i+3).c by A17,Th31
.= Comput(P,s1,4*i+4).c by A17,A19,Th31;
hence thesis by A21;
end;
end;
end;
reconsider k as Element of NAT by ORDINAL1:def 12;
P[k] from NAT_D:sch 2(A11,A12,A13);
hence thesis;
end;
for x being FinPartState of SCM st x in dom pf holds
Initialize x is Autonomy of IterativeAlgorithm(I)
from AutonomySch(A2,A3,A4);
hence thesis by A1;
end;
theorem
IterativeAlgorithm(AddTo(dl.2,dl.1)), Start-At(0,SCM) computes sumSCMFunction
proof
let x be set;
assume
A1: x in dom pf;
then consider n being Nat such that
A2: x = (a,b,c) --> (1,n,0) by Th37;
reconsider d = x as FinPartState of SCM by A2;
consider s being State of SCM such that
A3: Initialize d c= s by PBOOLE:141;
consider P being Instruction-Sequence of SCM such that
A4: q c= P by PBOOLE:145;
A5: P is IterativeAlgorithm(AddTo(c,b))-extending Instruction-Sequence of SCM
by A4,PROOFS_1:def 12;
take d;
thus x = d;
A6: Initialize d = SA+*d by A2,MEMSTR_0:82;
hence SA+*d is Autonomy of q by A1,Th39;
then
A7: Result(q,SA+*d) = Result(P,s)|dom(SA+*d) by A3,A4,A6,EXTPRO_1:def 13;
A8: pf.d = c .--> T(n) by A2,Th38;
A9: s is 0-started State-consisting of <%1,n,0%> by A2,A3,Th15,MEMSTR_0:17;
set f = Result(P,s)|dom(SA+*d);
A10: dom d c= dom(SA+*d) by FUNCT_4:10;
c in the carrier of SCM;
then
A11: c in dom Result(P,s) by PARTFUN1:def 2;
c in {a,b,c} by ENUMSET1:def 1;
then c in dom d by A2,FUNCT_4:128;
then
A12: c in dom f by A10,A11,RELAT_1:57;
then f.c = (Result(P,s)).c by FUNCT_1:47
.= T(n) by A5,A9,Th31;
hence thesis by A7,A8,A12,FUNCT_4:85;
end;