:: Partial Correctness of a Factorial Algorithm
:: by Adrian Jaszczak and Artur Korni{\l}owicz
::
:: Received May 27, 2019
:: Copyright (c) 2019-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 3.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/3.0/.
environ
vocabularies NOMIN_1, NUMBERS, ZFMISC_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1,
FINSEQ_1, NAT_1, ARYTM_3, PARTFUN1, XBOOLEAN, TARSKI, NOMIN_3, NOMIN_4,
XCMPLX_0, NOMIN_2, PARTPR_1, PARTPR_2, NOMIN_5, REALSET1, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS,
MARGREL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FUNCOP_1, BINOP_1, XXREAL_0, XCMPLX_0, FUNCT_3, NEWTON, NOMIN_1,
PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_3, NOMIN_4;
constructors RELSET_1, INT_2, BINOP_1, FUNCOP_1, FUNCT_3, NEWTON, ENUMSET1,
NOMIN_2, NOMIN_3, NOMIN_4;
registrations ORDINAL1, RELSET_1, NOMIN_1, XCMPLX_0, NOMIN_2, NAT_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, NOMIN_3;
equalities NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_4, XBOOLEAN, BINOP_1;
expansions TARSKI, PARTFUN1, NOMIN_4, ZFMISC_1;
theorems XBOOLE_0, NOMIN_1, PARTPR_1, NOMIN_2, NOMIN_3, NOMIN_4, FUNCT_1,
FUNCT_3, PARTFUN1, TARSKI, NEWTON, XCMPLX_0, PARTPR_2, ENUMSET1;
schemes BINOP_1, NOMIN_4, PARTPR_2;
begin
definition
let D be set;
let f1,f2,f3 be BinominativeFunction of D;
func PP_composition(f1,f2,f3) -> BinominativeFunction of D equals
PP_composition(PP_composition(f1,f2),f3);
coherence;
end;
definition
let D be set;
let f1,f2,f3,f4 be BinominativeFunction of D;
func PP_composition(f1,f2,f3,f4) -> BinominativeFunction of D equals
PP_composition(PP_composition(f1,f2,f3),f4);
coherence;
end;
reserve D for non empty set;
reserve f1,f2,f3,f4 for BinominativeFunction of D;
reserve p,q,r,t,w for PartialPredicate of D;
::$N unconditional composition rule for 3 programs
theorem
<*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D &
<*PP_inversion(q),f2,r*> is SFHT of D &
<*PP_inversion(r),f3,w*> is SFHT of D
implies <*p,PP_composition(f1,f2,f3),w*> is SFHT of D
proof
assume that
A1: <*p,f1,q*> is SFHT of D and
A2: <*q,f2,r*> is SFHT of D and
A3: <*r,f3,w*> is SFHT of D and
A4: <*PP_inversion(q),f2,r*> is SFHT of D and
A5: <*PP_inversion(r),f3,w*> is SFHT of D;
<*p,PP_composition(f1,f2),r*> is SFHT of D by A1,A2,A4,NOMIN_3:25;
hence thesis by A3,A5,NOMIN_3:25;
end;
::$N unconditional composition rule for 4 programs
theorem Th2:
<*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D &
<*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D &
<*PP_inversion(q),f2,r*> is SFHT of D &
<*PP_inversion(r),f3,w*> is SFHT of D &
<*PP_inversion(w),f4,t*> is SFHT of D
implies <*p,PP_composition(f1,f2,f3,f4),t*> is SFHT of D
proof
assume that
A1: <*p,f1,q*> is SFHT of D and
A2: <*q,f2,r*> is SFHT of D and
A3: <*r,f3,w*> is SFHT of D and
A4: <*w,f4,t*> is SFHT of D and
A5: <*PP_inversion(q),f2,r*> is SFHT of D and
A6: <*PP_inversion(r),f3,w*> is SFHT of D and
A7: <*PP_inversion(w),f4,t*> is SFHT of D;
<*p,PP_composition(f1,f2),r*> is SFHT of D by A1,A2,A5,NOMIN_3:25;
then <*p,PP_composition(PP_composition(f1,f2),f3),w*> is SFHT of D
by A3,A6,NOMIN_3:25;
hence thesis by A4,A7,NOMIN_3:25;
end;
reserve d,v,v1 for object;
reserve V,A for set;
reserve z for Element of V;
reserve d1 for NonatomicND of V,A;
reserve f for SCBinominativeFunction of V,A;
reserve T for TypeSCNominativeData of V,A;
theorem Th3:
A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1
implies local_overlapping(V,A,d1,T,v).v1 = d1.v1
proof
assume that
A1: A is_without_nonatomicND_wrt V and
A2: v in V & v <> v1;
not d1 in A & not naming(V,A,v,T) in A by A1,NOMIN_4:3;
hence thesis by A2,NOMIN_2:12;
end;
definition
let x,y be object;
assume
A1: x is Complex & y is Complex;
func addition(x,y) -> Complex means :Def3:
ex x1,y1 being Complex st x1 = x & y1 = y & it = x1 + y1;
existence
proof
reconsider x1 = x, y1 = y as Complex by A1;
take x1+y1;
thus thesis;
end;
uniqueness;
func multiplication(x,y) -> Complex means :Def4:
ex x1,y1 being Complex st x1 = x & y1 = y & it = x1 * y1;
existence
proof
reconsider x1 = x, y1 = y as Complex by A1;
take x1*y1;
thus thesis;
end;
uniqueness;
end;
definition
let A;
assume
A1: A is complex-containing;
deffunc F(object,object) = addition($1,$2);
func addition(A) -> Function of [:A,A:],A means :Def5:
for x,y being object st x in A & y in A holds it.(x,y) = addition(x,y);
existence
proof
A2: for x,y being object st x in A & y in A holds F(x,y) in A
proof
let x,y be object such that x in A & y in A;
F(x,y) in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
consider f being Function of [:A,A:],A such that
A3: for x,y being object st x in A & y in A holds f.(x,y) = F(x,y)
from BINOP_1:sch 2(A2);
take f;
thus thesis by A3;
end;
uniqueness
proof
for f,g being Function of [:A,A:],A st
(for x,y being object st x in A & y in A holds f.(x,y) = F(x,y)) &
(for x,y being object st x in A & y in A holds g.(x,y) = F(x,y))
holds f = g from NOMIN_4:sch 3;
hence thesis;
end;
deffunc G(object,object) = multiplication($1,$2);
func multiplication(A) -> Function of [:A,A:],A means :Def6:
for x,y being object st x in A & y in A holds it.(x,y) = multiplication(x,y);
existence
proof
A4: for x,y being object st x in A & y in A holds G(x,y) in A
proof
let x,y be object such that x in A & y in A;
G(x,y) in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
consider f being Function of [:A,A:],A such that
A5: for x,y being object st x in A & y in A holds f.(x,y) = G(x,y)
from BINOP_1:sch 2(A4);
take f;
thus thesis by A5;
end;
uniqueness
proof
for f,g being Function of [:A,A:],A st
(for x,y being object st x in A & y in A holds f.(x,y) = G(x,y)) &
(for x,y being object st x in A & y in A holds g.(x,y) = G(x,y))
holds f = g from NOMIN_4:sch 3;
hence thesis;
end;
end;
definition
let V,A;
let x,y be Element of V;
func addition(A,x,y) -> SCBinominativeFunction of V,A equals
lift_binary_op(addition(A),x,y);
coherence;
func multiplication(A,x,y) -> SCBinominativeFunction of V,A equals
lift_binary_op(multiplication(A),x,y);
coherence;
end;
theorem Th4:
for i,j being Element of V holds
A is complex-containing & i in dom d1 & j in dom d1 &
d1 in dom addition(A,i,j) implies
for x,y being Complex st x = d1.i & y = d1.j holds
addition(A,i,j).d1 = x + y
proof
let i,j be Element of V;
assume that
A1: A is complex-containing and
A2: i in dom d1 and
A3: j in dom d1 and
A4: d1 in dom addition(A,i,j);
let x,y be Complex such that
A5: x = d1.i & y = d1.j;
set Di = denaming(V,A,i);
set Dj = denaming(V,A,j);
A6: d1 in dom <:Di,Dj:> by A4,FUNCT_1:11;
then
A7: <:Di,Dj:>.d1 = [Di.d1,Dj.d1] by FUNCT_3:def 7;
A8: dom <:Di,Dj:> = dom Di /\ dom Dj by FUNCT_3:def 7;
then d1 in dom Di by A6,XBOOLE_0:def 4;
then
A9: Di.d1 = denaming(i,d1) by NOMIN_1:def 18
.= d1.i by A2,NOMIN_1:def 12;
d1 in dom Dj by A6,A8,XBOOLE_0:def 4;
then
A10: Dj.d1 = denaming(j,d1) by NOMIN_1:def 18
.= d1.j by A3,NOMIN_1:def 12;
A11: x in COMPLEX & y in COMPLEX by XCMPLX_0:def 2;
thus addition(A,i,j).d1 = (addition(A)).(Di.d1,Dj.d1) by A4,A7,FUNCT_1:12
.= addition(Di.d1,Dj.d1) by A1,A5,A9,A10,A11,Def5
.= x + y by A5,A9,A10,Def3;
end;
theorem Th5:
for i,j being Element of V holds
A is complex-containing & i in dom d1 & j in dom d1 &
d1 in dom multiplication(A,i,j) implies
for x,y being Complex st x = d1.i & y = d1.j holds
multiplication(A,i,j).d1 = x * y
proof
let i,j be Element of V;
assume that
A1: A is complex-containing and
A2: i in dom d1 and
A3: j in dom d1 and
A4: d1 in dom multiplication(A,i,j);
let x,y be Complex such that
A5: x = d1.i & y = d1.j;
set Di = denaming(V,A,i);
set Dj = denaming(V,A,j);
A6: d1 in dom <:Di,Dj:> by A4,FUNCT_1:11;
then
A7: <:Di,Dj:>.d1 = [Di.d1,Dj.d1] by FUNCT_3:def 7;
A8: dom <:Di,Dj:> = dom Di /\ dom Dj by FUNCT_3:def 7;
then d1 in dom Di by A6,XBOOLE_0:def 4;
then
A9: Di.d1 = denaming(i,d1) by NOMIN_1:def 18
.= d1.i by A2,NOMIN_1:def 12;
d1 in dom Dj by A6,A8,XBOOLE_0:def 4;
then
A10: Dj.d1 = denaming(j,d1) by NOMIN_1:def 18
.= d1.j by A3,NOMIN_1:def 12;
A11: x in COMPLEX & y in COMPLEX by XCMPLX_0:def 2;
thus multiplication(A,i,j).d1
= (multiplication(A)).(Di.d1,Dj.d1) by A4,A7,FUNCT_1:12
.= multiplication(Di.d1,Dj.d1) by A1,A5,A9,A10,A11,Def6
.= x * y by A5,A9,A10,Def4;
end;
:: Pseudocode of n!
::
:: i := val.1
:: j := val.2
:: n := val.3
:: s := val.4
:: { s == i! }
:: while ( i <> n )
:: i := i + j
:: s := s * i
:: return s
:: { n == i && s == i! }
::
:: where
:: val.1 = 0,
:: val.2 = 1,
:: val.3 - the number n the factorial of which we compute,
:: val.4 = 1
:: are input data from the environment,
:: and loc/.1 = i, loc/.2 = j, loc/.3 = n, loc/.4 = s.
reserve loc for V-valued Function;
reserve val for Function;
definition
let V,A,loc;
func factorial_loop_body(A,loc) -> SCBinominativeFunction of V,A equals
PP_composition(
SC_assignment(addition(A,loc/.1,loc/.2),loc/.1),
SC_assignment(multiplication(A,loc/.4,loc/.1),loc/.4)
);
coherence;
end;
definition
let V,A,loc;
func factorial_main_loop(A,loc) -> SCBinominativeFunction of V,A equals
PP_while(PP_not(Equality(A,loc/.1,loc/.3)),factorial_loop_body(A,loc));
coherence;
end;
definition
let V,A,loc,val;
func factorial_var_init(A,loc,val)
-> SCBinominativeFunction of V,A equals
PP_composition(
SC_assignment(denaming(V,A,val.1), loc/.1),
SC_assignment(denaming(V,A,val.2), loc/.2),
SC_assignment(denaming(V,A,val.3), loc/.3),
SC_assignment(denaming(V,A,val.4), loc/.4)
);
coherence;
end;
definition
let V,A,loc,val;
func factorial_main_part(A,loc,val)
-> SCBinominativeFunction of V,A equals
PP_composition(
factorial_var_init(A,loc,val),
factorial_main_loop(A,loc)
);
coherence;
end;
definition
let V,A,loc,val,z;
func factorial_program(A,loc,val,z)
-> SCBinominativeFunction of V,A equals
PP_composition(
factorial_main_part(A,loc,val),
SC_assignment(denaming(V,A,loc/.4),z)
);
coherence;
end;
reserve n0 for Nat;
definition
let V,A,val,n0,d;
pred valid_factorial_input_pred V,A,val,n0,d means
ex d1 being NonatomicND of V,A st d = d1 &
{ val.1, val.2, val.3, val.4 } c= dom d1 &
d1.(val.1) = 0 & d1.(val.2) = 1 & d1.(val.3) = n0 & d1.(val.4) = 1;
end;
definition
let V,A,val,n0;
defpred P[object] means valid_factorial_input_pred V,A,val,n0,$1;
func valid_factorial_input(V,A,val,n0)
-> SCPartialNominativePredicate of V,A
means :Def15:
dom it = ND(V,A) &
for d being object st d in dom it holds
(valid_factorial_input_pred V,A,val,n0,d implies it.d = TRUE) &
(not valid_factorial_input_pred V,A,val,n0,d
implies it.d = FALSE);
existence
proof
A1: ND(V,A) c= ND(V,A);
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))
from PARTPR_2:sch 1(A1);
take p;
thus thesis by A2;
end;
uniqueness
proof
for p,q being SCPartialNominativePredicate of V,A st
(dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))) &
(dom q = ND(V,A) & (for d being object st d in dom q holds
(P[d] implies q.d = TRUE) & (not P[d] implies q.d = FALSE)))
holds p = q from PARTPR_2:sch 2;
hence thesis;
end;
end;
registration
let V,A,val,n0;
cluster valid_factorial_input(V,A,val,n0) -> total;
coherence by Def15;
end;
definition
let V,A,z,n0,d;
pred valid_factorial_output_pred A,z,n0,d means
ex d1 being NonatomicND of V,A st d = d1 & z in dom d1 & d1.z = n0!;
end;
definition
let V,A,z,n0;
set D = {d where d is TypeSCNominativeData of V,A: d in dom denaming(V,A,z)};
defpred P[object] means valid_factorial_output_pred A,z,n0,$1;
func valid_factorial_output(A,z,n0) -> SCPartialNominativePredicate of V,A
means :Def17:
dom it = {d where d is TypeSCNominativeData of V,A:
d in dom denaming(V,A,z)} &
for d being object st d in dom it holds
(valid_factorial_output_pred A,z,n0,d implies it.d = TRUE) &
(not valid_factorial_output_pred A,z,n0,d implies it.d = FALSE);
existence
proof
A1: D c= ND(V,A)
proof
let v;
assume v in D;
then ex d being TypeSCNominativeData of V,A st v = d &
d in dom denaming(V,A,z);
hence thesis;
end;
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = D & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))
from PARTPR_2:sch 1(A1);
take p;
thus thesis by A2;
end;
uniqueness
proof
for p,q being SCPartialNominativePredicate of V,A st
(dom p = D & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))) &
(dom q = D & (for d being object st d in dom q holds
(P[d] implies q.d = TRUE) & (not P[d] implies q.d = FALSE)))
holds p = q from PARTPR_2:sch 2;
hence thesis;
end;
end;
definition
let V,A,loc,n0,d;
pred factorial_inv_pred A,loc,n0,d means
ex d1 being NonatomicND of V,A st
d = d1 & { loc/.1, loc/.2, loc/.3, loc/.4 } c= dom d1 &
d1.(loc/.2) = 1 & d1.(loc/.3) = n0 &
ex I,S being Nat st I = d1.(loc/.1) & S = d1.(loc/.4) & S = I!;
end;
definition
let V,A,loc,n0;
defpred P[object] means factorial_inv_pred A,loc,n0,$1;
func factorial_inv(A,loc,n0) -> SCPartialNominativePredicate of V,A means
:Def19:
dom it = ND(V,A) &
for d being object st d in dom it holds
(factorial_inv_pred A,loc,n0,d implies it.d = TRUE) &
(not factorial_inv_pred A,loc,n0,d implies it.d = FALSE);
existence
proof
A1: ND(V,A) c= ND(V,A);
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))
from PARTPR_2:sch 1(A1);
take p;
thus thesis by A2;
end;
uniqueness
proof
for p,q being SCPartialNominativePredicate of V,A st
(dom p = ND(V,A) & (for d being object st d in dom p holds
(P[d] implies p.d = TRUE) & (not P[d] implies p.d = FALSE))) &
(dom q = ND(V,A) & (for d being object st d in dom q holds
(P[d] implies q.d = TRUE) & (not P[d] implies q.d = FALSE)))
holds p = q from PARTPR_2:sch 2;
hence thesis;
end;
end;
registration
let V,A,loc,n0;
cluster factorial_inv(A,loc,n0) -> total;
coherence by Def19;
end;
definition
let V,loc,val;
pred loc,val are_compatible_wrt_4_locs means
val.4 <> loc/.3 & val.4 <> loc/.2 & val.4 <> loc/.1 &
val.3 <> loc/.2 & val.3 <> loc/.1 & val.2 <> loc/.1;
end;
theorem Th6:
V is non empty & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct &
loc,val are_compatible_wrt_4_locs
implies
<* valid_factorial_input(V,A,val,n0),
factorial_var_init(A,loc,val),
factorial_inv(A,loc,n0) *> is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4;
set i1 = val.1, j1 = val.2, n1 = val.3, s1 = val.4;
set D = ND(V,A);
set I = valid_factorial_input(V,A,val,n0);
set F = factorial_var_init(A,loc,val);
set inv = factorial_inv(A,loc,n0);
set Di = denaming(V,A,i1);
set Dj = denaming(V,A,j1);
set Dn = denaming(V,A,n1);
set Ds = denaming(V,A,s1);
set asi = SC_assignment(Di,i);
set asj = SC_assignment(Dj,j);
set asn = SC_assignment(Dn,n);
set ass = SC_assignment(Ds,s);
set S1 = SC_Psuperpos(inv,Ds,s);
set R1 = SC_Psuperpos(S1,Dn,n);
set Q1 = SC_Psuperpos(R1,Dj,j);
set P1 = SC_Psuperpos(Q1,Di,i);
assume that
A1: V is non empty and
A2: A is_without_nonatomicND_wrt V and
A3: i,j,n,s are_mutually_distinct and
A4: loc,val are_compatible_wrt_4_locs;
A5: <*Q1,asj,R1*> is SFHT of D by NOMIN_3:29;
A6: <*R1,asn,S1*> is SFHT of D by NOMIN_3:29;
A7: <*S1,ass,inv*> is SFHT of D by NOMIN_3:29;
A8: <*P1,asi,Q1*> is SFHT of D by NOMIN_3:29;
I ||= P1
proof
let d be Element of D;
assume d in dom I & I.d = TRUE;
then valid_factorial_input_pred V,A,val,n0,d by Def15;
then consider d1 being NonatomicND of V,A such that
A9: d = d1 and
A10: {i1,j1,n1,s1} c= dom d1 and
A11: d1.i1 = 0 and
A12: d1.j1 = 1 and
A13: d1.n1 = n0 and
A14: d1.s1 = 1;
A15: i1 in {i1,j1,n1,s1} by ENUMSET1:def 2;
A16: j1 in {i1,j1,n1,s1} by ENUMSET1:def 2;
A17: n1 in {i1,j1,n1,s1} by ENUMSET1:def 2;
A18: s1 in {i1,j1,n1,s1} by ENUMSET1:def 2;
A20: dom Di = {d where d is NonatomicND of V,A: i1 in dom d}
by NOMIN_1:def 18;
A21: dom Dj = {d where d is NonatomicND of V,A: j1 in dom d}
by NOMIN_1:def 18;
A22: dom Dn = {d where d is NonatomicND of V,A: n1 in dom d}
by NOMIN_1:def 18;
A23: dom Ds = {d where d is NonatomicND of V,A: s1 in dom d}
by NOMIN_1:def 18;
A24: dom P1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Di.d,i) in dom Q1 & d in dom Di}
by NOMIN_2:def 11;
A25: dom Q1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Dj.d,j) in dom R1 & d in dom Dj}
by NOMIN_2:def 11;
A26: dom R1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Dn.d,n) in dom S1 & d in dom Dn}
by NOMIN_2:def 11;
A27: dom S1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Ds.d,s) in dom inv & d in dom Ds}
by NOMIN_2:def 11;
reconsider Li = local_overlapping(V,A,d1,Di.d1,i) as NonatomicND of V,A
by NOMIN_2:9;
reconsider Lj = local_overlapping(V,A,Li,Dj.Li,j) as NonatomicND of V,A
by NOMIN_2:9;
reconsider Ln = local_overlapping(V,A,Lj,Dn.Lj,n) as NonatomicND of V,A
by NOMIN_2:9;
reconsider Ls = local_overlapping(V,A,Ln,Ds.Ln,s) as NonatomicND of V,A
by NOMIN_2:9;
A28: d1 in dom Di by A10,A15,A20;
then
A29: Di.d1 is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A30: dom Li = {i} \/ dom d1 by A1,A2,NOMIN_4:4;
dom inv = D by Def19;
then
A31: Ls in dom inv;
A32: j1 in dom Li by A10,A16,A30,XBOOLE_0:def 3;
then
A33: Li in dom Dj by A21;
then
A34: Dj.Li is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A35: dom Lj = {j} \/ dom Li by A1,A2,NOMIN_4:4;
A36: n1 in dom Li by A10,A17,A30,XBOOLE_0:def 3;
then
A37: n1 in dom Lj by A35,XBOOLE_0:def 3;
then
A38: Lj in dom Dn by A22;
then
A39: Dn.Lj is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A40: dom Ln = {n} \/ dom Lj by A1,A2,NOMIN_4:4;
A41: s1 in dom Li by A10,A18,A30,XBOOLE_0:def 3;
then
A42: s1 in dom Lj by A35,XBOOLE_0:def 3;
then
A43: s1 in dom Ln by A40,XBOOLE_0:def 3;
then
A44: Ln in dom Ds by A23;
then
A45: Ln in dom S1 by A27,A31;
A46: Lj in dom R1 by A26,A45,A38;
then
A47: Li in dom Q1 by A25,A33;
hence
A48: d in dom P1 by A9,A24,A28;
A49: factorial_inv_pred A,loc,n0,Ls
proof
take Ls;
thus Ls = Ls;
A50: Ds.Ln is TypeSCNominativeData of V,A by A44,PARTFUN1:4,NOMIN_1:39;
then
A51: dom Ls = {s} \/ dom Ln by A1,A2,NOMIN_4:4;
i in {i} by TARSKI:def 1;
then
A52: i in dom Li by A30,XBOOLE_0:def 3;
then
A53: i in dom Lj by A35,XBOOLE_0:def 3;
then
A54: i in dom Ln by A40,XBOOLE_0:def 3;
then
A55: i in dom Ls by A51,XBOOLE_0:def 3;
j in {j} by TARSKI:def 1;
then
A56: j in dom Lj by A35,XBOOLE_0:def 3;
then
A57: j in dom Ln by A40,XBOOLE_0:def 3;
then
A58: j in dom Ls by A51,XBOOLE_0:def 3;
n in {n} by TARSKI:def 1;
then
A59: n in dom Ln by A40,XBOOLE_0:def 3;
then
A60: n in dom Ls by A51,XBOOLE_0:def 3;
s in {s} by TARSKI:def 1;
then s in dom Ls by A51,XBOOLE_0:def 3;
hence {i,j,n,s} c= dom Ls by A55,A58,A60,ENUMSET1:def 2;
thus Ls.j = Ln.j by A1,A2,A3,A50,A57,Th3
.= Lj.j by A1,A2,A3,A39,A56,Th3
.= Dj.Li by A1,A34,NOMIN_2:10
.= denaming(j1,Li) by A33,NOMIN_1:def 18
.= Li.j1 by A32,NOMIN_1:def 12
.= 1 by A1,A2,A4,A10,A16,A12,A29,Th3;
thus Ls.n = Ln.n by A1,A2,A3,A50,A59,Th3
.= Dn.Lj by A1,A39,NOMIN_2:10
.= denaming(n1,Lj) by A38,NOMIN_1:def 18
.= Lj.n1 by A37,NOMIN_1:def 12
.= Li.n1 by A1,A2,A4,A34,A36,Th3
.= n0 by A1,A2,A4,A10,A17,A13,A29,Th3;
A61: Ln.s1 = Lj.s1 by A1,A2,A4,A42,A39,Th3
.= Li.s1 by A1,A2,A4,A34,A41,Th3
.= 1 by A1,A2,A4,A10,A18,A14,A29,Th3;
take 0,1;
thus Ls.i = Ln.i by A1,A2,A3,A50,A54,Th3
.= Lj.i by A1,A2,A3,A53,A39,Th3
.= Li.i by A1,A2,A3,A34,A52,Th3
.= Di.d1 by A1,A29,NOMIN_2:10
.= denaming(i1,d1) by A28,NOMIN_1:def 18
.= 0 by A10,A11,A15,NOMIN_1:def 12;
thus Ls.s = Ds.Ln by A1,A50,NOMIN_2:10
.= denaming(s1,Ln) by A44,NOMIN_1:def 18
.= 1 by A61,A43,NOMIN_1:def 12;
thus 1 = 0! by NEWTON:12;
end;
thus P1.d = Q1.Li by A9,A48,NOMIN_2:35
.= R1.Lj by A47,NOMIN_2:35
.= S1.Ln by A46,NOMIN_2:35
.= inv.Ls by A45,NOMIN_2:35
.= TRUE by A31,A49,Def19;
end;
then
A62: <*I,asi,Q1*> is SFHT of D by A8,NOMIN_3:15;
A63: <*PP_inversion(Q1),asj,R1*> is SFHT of D by NOMIN_4:16;
A64: <*PP_inversion(R1),asn,S1*> is SFHT of D by NOMIN_4:16;
<*PP_inversion(S1),ass,inv*> is SFHT of D by NOMIN_4:16;
hence thesis by A62,A5,A6,A7,A63,A64,Th2;
end;
theorem Th7:
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct
implies
<* factorial_inv(A,loc,n0),
factorial_loop_body(A,loc),
factorial_inv(A,loc,n0) *> is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4;
assume that
A1: V is non empty and
A2: A is complex-containing and
A3: A is_without_nonatomicND_wrt V and
A4: i,j,n,s are_mutually_distinct;
set D = ND(V,A);
set inv = factorial_inv(A,loc,n0);
set B = factorial_loop_body(A,loc);
set add = addition(A,i,j);
set mlt = multiplication(A,s,i);
set f = SC_assignment(add,i);
set g = SC_assignment(mlt,s);
set Di = denaming(V,A,i);
set Dj = denaming(V,A,j);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
now
let d be TypeSCNominativeData of V,A such that
A5: d in dom inv and
A6: inv.d = TRUE and
A7: d in dom B and
A8: B.d in dom inv;
factorial_inv_pred A,loc,n0,d by A5,A6,Def19;
then consider d1 being NonatomicND of V,A such that
A9: d = d1 and
A10: {i,j,n,s} c= dom d1 and
A11: d1.j = 1 and
A12: d1.n = n0 and
A13: ex I,S being Nat st I = d1.i & S = d1.s & S = I!;
A14: i in {i,j,n,s} by ENUMSET1:def 2;
A15: j in {i,j,n,s} by ENUMSET1:def 2;
A16: n in {i,j,n,s} by ENUMSET1:def 2;
A17: s in {i,j,n,s} by ENUMSET1:def 2;
consider I,S being Nat such that
A18: I = d1.i and
A19: S = d1.s and
A20: S = I! by A13;
A21: dom f = dom add by NOMIN_2:def 7;
A22: dom g = dom mlt by NOMIN_2:def 7;
A23: PP_composition(f,g) = g*f by PARTPR_2:def 1;
then
A24: d in dom f by A7,FUNCT_1:11;
then reconsider Ad = add.d1 as TypeSCNominativeData of V,A
by A21,A9,PARTFUN1:4,NOMIN_1:39;
reconsider La = local_overlapping(V,A,d1,Ad,i)
as NonatomicND of V,A by NOMIN_2:9;
reconsider Lm = local_overlapping(V,A,La,mlt.La,s)
as NonatomicND of V,A by NOMIN_2:9;
B = g*f by PARTPR_2:def 1;
then
A25: B.d = g.(f.d) by A7,FUNCT_1:12;
A26: f.d = La by A9,A24,NOMIN_2:def 7;
then
A27: La in dom g by A7,A23,FUNCT_1:11;
A28: g.La = Lm by A27,NOMIN_2:def 7;
factorial_inv_pred A,loc,n0,Lm
proof
take Lm;
thus Lm = Lm;
A29: mlt.La is TypeSCNominativeData of V,A by A22,A27,PARTFUN1:4,NOMIN_1:39;
A30: dom Lm = dom La \/ {s} by A3,A1,A22,A27,A28,NOMIN_4:5;
A31: dom La = {i} \/ dom d1 by A3,A1,NOMIN_4:4;
i in {i} by TARSKI:def 1;
then
A32: i in dom La by A31,XBOOLE_0:def 3;
then
A33: i in dom Lm by A30,XBOOLE_0:def 3;
A34: j in dom La by A10,A15,A31,XBOOLE_0:def 3;
then
A35: j in dom Lm by A30,XBOOLE_0:def 3;
A36: n in dom La by A10,A16,A31,XBOOLE_0:def 3;
then
A37: n in dom Lm by A30,XBOOLE_0:def 3;
s in {s} by TARSKI:def 1;
then s in dom Lm by A30,XBOOLE_0:def 3;
hence {i,j,n,s} c= dom Lm by A33,A35,A37,ENUMSET1:def 2;
thus Lm.j = La.j by A1,A3,A4,A29,A34,Th3
.= 1 by A3,A1,A10,A15,A11,A4,Th3;
thus Lm.n = La.n by A4,A1,A29,A36,A3,Th3
.= n0 by A3,A1,A4,A10,A16,A12,Th3;
take I1 = I+1, S1 = S*(I+1);
A38: La.i = Ad by A1,NOMIN_2:10
.= I1 by A14,A2,A18,A10,A11,A15,A9,A24,A21,Th4;
hence Lm.i = I1 by A1,A29,A3,A4,A32,Th3;
A39: s in dom La by A10,A17,A31,XBOOLE_0:def 3;
A40: La.s = d1.s by A3,A1,A10,A4,A17,Th3;
thus Lm.s = mlt.La by A1,A29,NOMIN_2:10
.= S1 by A32,A2,A19,A39,A22,A27,A38,A40,Th5;
thus S1 = I1! by A20,NEWTON:15;
end;
hence inv.(B.d) = TRUE by A8,A25,A26,A28,Def19;
end;
hence thesis by NOMIN_3:28;
end;
::$CT
theorem Th9:
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct
implies
<* factorial_inv(A,loc,n0),
factorial_main_loop(A,loc),
PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0)) *>
is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4;
set D = ND(V,A);
set inv = factorial_inv(A,loc,n0);
set B = factorial_loop_body(A,loc);
set E = Equality(A,i,n);
set N = PP_inversion(inv);
assume V is non empty & A is complex-containing &
A is_without_nonatomicND_wrt V & i,j,n,s are_mutually_distinct;
then
A1: <*inv,B,inv*> is SFHT of D by Th7;
PP_and(PP_not(E),inv) ||= inv by NOMIN_3:3;
then
A2: <*PP_and(PP_not(E),inv),B,inv*> is SFHT of D by A1,NOMIN_3:15;
A3: <*N,B,inv*> is SFHT of D by NOMIN_3:19;
PP_and(PP_not(E),N) ||= N by NOMIN_3:3;
then <*PP_and(PP_not(E),N),B,inv*> is SFHT of D by A3,NOMIN_3:15;
hence thesis by A2,NOMIN_3:26;
end;
theorem Th10:
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct &
loc,val are_compatible_wrt_4_locs
implies
<* valid_factorial_input(V,A,val,n0),
factorial_main_part(A,loc,val),
PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0)) *>
is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4;
set i1 = val.1, j1 = val.2, n1 = val.3, s1 = val.4;
set D = ND(V,A);
set p = valid_factorial_input(V,A,val,n0);
set f = factorial_var_init(A,loc,val);
set g = factorial_main_loop(A,loc);
set q = factorial_inv(A,loc,n0);
set r = PP_and(Equality(A,i,n),factorial_inv(A,loc,n0));
assume
A1: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
i,j,n,s are_mutually_distinct & loc,val are_compatible_wrt_4_locs;
then
A2: <*p,f,q*> is SFHT of D by Th6;
A3: <*q,g,r*> is SFHT of D by A1,Th9;
<*PP_inversion(q),g,r*> is SFHT of D by NOMIN_3:19;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th11:
V is non empty & A is_without_nonatomicND_wrt V &
(for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
implies
PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0))
||=
SC_Psuperpos(valid_factorial_output(A,z,n0),denaming(V,A,loc/.4),z)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4;
set D = ND(V,A);
set inv = factorial_inv(A,loc,n0);
set Di = denaming(V,A,i);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set Dz = denaming(V,A,z);
set ass = SC_assignment(Ds,z);
set out = valid_factorial_output(A,z,n0);
set p = SC_Psuperpos(out,Ds,z);
set E = Equality(A,i,n);
assume that
A1: V is non empty & A is_without_nonatomicND_wrt V and
A2: for T holds i is_a_value_on T & n is_a_value_on T;
let d be Element of D such that
A3: d in dom PP_and(E,inv) and
A4: (PP_and(E,inv)).d = TRUE;
A5: dom p = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Ds.d,z) in dom out & d in dom Ds}
by NOMIN_2:def 11;
A6: dom out = {d where d is TypeSCNominativeData of V,A: d in dom Dz}
by Def17;
A7: dom Ds = {d where d is NonatomicND of V,A: s in dom d} by NOMIN_1:def 18;
A8: dom Dz = {d where d is NonatomicND of V,A: z in dom d} by NOMIN_1:def 18;
A9: d in dom E by A3,A4,PARTPR_1:23;
A10: d in dom inv by A3,A4,PARTPR_1:23;
A11: dom E = dom Di /\ dom Dn by A2,NOMIN_4:11;
then
A12: d in dom Di by A9,XBOOLE_0:def 4;
inv.d = TRUE by A3,A4,PARTPR_1:23;
then factorial_inv_pred A,loc,n0,d by A10,Def19;
then consider d1 being NonatomicND of V,A such that
A13: d = d1 and
A14: {i,j,n,s} c= dom d1 and
d1.j = 1 and
A15: d1.n = n0 and
A16: ex I,S being Nat st I = d1.i & S = d1.s & S = I!;
A17: i in {i,j,n,s} by ENUMSET1:def 2;
A18: n in {i,j,n,s} by ENUMSET1:def 2;
A19: s in {i,j,n,s} by ENUMSET1:def 2;
reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;
set L = local_overlapping(V,A,dd,Ds.dd,z);
A20: dd in dom Ds by A7,A13,A14,A19;
then Ds.d1 in D by A13,PARTFUN1:4;
then
A21: ex d2 being TypeSCNominativeData of V,A st Ds.d1 = d2;
then
A22: L in dom Dz by A1,A13,NOMIN_4:6;
then
A23: L in dom out by A6;
hence
A24: d in dom p by A5,A20;
valid_factorial_output_pred A,z,n0,L
proof
consider I,S being Nat such that
A25: I = d1.i and
A26: S = d1.s and
A27: S = I! by A16;
A28: ex d being NonatomicND of V,A st L = d & z in dom d by A8,A22;
then reconsider dlo = L as NonatomicND of V,A;
take dlo;
thus L = dlo;
thus z in dom dlo by A28;
A29: i is_a_value_on dd by A2;
A30: n is_a_value_on dd by A2;
A31: dom <:Di,Dn:> = dom Di /\ dom Dn by FUNCT_3:def 7;
d in dom <:Di,Dn:> by A9,A11,FUNCT_3:def 7;
then
A32: E.d = (Equality(A)).(<:Di,Dn:>.d) by FUNCT_1:13;
A33: d in dom Dn by A9,A11,XBOOLE_0:def 4;
A34: <:Di,Dn:>.d = [Di.d,Dn.d] by A9,A11,A31,FUNCT_3:def 7;
A35: Di.d = denaming(i,d1) by A13,A12,NOMIN_1:def 18
.= d1.i by A14,A17,NOMIN_1:def 12;
A36: Dn.d = denaming(n,d1) by A13,A33,NOMIN_1:def 18
.= d1.n by A14,A18,NOMIN_1:def 12;
A37: Ds.d = denaming(s,d1) by A20,A13,NOMIN_1:def 18
.= d1.s by A14,A19,NOMIN_1:def 12;
(Equality(A)).(Di.d,Dn.d) <> FALSE by A3,A4,A32,A34,PARTPR_1:23;
then Di.d = Dn.d by A29,A30,NOMIN_4:def 9;
hence dlo.z = n0! by A1,A13,A15,A21,A25,A26,A27,A35,A36,A37,NOMIN_2:10;
end;
hence TRUE = out.L by A23,Def17
.= p.d by A24,NOMIN_2:35;
end;
theorem Th12:
V is non empty & A is_without_nonatomicND_wrt V &
(for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
implies
<* PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0)),
SC_assignment(denaming(V,A,loc/.4),z),
valid_factorial_output(A,z,n0) *> is SFHT of ND(V,A)
proof
set s = loc/.4;
<*SC_Psuperpos(valid_factorial_output(A,z,n0),denaming(V,A,s),z),
SC_assignment(denaming(V,A,s),z),
valid_factorial_output(A,z,n0)*> is SFHT of ND(V,A) by NOMIN_3:29;
hence thesis by Th11,NOMIN_3:15;
end;
theorem Th13:
(for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
implies
<* PP_inversion(PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0))),
SC_assignment(denaming(V,A,loc/.4),z),
valid_factorial_output(A,z,n0) *> is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4;
set D = ND(V,A);
set inv = factorial_inv(A,loc,n0);
set O = valid_factorial_output(A,z,n0);
set Di = denaming(V,A,i);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set g = SC_assignment(Ds,z);
set E = Equality(A,i,n);
set q = PP_and(E,inv);
set N = PP_inversion(q);
assume
A1: for T holds i is_a_value_on T & n is_a_value_on T;
now
let d be TypeSCNominativeData of V,A such that
A2: d in dom N and
N.d = TRUE and
d in dom g and
g.d in dom O;
A3: dom q = {d where d is Element of D:
d in dom E & E.d = FALSE or d in dom inv & inv.d = FALSE
or d in dom E & E.d = TRUE & d in dom inv & inv.d = TRUE} by PARTPR_1:16;
A4: dom Di = {d where d is NonatomicND of V,A: i in dom d} by NOMIN_1:def 18;
A5: dom Dn = {d where d is NonatomicND of V,A: n in dom d} by NOMIN_1:def 18;
A6: dom E = dom Di /\ dom Dn by A1,NOMIN_4:11;
A7: not d in dom q by A2,PARTPR_2:9;
dom E c= dom q by PARTPR_2:3;
then not d in dom E by A2,PARTPR_2:9;
then
A8: not d in dom Di or not d in dom Dn by A6,XBOOLE_0:def 4;
dom inv = D by Def19;
then
A9: d in dom inv;
then inv.d <> FALSE by A3,A7;
then factorial_inv_pred A,loc,n0,d by A9,Def19;
then consider d1 being NonatomicND of V,A such that
A10: d = d1 and
A11: {i,j,n,s} c= dom d1 and
d1.(loc/.2) = 1 & d1.(loc/.3) = n0 &
ex I,S being Nat st I = d1.(loc/.1) & S = d1.(loc/.4) & S = I!;
i in {i,j,n,s} & n in {i,j,n,s} by ENUMSET1:def 2;
hence O.(g.d) = TRUE by A4,A5,A8,A10,A11;
end;
hence thesis by NOMIN_3:28;
end;
::$N Partial correctness of a FACTORIAL algorithm
theorem
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct &
loc,val are_compatible_wrt_4_locs &
(for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
implies
<* valid_factorial_input(V,A,val,n0),
factorial_program(A,loc,val,z),
valid_factorial_output(A,z,n0) *>
is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, n = loc/.3, s = loc/.4;
set i1 = val.1, j1 = val.2, n1 = val.3, s1 = val.4;
set D = ND(V,A);
set p = valid_factorial_input(V,A,val,n0);
set f = factorial_main_part(A,loc,val);
set g = SC_assignment(denaming(V,A,s),z);
set q = valid_factorial_output(A,z,n0);
set inv = factorial_inv(A,loc,n0);
set E = Equality(A,i,n);
assume that
A1: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V
and
A2: i,j,n,s are_mutually_distinct and
A3: loc,val are_compatible_wrt_4_locs and
A4: for T holds i is_a_value_on T & n is_a_value_on T;
A5: <*p,f,PP_and(E,inv)*> is SFHT of D by A1,A3,A2,Th10;
A6: <*PP_and(E,inv),g,q*> is SFHT of D by A1,A4,Th12;
<*PP_inversion(PP_and(E,inv)),g,q*> is SFHT of D by A4,Th13;
hence thesis by A5,A6,NOMIN_3:25;
end;