:: by Adrian Jaszczak

::

:: Received May 27, 2019

:: Copyright (c) 2019 Association of Mizar Users

definition

let D be set ;

let f1, f2, f3, f4, f5 be BinominativeFunction of D;

PP_composition ((PP_composition (f1,f2,f3,f4)),f5) is BinominativeFunction of D ;

end;
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);

PP_composition ((PP_composition (f1,f2,f3,f4)),f5) is BinominativeFunction of D ;

:: 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);

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);

:: 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

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

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

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;

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;
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))));

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 ;

:: deftheorem defines power_loop_body NOMIN_6:def 2 :

for V, A being set

for loc being b_{1} -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))));

for V, A being set

for loc being b

definition

let V, A be set ;

let loc be V -valued Function;

PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_loop_body (A,loc))) is SCBinominativeFunction of V,A ;

end;
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)));

PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_loop_body (A,loc))) is SCBinominativeFunction of V,A ;

:: deftheorem defines power_main_loop NOMIN_6:def 3 :

for V, A being set

for loc being b_{1} -valued Function holds power_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_loop_body (A,loc)));

for V, A being set

for loc being b

definition

let V, A be set ;

let loc be V -valued Function;

let val be Function;

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;
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))));

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 ;

:: deftheorem defines power_var_init NOMIN_6:def 4 :

for V, A being set

for loc being b_{1} -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))));

for V, A being set

for loc being b

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;

PP_composition ((power_var_init (A,loc,val)),(power_main_loop (A,loc))) is SCBinominativeFunction of V,A ;

end;
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)));

PP_composition ((power_var_init (A,loc,val)),(power_main_loop (A,loc))) is SCBinominativeFunction of V,A ;

:: deftheorem defines power_main_part NOMIN_6:def 5 :

for V, A being set

for loc being b_{1} -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)));

for V, A being set

for loc being b

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;

PP_composition ((power_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 5))),z))) is SCBinominativeFunction of V,A ;

end;
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)));

PP_composition ((power_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 5))),z))) is SCBinominativeFunction of V,A ;

:: deftheorem defines power_program NOMIN_6:def 6 :

for V, A being set

for loc being b_{1} -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)));

for V, A being set

for loc being b

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
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 ) );

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 S_{1}[ object ] means valid_power_input_pred V,A,val,b0,n0,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( valid_power_input_pred V,A,val,b0,n0,d implies b_{1} . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( valid_power_input_pred V,A,val,b0,n0,d implies b_{1} . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = ND (V,A) & ( for d being object st d in dom b_{2} holds

( ( valid_power_input_pred V,A,val,b0,n0,d implies b_{2} . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let val be Function;

let b0 be Complex;

let n0 be Nat;

defpred S

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 ( 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 ) ) ) );

ex b

( dom b

( ( valid_power_input_pred V,A,val,b0,n0,d implies b

proof end;

uniqueness for b

( ( valid_power_input_pred V,A,val,b0,n0,d implies b

( ( valid_power_input_pred V,A,val,b0,n0,d implies b

b

proof 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 b_{6} being SCPartialNominativePredicate of V,A holds

( b_{6} = valid_power_input (V,A,val,b0,n0) iff ( dom b_{6} = ND (V,A) & ( for d being object st d in dom b_{6} holds

( ( valid_power_input_pred V,A,val,b0,n0,d implies b_{6} . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b_{6} . d = FALSE ) ) ) ) );

for V, A being set

for val being Function

for b0 being Complex

for n0 being Nat

for b

( b

( ( valid_power_input_pred V,A,val,b0,n0,d implies b

registration

let V, A be set ;

let val be Function;

let b0 be Complex;

let n0 be Nat;

coherence

valid_power_input (V,A,val,b0,n0) is total by Def8;

end;
let val be Function;

let b0 be Complex;

let n0 be Nat;

coherence

valid_power_input (V,A,val,b0,n0) is total by Def8;

definition

let V, A be set ;

let z be Element of V;

let b0 be Complex;

let n0 be Nat;

let d be object ;

end;
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 );

ex d1 being NonatomicND of V,A st

( d = d1 & z in dom d1 & d1 . z = b0 |^ n0 );

:: 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 ) );

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 S_{1}[ object ] means valid_power_output_pred A,z,b0,n0,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{1} holds

( ( valid_power_output_pred A,z,b0,n0,d implies b_{1} . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{1} holds

( ( valid_power_output_pred A,z,b0,n0,d implies b_{1} . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{2} holds

( ( valid_power_output_pred A,z,b0,n0,d implies b_{2} . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
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 S

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 ( 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 ) ) ) );

ex b

( dom b

( ( valid_power_output_pred A,z,b0,n0,d implies b

proof end;

uniqueness for b

( ( valid_power_output_pred A,z,b0,n0,d implies b

( ( valid_power_output_pred A,z,b0,n0,d implies b

b

proof 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 b_{6} being SCPartialNominativePredicate of V,A holds

( b_{6} = valid_power_output (A,z,b0,n0) iff ( dom b_{6} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{6} holds

( ( valid_power_output_pred A,z,b0,n0,d implies b_{6} . d = TRUE ) & ( not valid_power_output_pred A,z,b0,n0,d implies b_{6} . d = FALSE ) ) ) ) );

for V, A being set

for z being Element of V

for b0 being Complex

for n0 being Nat

for b

( b

( ( valid_power_output_pred A,z,b0,n0,d implies b

definition

let V, A be set ;

let loc be V -valued Function;

let b0 be Complex;

let n0 be Nat;

let d be object ;

end;
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 ) );

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 ) );

:: deftheorem defines power_inv_pred NOMIN_6:def 11 :

for V, A being set

for loc being b_{1} -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 ) ) );

for V, A being set

for loc being b

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 S_{1}[ object ] means power_inv_pred A,loc,b0,n0,$1;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( power_inv_pred A,loc,b0,n0,d implies b_{1} . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( power_inv_pred A,loc,b0,n0,d implies b_{1} . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = ND (V,A) & ( for d being object st d in dom b_{2} holds

( ( power_inv_pred A,loc,b0,n0,d implies b_{2} . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let loc be V -valued Function;

let b0 be Complex;

let n0 be Nat;

defpred S

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 ( 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 ) ) ) );

ex b

( dom b

( ( power_inv_pred A,loc,b0,n0,d implies b

proof end;

uniqueness for b

( ( power_inv_pred A,loc,b0,n0,d implies b

( ( power_inv_pred A,loc,b0,n0,d implies b

b

proof end;

:: deftheorem Def12 defines power_inv NOMIN_6:def 12 :

for V, A being set

for loc being b_{1} -valued Function

for b0 being Complex

for n0 being Nat

for b_{6} being SCPartialNominativePredicate of V,A holds

( b_{6} = power_inv (A,loc,b0,n0) iff ( dom b_{6} = ND (V,A) & ( for d being object st d in dom b_{6} holds

( ( power_inv_pred A,loc,b0,n0,d implies b_{6} . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b_{6} . d = FALSE ) ) ) ) );

for V, A being set

for loc being b

for b0 being Complex

for n0 being Nat

for b

( b

( ( power_inv_pred A,loc,b0,n0,d implies b

registration

let V, A be set ;

let loc be V -valued Function;

let b0 be Complex;

let n0 be Nat;

coherence

power_inv (A,loc,b0,n0) is total by Def12;

end;
let loc be V -valued Function;

let b0 be Complex;

let n0 be Nat;

coherence

power_inv (A,loc,b0,n0) is total by Def12;

:: deftheorem defines are_compatible_wrt_5_locs NOMIN_6:def 13 :

for V being set

for loc being b_{1} -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 ) );

for V being set

for loc being b

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 b_{1} -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))

for loc being b

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 b_{1} -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))

for loc being b

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 Th6: :: NOMIN_6:6

for V, A being set

for loc being b_{1} -valued Function

for n0 being Nat

for b0 being Complex holds <*(PP_inversion (power_inv (A,loc,b0,n0))),(power_loop_body (A,loc)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))

for loc being b

for n0 being Nat

for b0 being Complex holds <*(PP_inversion (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 Th7: :: NOMIN_6:7

for V, A being set

for loc being b_{1} -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))

for loc being b

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 b_{1} -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))

for loc being b

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 b_{1} -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)

for z being Element of V

for loc being b

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 b_{1} -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))

for z being Element of V

for loc being b

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 b_{1} -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))

for z being Element of V

for loc being b

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;

theorem :: NOMIN_6:12

for V, A being set

for z being Element of V

for loc being b_{1} -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))

for z being Element of V

for loc being b

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;