:: Partial Correctness of a Factorial Algorithm
:: by Adrian Jaszczak and Artur Korni{\l}owicz
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


definition
let D be set ;
let f1, f2, f3 be BinominativeFunction of D;
func PP_composition (f1,f2,f3) -> BinominativeFunction of D equals :: NOMIN_5:def 1
PP_composition ((PP_composition (f1,f2)),f3);
coherence
PP_composition ((PP_composition (f1,f2)),f3) is BinominativeFunction of D
;
end;

:: deftheorem defines PP_composition NOMIN_5:def 1 :
for D being set
for f1, f2, f3 being BinominativeFunction of D holds PP_composition (f1,f2,f3) = PP_composition ((PP_composition (f1,f2)),f3);

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 :: NOMIN_5:def 2
PP_composition ((PP_composition (f1,f2,f3)),f4);
coherence
PP_composition ((PP_composition (f1,f2,f3)),f4) is BinominativeFunction of D
;
end;

:: deftheorem defines PP_composition NOMIN_5:def 2 :
for D being set
for f1, f2, f3, f4 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4) = PP_composition ((PP_composition (f1,f2,f3)),f4);

:: WP: unconditional composition rule for 3 programs
theorem :: NOMIN_5:1
for D being non empty set
for f1, f2, f3 being BinominativeFunction of D
for p, q, r, w being PartialPredicate of D st <*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 holds
<*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D
proof end;

:: WP: unconditional composition rule for 4 programs
theorem Th2: :: NOMIN_5:2
for D being non empty set
for f1, f2, f3, f4 being BinominativeFunction of D
for p, q, r, t, w being PartialPredicate of D st <*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 holds
<*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D
proof end;

theorem Th3: :: NOMIN_5:3
for v, v1 being object
for V, A being set
for d1 being NonatomicND of V,A
for T being TypeSCNominativeData of V,A st A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 holds
(local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1
proof end;

definition
let x, y be object ;
assume A1: ( x is Complex & y is Complex ) ;
func addition (x,y) -> Complex means :Def3: :: NOMIN_5:def 3
ex x1, y1 being Complex st
( x1 = x & y1 = y & it = x1 + y1 );
existence
ex b1, x1, y1 being Complex st
( x1 = x & y1 = y & b1 = x1 + y1 )
proof end;
uniqueness
for b1, b2 being Complex st ex x1, y1 being Complex st
( x1 = x & y1 = y & b1 = x1 + y1 ) & ex x1, y1 being Complex st
( x1 = x & y1 = y & b2 = x1 + y1 ) holds
b1 = b2
;
func multiplication (x,y) -> Complex means :Def4: :: NOMIN_5:def 4
ex x1, y1 being Complex st
( x1 = x & y1 = y & it = x1 * y1 );
existence
ex b1, x1, y1 being Complex st
( x1 = x & y1 = y & b1 = x1 * y1 )
proof end;
uniqueness
for b1, b2 being Complex st ex x1, y1 being Complex st
( x1 = x & y1 = y & b1 = x1 * y1 ) & ex x1, y1 being Complex st
( x1 = x & y1 = y & b2 = x1 * y1 ) holds
b1 = b2
;
end;

:: deftheorem Def3 defines addition NOMIN_5:def 3 :
for x, y being object st x is Complex & y is Complex holds
for b3 being Complex holds
( b3 = addition (x,y) iff ex x1, y1 being Complex st
( x1 = x & y1 = y & b3 = x1 + y1 ) );

:: deftheorem Def4 defines multiplication NOMIN_5:def 4 :
for x, y being object st x is Complex & y is Complex holds
for b3 being Complex holds
( b3 = multiplication (x,y) iff ex x1, y1 being Complex st
( x1 = x & y1 = y & b3 = x1 * y1 ) );

definition
let A be set ;
assume A1: A is complex-containing ;
deffunc H1( object , object ) -> Complex = addition ($1,$2);
func addition A -> Function of [:A,A:],A means :Def5: :: NOMIN_5:def 5
for x, y being object st x in A & y in A holds
it . (x,y) = addition (x,y);
existence
ex b1 being Function of [:A,A:],A st
for x, y being object st x in A & y in A holds
b1 . (x,y) = addition (x,y)
proof end;
uniqueness
for b1, b2 being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds
b1 . (x,y) = addition (x,y) ) & ( for x, y being object st x in A & y in A holds
b2 . (x,y) = addition (x,y) ) holds
b1 = b2
proof end;
deffunc H2( object , object ) -> Complex = multiplication ($1,$2);
func multiplication A -> Function of [:A,A:],A means :Def6: :: NOMIN_5:def 6
for x, y being object st x in A & y in A holds
it . (x,y) = multiplication (x,y);
existence
ex b1 being Function of [:A,A:],A st
for x, y being object st x in A & y in A holds
b1 . (x,y) = multiplication (x,y)
proof end;
uniqueness
for b1, b2 being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds
b1 . (x,y) = multiplication (x,y) ) & ( for x, y being object st x in A & y in A holds
b2 . (x,y) = multiplication (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines addition NOMIN_5:def 5 :
for A being set st A is complex-containing holds
for b2 being Function of [:A,A:],A holds
( b2 = addition A iff for x, y being object st x in A & y in A holds
b2 . (x,y) = addition (x,y) );

:: deftheorem Def6 defines multiplication NOMIN_5:def 6 :
for A being set st A is complex-containing holds
for b2 being Function of [:A,A:],A holds
( b2 = multiplication A iff for x, y being object st x in A & y in A holds
b2 . (x,y) = multiplication (x,y) );

definition
let V, A be set ;
let x, y be Element of V;
func addition (A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 7
lift_binary_op ((addition A),x,y);
coherence
lift_binary_op ((addition A),x,y) is SCBinominativeFunction of V,A
;
func multiplication (A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 8
lift_binary_op ((multiplication A),x,y);
coherence
lift_binary_op ((multiplication A),x,y) is SCBinominativeFunction of V,A
;
end;

:: deftheorem defines addition NOMIN_5:def 7 :
for V, A being set
for x, y being Element of V holds addition (A,x,y) = lift_binary_op ((addition A),x,y);

:: deftheorem defines multiplication NOMIN_5:def 8 :
for V, A being set
for x, y being Element of V holds multiplication (A,x,y) = lift_binary_op ((multiplication A),x,y);

theorem Th4: :: NOMIN_5:4
for V, A being set
for d1 being NonatomicND of V,A
for i, j being Element of V st A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (addition (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(addition (A,i,j)) . d1 = x + y
proof end;

theorem Th5: :: NOMIN_5:5
for V, A being set
for d1 being NonatomicND of V,A
for i, j being Element of V st A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (multiplication (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(multiplication (A,i,j)) . d1 = x * y
proof end;

definition
let V, A be set ;
let loc be V -valued Function;
func factorial_loop_body (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 9
PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))));
coherence
PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4)))) is SCBinominativeFunction of V,A
;
end;

:: deftheorem defines factorial_loop_body NOMIN_5:def 9 :
for V, A being set
for loc being b1 -valued Function holds factorial_loop_body (A,loc) = PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))));

definition
let V, A be set ;
let loc be V -valued Function;
func factorial_main_loop (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 10
PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_loop_body (A,loc)));
coherence
PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_loop_body (A,loc))) is SCBinominativeFunction of V,A
;
end;

:: deftheorem defines factorial_main_loop NOMIN_5:def 10 :
for V, A being set
for loc being b1 -valued Function holds factorial_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_loop_body (A,loc)));

definition
let V, A be set ;
let loc be V -valued Function;
let val be Function;
func factorial_var_init (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 11
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
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)))) is SCBinominativeFunction of V,A
;
end;

:: deftheorem defines factorial_var_init NOMIN_5:def 11 :
for V, A being set
for loc being b1 -valued Function
for val being Function holds factorial_var_init (A,loc,val) = 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))));

definition
let V, A be set ;
let loc be V -valued Function;
let val be Function;
func factorial_main_part (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 12
PP_composition ((factorial_var_init (A,loc,val)),(factorial_main_loop (A,loc)));
coherence
PP_composition ((factorial_var_init (A,loc,val)),(factorial_main_loop (A,loc))) is SCBinominativeFunction of V,A
;
end;

:: deftheorem defines factorial_main_part NOMIN_5:def 12 :
for V, A being set
for loc being b1 -valued Function
for val being Function holds factorial_main_part (A,loc,val) = PP_composition ((factorial_var_init (A,loc,val)),(factorial_main_loop (A,loc)));

definition
let V, A be set ;
let loc be V -valued Function;
let val be Function;
let z be Element of V;
func factorial_program (A,loc,val,z) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 13
PP_composition ((factorial_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));
coherence
PP_composition ((factorial_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z))) is SCBinominativeFunction of V,A
;
end;

:: deftheorem defines factorial_program NOMIN_5:def 13 :
for V, A being set
for loc being b1 -valued Function
for val being Function
for z being Element of V holds factorial_program (A,loc,val,z) = PP_composition ((factorial_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));

definition
let V, A be set ;
let val be Function;
let n0 be Nat;
let d be object ;
pred valid_factorial_input_pred V,A,val,n0,d means :: NOMIN_5:def 14
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;

:: deftheorem defines valid_factorial_input_pred NOMIN_5:def 14 :
for V, A being set
for val being Function
for n0 being Nat
for d being object holds
( valid_factorial_input_pred V,A,val,n0,d iff 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 ) );

definition
let V, A be set ;
let val be Function;
let n0 be Nat;
defpred S1[ 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: :: NOMIN_5:def 15
( 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
ex b1 being SCPartialNominativePredicate of V,A st
( dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( valid_factorial_input_pred V,A,val,n0,d implies b1 . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,n0,d implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( valid_factorial_input_pred V,A,val,n0,d implies b1 . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( valid_factorial_input_pred V,A,val,n0,d implies b2 . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines valid_factorial_input NOMIN_5:def 15 :
for V, A being set
for val being Function
for n0 being Nat
for b5 being SCPartialNominativePredicate of V,A holds
( b5 = valid_factorial_input (V,A,val,n0) iff ( dom b5 = ND (V,A) & ( for d being object st d in dom b5 holds
( ( valid_factorial_input_pred V,A,val,n0,d implies b5 . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,n0,d implies b5 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let val be Function;
let n0 be Nat;
cluster valid_factorial_input (V,A,val,n0) -> total ;
coherence
valid_factorial_input (V,A,val,n0) is total
by Def15;
end;

definition
let V, A be set ;
let z be Element of V;
let n0 be Nat;
let d be object ;
pred valid_factorial_output_pred A,z,n0,d means :: NOMIN_5:def 16
ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = n0 ! );
end;

:: deftheorem defines valid_factorial_output_pred NOMIN_5:def 16 :
for V, A being set
for z being Element of V
for n0 being Nat
for d being object holds
( valid_factorial_output_pred A,z,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = n0 ! ) );

definition
let V, A be set ;
let z be Element of V;
let n0 be Nat;
set D = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } ;
defpred S1[ object ] means valid_factorial_output_pred A,z,n0,$1;
func valid_factorial_output (A,z,n0) -> SCPartialNominativePredicate of V,A means :Def17: :: NOMIN_5:def 17
( 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
ex b1 being SCPartialNominativePredicate of V,A st
( dom b1 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b1 holds
( ( valid_factorial_output_pred A,z,n0,d implies b1 . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b1 holds
( ( valid_factorial_output_pred A,z,n0,d implies b1 . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b2 holds
( ( valid_factorial_output_pred A,z,n0,d implies b2 . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines valid_factorial_output NOMIN_5:def 17 :
for V, A being set
for z being Element of V
for n0 being Nat
for b5 being SCPartialNominativePredicate of V,A holds
( b5 = valid_factorial_output (A,z,n0) iff ( dom b5 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b5 holds
( ( valid_factorial_output_pred A,z,n0,d implies b5 . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b5 . d = FALSE ) ) ) ) );

definition
let V, A be set ;
let loc be V -valued Function;
let n0 be Nat;
let d be object ;
pred factorial_inv_pred A,loc,n0,d means :: NOMIN_5:def 18
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;

:: deftheorem defines factorial_inv_pred NOMIN_5:def 18 :
for V, A being set
for loc being b1 -valued Function
for n0 being Nat
for d being object holds
( factorial_inv_pred A,loc,n0,d iff 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 ! ) ) );

definition
let V, A be set ;
let loc be V -valued Function;
let n0 be Nat;
defpred S1[ object ] means factorial_inv_pred A,loc,n0,$1;
func factorial_inv (A,loc,n0) -> SCPartialNominativePredicate of V,A means :Def19: :: NOMIN_5:def 19
( 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
ex b1 being SCPartialNominativePredicate of V,A st
( dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( factorial_inv_pred A,loc,n0,d implies b1 . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( factorial_inv_pred A,loc,n0,d implies b1 . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( factorial_inv_pred A,loc,n0,d implies b2 . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines factorial_inv NOMIN_5:def 19 :
for V, A being set
for loc being b1 -valued Function
for n0 being Nat
for b5 being SCPartialNominativePredicate of V,A holds
( b5 = factorial_inv (A,loc,n0) iff ( dom b5 = ND (V,A) & ( for d being object st d in dom b5 holds
( ( factorial_inv_pred A,loc,n0,d implies b5 . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b5 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let loc be V -valued Function;
let n0 be Nat;
cluster factorial_inv (A,loc,n0) -> total ;
coherence
factorial_inv (A,loc,n0) is total
by Def19;
end;

definition
let V be set ;
let loc be V -valued Function;
let val be Function;
pred loc,val are_compatible_wrt_4_locs means :: NOMIN_5:def 20
( 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;

:: deftheorem defines are_compatible_wrt_4_locs NOMIN_5:def 20 :
for V being set
for loc being b1 -valued Function
for val being Function holds
( loc,val are_compatible_wrt_4_locs iff ( val . 4 <> loc /. 3 & val . 4 <> loc /. 2 & val . 4 <> loc /. 1 & val . 3 <> loc /. 2 & val . 3 <> loc /. 1 & val . 2 <> loc /. 1 ) );

theorem Th6: :: NOMIN_5:6
for V, A being set
for loc being b1 -valued Function
for val being Function
for n0 being Nat st not V is 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 holds
<*(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 end;

theorem Th7: :: NOMIN_5:7
for V, A being set
for loc being b1 -valued Function
for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct holds
<*(factorial_inv (A,loc,n0)),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
proof end;

theorem :: NOMIN_5:8
canceled;

::$CT
theorem Th9: :: NOMIN_5:9
for V, A being set
for loc being b1 -valued Function
for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct holds
<*(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 end;

theorem Th10: :: NOMIN_5:10
for V, A being set
for loc being b1 -valued Function
for val being Function
for n0 being Nat st not V is 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 holds
<*(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 end;

theorem Th11: :: NOMIN_5:11
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
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 end;

theorem Th12: :: NOMIN_5:12
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(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 end;

theorem Th13: :: NOMIN_5:13
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for n0 being Nat st ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(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 end;

:: WP: Partial correctness of a FACTORIAL algorithm
theorem :: NOMIN_5:14
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for val being Function
for n0 being Nat st not V is 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 being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(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 end;