:: by Adrian Jaszczak and Artur Korni{\l}owicz

::

:: Received May 27, 2019

:: Copyright (c) 2019 Association of Mizar Users

definition

let D be set ;

let f1, f2, f3 be BinominativeFunction of D;

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

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

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

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

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;

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

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

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

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

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

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

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;

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

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

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

ex b_{1}, x1, y1 being Complex st

( x1 = x & y1 = y & b_{1} = x1 + y1 )

for b_{1}, b_{2} being Complex st ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{1} = x1 + y1 ) & ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{2} = x1 + y1 ) holds

b_{1} = b_{2}
;

ex b_{1}, x1, y1 being Complex st

( x1 = x & y1 = y & b_{1} = x1 * y1 )

for b_{1}, b_{2} being Complex st ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{1} = x1 * y1 ) & ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{2} = x1 * y1 ) holds

b_{1} = b_{2}
;

end;
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 x1, y1 being Complex st

( x1 = x & y1 = y & it = x1 + y1 );

ex b

( x1 = x & y1 = y & b

proof end;

uniqueness for b

( x1 = x & y1 = y & b

( x1 = x & y1 = y & b

b

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 x1, y1 being Complex st

( x1 = x & y1 = y & it = x1 * y1 );

ex b

( x1 = x & y1 = y & b

proof end;

uniqueness for b

( x1 = x & y1 = y & b

( x1 = x & y1 = y & b

b

:: deftheorem Def3 defines addition NOMIN_5:def 3 :

for x, y being object st x is Complex & y is Complex holds

for b_{3} being Complex holds

( b_{3} = addition (x,y) iff ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{3} = x1 + y1 ) );

for x, y being object st x is Complex & y is Complex holds

for b

( b

( x1 = x & y1 = y & b

:: deftheorem Def4 defines multiplication NOMIN_5:def 4 :

for x, y being object st x is Complex & y is Complex holds

for b_{3} being Complex holds

( b_{3} = multiplication (x,y) iff ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{3} = x1 * y1 ) );

for x, y being object st x is Complex & y is Complex holds

for b

( b

( x1 = x & y1 = y & b

definition

let A be set ;

assume A1: A is complex-containing ;

deffunc H_{1}( object , object ) -> Complex = addition ($1,$2);

ex b_{1} being Function of [:A,A:],A st

for x, y being object st x in A & y in A holds

b_{1} . (x,y) = addition (x,y)

for b_{1}, b_{2} being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds

b_{1} . (x,y) = addition (x,y) ) & ( for x, y being object st x in A & y in A holds

b_{2} . (x,y) = addition (x,y) ) holds

b_{1} = b_{2}
_{2}( object , object ) -> Complex = multiplication ($1,$2);

ex b_{1} being Function of [:A,A:],A st

for x, y being object st x in A & y in A holds

b_{1} . (x,y) = multiplication (x,y)

for b_{1}, b_{2} being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds

b_{1} . (x,y) = multiplication (x,y) ) & ( for x, y being object st x in A & y in A holds

b_{2} . (x,y) = multiplication (x,y) ) holds

b_{1} = b_{2}

end;
assume A1: A is complex-containing ;

deffunc H

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 for x, y being object st x in A & y in A holds

it . (x,y) = addition (x,y);

ex b

for x, y being object st x in A & y in A holds

b

proof end;

uniqueness for b

b

b

b

proof end;

deffunc H
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 for x, y being object st x in A & y in A holds

it . (x,y) = multiplication (x,y);

ex b

for x, y being object st x in A & y in A holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines addition NOMIN_5:def 5 :

for A being set st A is complex-containing holds

for b_{2} being Function of [:A,A:],A holds

( b_{2} = addition A iff for x, y being object st x in A & y in A holds

b_{2} . (x,y) = addition (x,y) );

for A being set st A is complex-containing holds

for b

( b

b

:: deftheorem Def6 defines multiplication NOMIN_5:def 6 :

for A being set st A is complex-containing holds

for b_{2} being Function of [:A,A:],A holds

( b_{2} = multiplication A iff for x, y being object st x in A & y in A holds

b_{2} . (x,y) = multiplication (x,y) );

for A being set st A is complex-containing holds

for b

( b

b

definition

let V, A be set ;

let x, y be Element of V;

lift_binary_op ((addition A),x,y) is SCBinominativeFunction of V,A ;

lift_binary_op ((multiplication A),x,y) is SCBinominativeFunction of V,A ;

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

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

lift_binary_op ((multiplication A),x,y) is SCBinominativeFunction of V,A ;

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

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

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

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

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;

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

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 ;

:: deftheorem defines factorial_loop_body NOMIN_5:def 9 :

for V, A being set

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

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 /. 3)))),(factorial_loop_body (A,loc))) is SCBinominativeFunction of V,A ;

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

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

:: deftheorem defines factorial_main_loop NOMIN_5:def 10 :

for V, A being set

for loc being b_{1} -valued Function holds factorial_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_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)))) is SCBinominativeFunction of V,A ;

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

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 ;

:: deftheorem defines factorial_var_init NOMIN_5:def 11 :

for V, A being set

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

for V, A being set

for loc being b

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;

PP_composition ((factorial_var_init (A,loc,val)),(factorial_main_loop (A,loc))) is SCBinominativeFunction of V,A ;

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

PP_composition ((factorial_var_init (A,loc,val)),(factorial_main_loop (A,loc))) is SCBinominativeFunction of V,A ;

:: deftheorem defines factorial_main_part NOMIN_5:def 12 :

for V, A being set

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

for V, A being set

for loc being b

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;

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

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

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

:: deftheorem defines factorial_program NOMIN_5:def 13 :

for V, A being set

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

for V, A being set

for loc being b

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

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

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 S_{1}[ object ] means valid_factorial_input_pred V,A,val,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_factorial_input_pred V,A,val,n0,d implies b_{1} . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,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_factorial_input_pred V,A,val,n0,d implies b_{1} . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,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_factorial_input_pred V,A,val,n0,d implies b_{2} . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let val be Function;

let n0 be Nat;

defpred S

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

ex b

( dom b

( ( valid_factorial_input_pred V,A,val,n0,d implies b

proof end;

uniqueness for b

( ( valid_factorial_input_pred V,A,val,n0,d implies b

( ( valid_factorial_input_pred V,A,val,n0,d implies b

b

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

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

( ( valid_factorial_input_pred V,A,val,n0,d implies b_{5} . d = TRUE ) & ( not valid_factorial_input_pred V,A,val,n0,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for val being Function

for n0 being Nat

for b

( b

( ( valid_factorial_input_pred V,A,val,n0,d implies b

registration

let V, A be set ;

let val be Function;

let n0 be Nat;

coherence

valid_factorial_input (V,A,val,n0) is total by Def15;

end;
let val be Function;

let n0 be Nat;

coherence

valid_factorial_input (V,A,val,n0) is total by Def15;

definition

let V, A be set ;

let z be Element of V;

let n0 be Nat;

let d be object ;

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

ex d1 being NonatomicND of V,A st

( d = d1 & z in dom d1 & d1 . z = n0 ! );

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

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 S_{1}[ object ] means valid_factorial_output_pred A,z,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_factorial_output_pred A,z,n0,d implies b_{1} . d = TRUE ) & ( not valid_factorial_output_pred A,z,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_factorial_output_pred A,z,n0,d implies b_{1} . d = TRUE ) & ( not valid_factorial_output_pred A,z,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_factorial_output_pred A,z,n0,d implies b_{2} . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

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

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

ex b

( dom b

( ( valid_factorial_output_pred A,z,n0,d implies b

proof end;

uniqueness for b

( ( valid_factorial_output_pred A,z,n0,d implies b

( ( valid_factorial_output_pred A,z,n0,d implies b

b

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

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

( ( valid_factorial_output_pred A,z,n0,d implies b_{5} . d = TRUE ) & ( not valid_factorial_output_pred A,z,n0,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for z being Element of V

for n0 being Nat

for b

( b

( ( valid_factorial_output_pred A,z,n0,d implies b

:: deftheorem defines factorial_inv_pred NOMIN_5:def 18 :

for V, A being set

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

for V, A being set

for loc being b

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 S_{1}[ object ] means factorial_inv_pred A,loc,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

( ( factorial_inv_pred A,loc,n0,d implies b_{1} . d = TRUE ) & ( not factorial_inv_pred A,loc,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

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

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

b_{1} = b_{2}

end;
let loc be V -valued Function;

let n0 be Nat;

defpred S

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

ex b

( dom b

( ( factorial_inv_pred A,loc,n0,d implies b

proof end;

uniqueness for b

( ( factorial_inv_pred A,loc,n0,d implies b

( ( factorial_inv_pred A,loc,n0,d implies b

b

proof end;

:: deftheorem Def19 defines factorial_inv NOMIN_5:def 19 :

for V, A being set

for loc being b_{1} -valued Function

for n0 being Nat

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

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

( ( factorial_inv_pred A,loc,n0,d implies b_{5} . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b_{5} . d = FALSE ) ) ) ) );

for V, A being set

for loc being b

for n0 being Nat

for b

( b

( ( factorial_inv_pred A,loc,n0,d implies b

registration

let V, A be set ;

let loc be V -valued Function;

let n0 be Nat;

coherence

factorial_inv (A,loc,n0) is total by Def19;

end;
let loc be V -valued Function;

let n0 be Nat;

coherence

factorial_inv (A,loc,n0) is total by Def19;

:: deftheorem defines are_compatible_wrt_4_locs NOMIN_5:def 20 :

for V being set

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

for V being set

for loc being b

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

for loc being b

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

for loc being b

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 Th8: :: NOMIN_5:8

for V, A being set

for loc being b_{1} -valued Function

for n0 being Nat holds <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))

for loc being b

for n0 being Nat holds <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))

proof end;

theorem Th9: :: NOMIN_5:9

for V, A being set

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

for loc being b

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

for loc being b

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

for z being Element of V

for loc being b

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

for z being Element of V

for loc being b

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

for z being Element of V

for loc being b

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;

theorem :: NOMIN_5:14

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

for z being Element of V

for loc being b

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;