:: Partial Correctness of a Power Algorithm
:: by Adrian Jaszczak
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


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

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

:: WP: unconditional composition rule for 5 programs
theorem Th1: :: NOMIN_6:1
for D being non empty set
for f1, f2, f3, f4, f5 being BinominativeFunction of D
for p, q, r, t, w, u 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 & <*t,f5,u*> 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 & <*(PP_inversion t),f5,u*> is SFHT of D holds
<*p,(PP_composition (f1,f2,f3,f4,f5)),u*> is SFHT of D
proof end;

theorem Th2: :: NOMIN_6:2
for V, A being set
for i, j, b, n, s being Element of V
for i1, j1, b1, n1, s1 being object
for d1, Li, Lj, Lb, Ln, Ls being NonatomicND of V,A
for Di, Dj, Db, Dn, Ds being SCBinominativeFunction of V,A st not V is empty & A is_without_nonatomicND_wrt V & Di = denaming (V,A,i1) & Dj = denaming (V,A,j1) & Db = denaming (V,A,b1) & Dn = denaming (V,A,n1) & Ds = denaming (V,A,s1) & Li = local_overlapping (V,A,d1,(Di . d1),i) & Lj = local_overlapping (V,A,Li,(Dj . Li),j) & Lb = local_overlapping (V,A,Lj,(Db . Lj),b) & Ln = local_overlapping (V,A,Lb,(Dn . Lb),n) & Ls = local_overlapping (V,A,Ln,(Ds . Ln),s) & j1 in dom d1 & b1 in dom d1 & n1 in dom d1 & s1 in dom d1 & d1 in dom Di & s <> n holds
Ls . n = Ln . n
proof end;

theorem Th3: :: NOMIN_6:3
for V, A being set
for i, j, b, n, s being Element of V
for i1, j1, b1, n1, s1 being object
for d1, Li, Lj, Lb, Ln, Ls being NonatomicND of V,A
for Di, Dj, Db, Dn, Ds being SCBinominativeFunction of V,A st not V is empty & A is_without_nonatomicND_wrt V & Di = denaming (V,A,i1) & Dj = denaming (V,A,j1) & Db = denaming (V,A,b1) & Dn = denaming (V,A,n1) & Ds = denaming (V,A,s1) & Li = local_overlapping (V,A,d1,(Di . d1),i) & Lj = local_overlapping (V,A,Li,(Dj . Li),j) & Lb = local_overlapping (V,A,Lj,(Db . Lj),b) & Ln = local_overlapping (V,A,Lb,(Dn . Lb),n) & Ls = local_overlapping (V,A,Ln,(Ds . Ln),s) & j1 in dom d1 & b1 in dom d1 & n1 in dom d1 & s1 in dom d1 & d1 in dom Di & s <> i holds
Ls . i = Ln . i
proof end;

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

:: deftheorem defines power_loop_body NOMIN_6:def 2 :
for V, A being set
for loc being b1 -valued Function holds power_loop_body (A,loc) = PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))));

definition
let V, A be set ;
let loc be V -valued Function;
func power_main_loop (A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_6:def 3
 PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_loop_body (A,loc)));
coherence
PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_loop_body (A,loc))) is SCBinominativeFunction of V,A ;
end;

:: deftheorem defines power_main_loop NOMIN_6:def 3 :
for V, A being set
for loc being b1 -valued Function holds power_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_loop_body (A,loc)));

definition
let V, A be set ;
let loc be V -valued Function;
let val be Function;
func power_var_init (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_6:def 4
 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))),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5))));
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))),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5)))) is SCBinominativeFunction of V,A ;
end;

:: deftheorem defines power_var_init NOMIN_6:def 4 :
for V, A being set
for loc being b1 -valued Function
for val being Function holds power_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))),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5))));

definition
let V, A be set ;
let loc be V -valued Function;
let val be Function;
func power_main_part (A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_6:def 5
 PP_composition ((power_var_init (A,loc,val)),(power_main_loop (A,loc)));
coherence
PP_composition ((power_var_init (A,loc,val)),(power_main_loop (A,loc))) is SCBinominativeFunction of V,A ;
end;

:: deftheorem defines power_main_part NOMIN_6:def 5 :
for V, A being set
for loc being b1 -valued Function
for val being Function holds power_main_part (A,loc,val) = PP_composition ((power_var_init (A,loc,val)),(power_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 power_program (A,loc,val,z) -> SCBinominativeFunction of V,A equals :: NOMIN_6:def 6
 PP_composition ((power_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 5))),z)));
coherence
PP_composition ((power_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 5))),z))) is SCBinominativeFunction of V,A ;
end;

:: deftheorem defines power_program NOMIN_6:def 6 :
for V, A being set
for loc being b1 -valued Function
for val being Function
for z being Element of V holds power_program (A,loc,val,z) = PP_composition ((power_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 5))),z)));

definition
let V, A be set ;
let val be Function;
let b0 be Complex;
let n0 be Nat;
let d be object ;
pred valid_power_input_pred V,A,val,b0,n0,d means :: NOMIN_6:def 7
 ex d1 being NonatomicND of V,A st
( d = d1 & {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)} c= dom d1 & d1 . (val . 1) = 0 & d1 . (val . 2) = 1 & d1 . (val . 3) = b0 & d1 . (val . 4) = n0 & d1 . (val . 5) = 1 );
end;

:: deftheorem defines valid_power_input_pred NOMIN_6:def 7 :
for V, A being set
for val being Function
for b0 being Complex
for n0 being Nat
for d being object holds
( valid_power_input_pred V,A,val,b0,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)} c= dom d1 & d1 . (val . 1) = 0 & d1 . (val . 2) = 1 & d1 . (val . 3) = b0 & d1 . (val . 4) = n0 & d1 . (val . 5) = 1 ) );

definition
let V, A be set ;
let val be Function;
let b0 be Complex;
let n0 be Nat;
defpred S1[ object ] means valid_power_input_pred V,A,val,b0,n0,$1;
func valid_power_input (V,A,val,b0,n0) -> SCPartialNominativePredicate of V,A means :Def8: :: NOMIN_6:def 8
( dom it = ND (V,A) & ( for d being object st d in dom it holds
( ( valid_power_input_pred V,A,val,b0,n0,d implies it . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,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_power_input_pred V,A,val,b0,n0,d implies b1 . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,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_power_input_pred V,A,val,b0,n0,d implies b1 . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( valid_power_input_pred V,A,val,b0,n0,d implies b2 . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines valid_power_input NOMIN_6:def 8 :
for V, A being set
for val being Function
for b0 being Complex
for n0 being Nat
for b6 being SCPartialNominativePredicate of V,A holds
( b6 = valid_power_input (V,A,val,b0,n0) iff ( dom b6 = ND (V,A) & ( for d being object st d in dom b6 holds
( ( valid_power_input_pred V,A,val,b0,n0,d implies b6 . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b6 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let val be Function;
let b0 be Complex;
let n0 be Nat;
cluster valid_power_input (V,A,val,b0,n0) -> total ;
coherence
valid_power_input (V,A,val,b0,n0) is total by Def8;
end;

definition
let V, A be set ;
let z be Element of V;
let b0 be Complex;
let n0 be Nat;
let d be object ;
pred valid_power_output_pred A,z,b0,n0,d means :: NOMIN_6:def 9
 ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = b0 |^ n0 );
end;

:: deftheorem defines valid_power_output_pred NOMIN_6:def 9 :
for V, A being set
for z being Element of V
for b0 being Complex
for n0 being Nat
for d being object holds
( valid_power_output_pred A,z,b0,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = b0 |^ n0 ) );

definition
let V, A be set ;
let z be Element of V;
let b0 be Complex;
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_power_output_pred A,z,b0,n0,$1;
func valid_power_output (A,z,b0,n0) -> SCPartialNominativePredicate of V,A means :Def10: :: NOMIN_6:def 10
( 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_power_output_pred A,z,b0,n0,d implies it . d = TRUE ) & ( not valid_power_output_pred A,z,b0,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_power_output_pred A,z,b0,n0,d implies b1 . d = TRUE ) & ( not valid_power_output_pred A,z,b0,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_power_output_pred A,z,b0,n0,d implies b1 . d = TRUE ) & ( not valid_power_output_pred A,z,b0,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_power_output_pred A,z,b0,n0,d implies b2 . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines valid_power_output NOMIN_6:def 10 :
for V, A being set
for z being Element of V
for b0 being Complex
for n0 being Nat
for b6 being SCPartialNominativePredicate of V,A holds
( b6 = valid_power_output (A,z,b0,n0) iff ( dom b6 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b6 holds
( ( valid_power_output_pred A,z,b0,n0,d implies b6 . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies b6 . d = FALSE ) ) ) ) );

definition
let V, A be set ;
let loc be V -valued Function;
let b0 be Complex;
let n0 be Nat;
let d be object ;
pred power_inv_pred A,loc,b0,n0,d means :: NOMIN_6:def 11
 ex d1 being NonatomicND of V,A st
( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = b0 & d1 . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 5) & S = b0 |^ I ) );
end;

:: deftheorem defines power_inv_pred NOMIN_6:def 11 :
for V, A being set
for loc being b1 -valued Function
for b0 being Complex
for n0 being Nat
for d being object holds
( power_inv_pred A,loc,b0,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = b0 & d1 . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 5) & S = b0 |^ I ) ) );

definition
let V, A be set ;
let loc be V -valued Function;
let b0 be Complex;
let n0 be Nat;
defpred S1[ object ] means power_inv_pred A,loc,b0,n0,$1;
func power_inv (A,loc,b0,n0) -> SCPartialNominativePredicate of V,A means :Def12: :: NOMIN_6:def 12
( dom it = ND (V,A) & ( for d being object st d in dom it holds
( ( power_inv_pred A,loc,b0,n0,d implies it . d = TRUE ) & ( not power_inv_pred A,loc,b0,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
( ( power_inv_pred A,loc,b0,n0,d implies b1 . d = TRUE ) & ( not power_inv_pred A,loc,b0,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
( ( power_inv_pred A,loc,b0,n0,d implies b1 . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( power_inv_pred A,loc,b0,n0,d implies b2 . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines power_inv NOMIN_6:def 12 :
for V, A being set
for loc being b1 -valued Function
for b0 being Complex
for n0 being Nat
for b6 being SCPartialNominativePredicate of V,A holds
( b6 = power_inv (A,loc,b0,n0) iff ( dom b6 = ND (V,A) & ( for d being object st d in dom b6 holds
( ( power_inv_pred A,loc,b0,n0,d implies b6 . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b6 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let loc be V -valued Function;
let b0 be Complex;
let n0 be Nat;
cluster power_inv (A,loc,b0,n0) -> total ;
coherence
power_inv (A,loc,b0,n0) is total by Def12;
end;

definition
let V be set ;
let loc be V -valued Function;
let val be Function;
pred loc,val are_compatible_wrt_5_locs means :: NOMIN_6:def 13
( val . 5 <> loc /. 4 & val . 5 <> loc /. 3 & val . 5 <> loc /. 2 & val . 5 <> loc /. 1 & 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_5_locs NOMIN_6:def 13 :
for V being set
for loc being b1 -valued Function
for val being Function holds
( loc,val are_compatible_wrt_5_locs iff ( val . 5 <> loc /. 4 & val . 5 <> loc /. 3 & val . 5 <> loc /. 2 & val . 5 <> loc /. 1 & 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 Th4: :: NOMIN_6:4
for V, A being set
for loc being b1 -valued Function
for val being Function
for n0 being Nat
for b0 being Complex st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs holds
<*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
proof end;

theorem Th5: :: NOMIN_6:5
for V, A being set
for loc being b1 -valued Function
for n0 being Nat
for b0 being Complex st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct holds
<*(power_inv (A,loc,b0,n0)),(power_loop_body (A,loc)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
proof end;

theorem :: NOMIN_6:6
canceled;

::$CT
theorem Th7: :: NOMIN_6:7
for V, A being set
for loc being b1 -valued Function
for n0 being Nat
for b0 being Complex st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct holds
<*(power_inv (A,loc,b0,n0)),(power_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A))
proof end;

theorem Th8: :: NOMIN_6:8
for V, A being set
for loc being b1 -valued Function
for val being Function
for n0 being Nat
for b0 being Complex st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs holds
<*(valid_power_input (V,A,val,b0,n0)),(power_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A))
proof end;

theorem Th9: :: NOMIN_6:9
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for n0 being Nat
for b0 being Complex 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 ) & ( for T being TypeSCNominativeData of V,A holds loc /. 4 is_a_value_on T ) holds
PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))) ||= SC_Psuperpos ((valid_power_output (A,z,b0,n0)),(denaming (V,A,(loc /. 5))),z)
proof end;

theorem Th10: :: NOMIN_6:10
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for n0 being Nat
for b0 being Complex 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 ) & ( for T being TypeSCNominativeData of V,A holds loc /. 4 is_a_value_on T ) holds
<*(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0)))),(SC_assignment ((denaming (V,A,(loc /. 5))),z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
proof end;

theorem Th11: :: NOMIN_6:11
for V, A being set
for z being Element of V
for loc being b1 -valued Function
for n0 being Nat
for b0 being Complex st ( for T being TypeSCNominativeData of V,A holds loc /. 1 is_a_value_on T ) & ( for T being TypeSCNominativeData of V,A holds loc /. 4 is_a_value_on T ) holds
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))),(SC_assignment ((denaming (V,A,(loc /. 5))),z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
proof end;

:: WP: Partial correctness of a POWER algorithm
theorem :: NOMIN_6:12
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
for b0 being Complex st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs & ( for T being TypeSCNominativeData of V,A holds loc /. 1 is_a_value_on T ) & ( for T being TypeSCNominativeData of V,A holds loc /. 4 is_a_value_on T ) holds
<*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
proof end;