nomin_5.miz



    begin

    definition

      let D be set;

      let f1,f2,f3 be BinominativeFunction of D;

      :: NOMIN_5:def1

      func PP_composition (f1,f2,f3) -> BinominativeFunction of D equals ( PP_composition (( PP_composition (f1,f2)),f3));

      coherence ;

    end

    definition

      let D be set;

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

      :: NOMIN_5:def2

      func PP_composition (f1,f2,f3,f4) -> BinominativeFunction of D equals ( PP_composition (( PP_composition (f1,f2,f3)),f4));

      coherence ;

    end

    reserve D for non empty set;

    reserve f1,f2,f3,f4 for BinominativeFunction of D;

    reserve p,q,r,t,w for PartialPredicate of D;

    ::$Notion-Name

    theorem :: NOMIN_5:1

     <*p, f1, q*> is SFHT of D & <*q, f2, r*> is SFHT of D & <*r, f3, w*> is SFHT of D & <*( PP_inversion q), f2, r*> is SFHT of D & <*( PP_inversion r), f3, w*> is SFHT of D implies <*p, ( PP_composition (f1,f2,f3)), w*> is SFHT of D

    proof

      assume that

       A1: <*p, f1, q*> is SFHT of D and

       A2: <*q, f2, r*> is SFHT of D and

       A3: <*r, f3, w*> is SFHT of D and

       A4: <*( PP_inversion q), f2, r*> is SFHT of D and

       A5: <*( PP_inversion r), f3, w*> is SFHT of D;

       <*p, ( PP_composition (f1,f2)), r*> is SFHT of D by A1, A2, A4, NOMIN_3: 25;

      hence thesis by A3, A5, NOMIN_3: 25;

    end;

    ::$Notion-Name

    theorem :: NOMIN_5:2

    

     Th2: <*p, f1, q*> is SFHT of D & <*q, f2, r*> is SFHT of D & <*r, f3, w*> is SFHT of D & <*w, f4, t*> is SFHT of D & <*( PP_inversion q), f2, r*> is SFHT of D & <*( PP_inversion r), f3, w*> is SFHT of D & <*( PP_inversion w), f4, t*> is SFHT of D implies <*p, ( PP_composition (f1,f2,f3,f4)), t*> is SFHT of D

    proof

      assume that

       A1: <*p, f1, q*> is SFHT of D and

       A2: <*q, f2, r*> is SFHT of D and

       A3: <*r, f3, w*> is SFHT of D and

       A4: <*w, f4, t*> is SFHT of D and

       A5: <*( PP_inversion q), f2, r*> is SFHT of D and

       A6: <*( PP_inversion r), f3, w*> is SFHT of D and

       A7: <*( PP_inversion w), f4, t*> is SFHT of D;

       <*p, ( PP_composition (f1,f2)), r*> is SFHT of D by A1, A2, A5, NOMIN_3: 25;

      then <*p, ( PP_composition (( PP_composition (f1,f2)),f3)), w*> is SFHT of D by A3, A6, NOMIN_3: 25;

      hence thesis by A4, A7, NOMIN_3: 25;

    end;

    reserve d,v,v1 for object;

    reserve V,A for set;

    reserve z for Element of V;

    reserve d1 for NonatomicND of V, A;

    reserve f for SCBinominativeFunction of V, A;

    reserve T for TypeSCNominativeData of V, A;

    theorem :: NOMIN_5:3

    

     Th3: A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in ( dom d1) implies (( local_overlapping (V,A,d1,T,v)) . v1) = (d1 . v1)

    proof

      assume that

       A1: A is_without_nonatomicND_wrt V and

       A2: v in V & v <> v1;

       not d1 in A & not ( naming (V,A,v,T)) in A by A1, NOMIN_4: 3;

      hence thesis by A2, NOMIN_2: 12;

    end;

    definition

      let x,y be object;

      assume

       A1: x is Complex & y is Complex;

      :: NOMIN_5:def3

      func addition (x,y) -> Complex means

      : Def3: ex x1,y1 be Complex st x1 = x & y1 = y & it = (x1 + y1);

      existence

      proof

        reconsider x1 = x, y1 = y as Complex by A1;

        take (x1 + y1);

        thus thesis;

      end;

      uniqueness ;

      :: NOMIN_5:def4

      func multiplication (x,y) -> Complex means

      : Def4: ex x1,y1 be Complex st x1 = x & y1 = y & it = (x1 * y1);

      existence

      proof

        reconsider x1 = x, y1 = y as Complex by A1;

        take (x1 * y1);

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let A;

      assume

       A1: A is complex-containing;

      deffunc F( object, object) = ( addition ($1,$2));

      :: NOMIN_5:def5

      func addition (A) -> Function of [:A, A:], A means

      : Def5: for x,y be object st x in A & y in A holds (it . (x,y)) = ( addition (x,y));

      existence

      proof

        

         A2: for x,y be object st x in A & y in A holds F(x,y) in A

        proof

          let x,y be object such that x in A & y in A;

           F(x,y) in COMPLEX by XCMPLX_0:def 2;

          hence thesis by A1;

        end;

        consider f be Function of [:A, A:], A such that

         A3: for x,y be object st x in A & y in A holds (f . (x,y)) = F(x,y) from BINOP_1:sch 2( A2);

        take f;

        thus thesis by A3;

      end;

      uniqueness

      proof

        for f,g be Function of [:A, A:], A st (for x,y be object st x in A & y in A holds (f . (x,y)) = F(x,y)) & (for x,y be object st x in A & y in A holds (g . (x,y)) = F(x,y)) holds f = g from NOMIN_4:sch 3;

        hence thesis;

      end;

      deffunc G( object, object) = ( multiplication ($1,$2));

      :: NOMIN_5:def6

      func multiplication (A) -> Function of [:A, A:], A means

      : Def6: for x,y be object st x in A & y in A holds (it . (x,y)) = ( multiplication (x,y));

      existence

      proof

        

         A4: for x,y be object st x in A & y in A holds G(x,y) in A

        proof

          let x,y be object such that x in A & y in A;

           G(x,y) in COMPLEX by XCMPLX_0:def 2;

          hence thesis by A1;

        end;

        consider f be Function of [:A, A:], A such that

         A5: for x,y be object st x in A & y in A holds (f . (x,y)) = G(x,y) from BINOP_1:sch 2( A4);

        take f;

        thus thesis by A5;

      end;

      uniqueness

      proof

        for f,g be Function of [:A, A:], A st (for x,y be object st x in A & y in A holds (f . (x,y)) = G(x,y)) & (for x,y be object st x in A & y in A holds (g . (x,y)) = G(x,y)) holds f = g from NOMIN_4:sch 3;

        hence thesis;

      end;

    end

    definition

      let V, A;

      let x,y be Element of V;

      :: NOMIN_5:def7

      func addition (A,x,y) -> SCBinominativeFunction of V, A equals ( lift_binary_op (( addition A),x,y));

      coherence ;

      :: NOMIN_5:def8

      func multiplication (A,x,y) -> SCBinominativeFunction of V, A equals ( lift_binary_op (( multiplication A),x,y));

      coherence ;

    end

    theorem :: NOMIN_5:4

    

     Th4: for i,j be Element of V holds A is complex-containing & i in ( dom d1) & j in ( dom d1) & d1 in ( dom ( addition (A,i,j))) implies for x,y be Complex st x = (d1 . i) & y = (d1 . j) holds (( addition (A,i,j)) . d1) = (x + y)

    proof

      let i,j be Element of V;

      assume that

       A1: A is complex-containing and

       A2: i in ( dom d1) and

       A3: j in ( dom d1) and

       A4: d1 in ( dom ( addition (A,i,j)));

      let x,y be Complex such that

       A5: x = (d1 . i) & y = (d1 . j);

      set Di = ( denaming (V,A,i));

      set Dj = ( denaming (V,A,j));

      

       A6: d1 in ( dom <:Di, Dj:>) by A4, FUNCT_1: 11;

      then

       A7: ( <:Di, Dj:> . d1) = [(Di . d1), (Dj . d1)] by FUNCT_3:def 7;

      

       A8: ( dom <:Di, Dj:>) = (( dom Di) /\ ( dom Dj)) by FUNCT_3:def 7;

      then d1 in ( dom Di) by A6, XBOOLE_0:def 4;

      

      then

       A9: (Di . d1) = ( denaming (i,d1)) by NOMIN_1:def 18

      .= (d1 . i) by A2, NOMIN_1:def 12;

      d1 in ( dom Dj) by A6, A8, XBOOLE_0:def 4;

      

      then

       A10: (Dj . d1) = ( denaming (j,d1)) by NOMIN_1:def 18

      .= (d1 . j) by A3, NOMIN_1:def 12;

      

       A11: x in COMPLEX & y in COMPLEX by XCMPLX_0:def 2;

      

      thus (( addition (A,i,j)) . d1) = (( addition A) . ((Di . d1),(Dj . d1))) by A4, A7, FUNCT_1: 12

      .= ( addition ((Di . d1),(Dj . d1))) by A1, A5, A9, A10, A11, Def5

      .= (x + y) by A5, A9, A10, Def3;

    end;

    theorem :: NOMIN_5:5

    

     Th5: for i,j be Element of V holds A is complex-containing & i in ( dom d1) & j in ( dom d1) & d1 in ( dom ( multiplication (A,i,j))) implies for x,y be Complex st x = (d1 . i) & y = (d1 . j) holds (( multiplication (A,i,j)) . d1) = (x * y)

    proof

      let i,j be Element of V;

      assume that

       A1: A is complex-containing and

       A2: i in ( dom d1) and

       A3: j in ( dom d1) and

       A4: d1 in ( dom ( multiplication (A,i,j)));

      let x,y be Complex such that

       A5: x = (d1 . i) & y = (d1 . j);

      set Di = ( denaming (V,A,i));

      set Dj = ( denaming (V,A,j));

      

       A6: d1 in ( dom <:Di, Dj:>) by A4, FUNCT_1: 11;

      then

       A7: ( <:Di, Dj:> . d1) = [(Di . d1), (Dj . d1)] by FUNCT_3:def 7;

      

       A8: ( dom <:Di, Dj:>) = (( dom Di) /\ ( dom Dj)) by FUNCT_3:def 7;

      then d1 in ( dom Di) by A6, XBOOLE_0:def 4;

      

      then

       A9: (Di . d1) = ( denaming (i,d1)) by NOMIN_1:def 18

      .= (d1 . i) by A2, NOMIN_1:def 12;

      d1 in ( dom Dj) by A6, A8, XBOOLE_0:def 4;

      

      then

       A10: (Dj . d1) = ( denaming (j,d1)) by NOMIN_1:def 18

      .= (d1 . j) by A3, NOMIN_1:def 12;

      

       A11: x in COMPLEX & y in COMPLEX by XCMPLX_0:def 2;

      

      thus (( multiplication (A,i,j)) . d1) = (( multiplication A) . ((Di . d1),(Dj . d1))) by A4, A7, FUNCT_1: 12

      .= ( multiplication ((Di . d1),(Dj . d1))) by A1, A5, A9, A10, A11, Def6

      .= (x * y) by A5, A9, A10, Def4;

    end;

    reserve loc for V -valued Function;

    reserve val for Function;

    definition

      let V, A, loc;

      :: NOMIN_5:def9

      func factorial_loop_body (A,loc) -> SCBinominativeFunction of V, A equals ( PP_composition (( SC_assignment (( addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),( SC_assignment (( multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4)))));

      coherence ;

    end

    definition

      let V, A, loc;

      :: NOMIN_5:def10

      func factorial_main_loop (A,loc) -> SCBinominativeFunction of V, A equals ( PP_while (( PP_not ( Equality (A,(loc /. 1),(loc /. 3)))),( factorial_loop_body (A,loc))));

      coherence ;

    end

    definition

      let V, A, loc, val;

      :: NOMIN_5:def11

      func factorial_var_init (A,loc,val) -> SCBinominativeFunction of V, A equals ( PP_composition (( SC_assignment (( denaming (V,A,(val . 1))),(loc /. 1))),( SC_assignment (( denaming (V,A,(val . 2))),(loc /. 2))),( SC_assignment (( denaming (V,A,(val . 3))),(loc /. 3))),( SC_assignment (( denaming (V,A,(val . 4))),(loc /. 4)))));

      coherence ;

    end

    definition

      let V, A, loc, val;

      :: NOMIN_5:def12

      func factorial_main_part (A,loc,val) -> SCBinominativeFunction of V, A equals ( PP_composition (( factorial_var_init (A,loc,val)),( factorial_main_loop (A,loc))));

      coherence ;

    end

    definition

      let V, A, loc, val, z;

      :: NOMIN_5:def13

      func factorial_program (A,loc,val,z) -> SCBinominativeFunction of V, A equals ( PP_composition (( factorial_main_part (A,loc,val)),( SC_assignment (( denaming (V,A,(loc /. 4))),z))));

      coherence ;

    end

    reserve n0 for Nat;

    definition

      let V, A, val, n0, d;

      :: NOMIN_5:def14

      pred valid_factorial_input_pred V,A,val,n0,d means ex d1 be NonatomicND of V, A st d = d1 & {(val . 1), (val . 2), (val . 3), (val . 4)} c= ( dom d1) & (d1 . (val . 1)) = 0 & (d1 . (val . 2)) = 1 & (d1 . (val . 3)) = n0 & (d1 . (val . 4)) = 1;

    end

    definition

      let V, A, val, n0;

      defpred P[ object] means valid_factorial_input_pred (V,A,val,n0,$1);

      :: NOMIN_5:def15

      func valid_factorial_input (V,A,val,n0) -> SCPartialNominativePredicate of V, A means

      : Def15: ( dom it ) = ( ND (V,A)) & for d be object st d in ( dom it ) holds ( valid_factorial_input_pred (V,A,val,n0,d) implies (it . d) = TRUE ) & ( not valid_factorial_input_pred (V,A,val,n0,d) implies (it . d) = FALSE );

      existence

      proof

        

         A1: ( ND (V,A)) c= ( ND (V,A));

        consider p be SCPartialNominativePredicate of V, A such that

         A2: ( dom p) = ( ND (V,A)) & (for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE )) from PARTPR_2:sch 1( A1);

        take p;

        thus thesis by A2;

      end;

      uniqueness

      proof

        for p,q be SCPartialNominativePredicate of V, A st (( dom p) = ( ND (V,A)) & (for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE ))) & (( dom q) = ( ND (V,A)) & (for d be object st d in ( dom q) holds ( P[d] implies (q . d) = TRUE ) & ( not P[d] implies (q . d) = FALSE ))) holds p = q from PARTPR_2:sch 2;

        hence thesis;

      end;

    end

    registration

      let V, A, val, n0;

      cluster ( valid_factorial_input (V,A,val,n0)) -> total;

      coherence by Def15;

    end

    definition

      let V, A, z, n0, d;

      :: NOMIN_5:def16

      pred valid_factorial_output_pred A,z,n0,d means ex d1 be NonatomicND of V, A st d = d1 & z in ( dom d1) & (d1 . z) = (n0 ! );

    end

    definition

      let V, A, z, n0;

      set D = { d where d be TypeSCNominativeData of V, A : d in ( dom ( denaming (V,A,z))) };

      defpred P[ object] means valid_factorial_output_pred (A,z,n0,$1);

      :: NOMIN_5:def17

      func valid_factorial_output (A,z,n0) -> SCPartialNominativePredicate of V, A means

      : Def17: ( dom it ) = { d where d be TypeSCNominativeData of V, A : d in ( dom ( denaming (V,A,z))) } & for d be object st d in ( dom it ) holds ( valid_factorial_output_pred (A,z,n0,d) implies (it . d) = TRUE ) & ( not valid_factorial_output_pred (A,z,n0,d) implies (it . d) = FALSE );

      existence

      proof

        

         A1: D c= ( ND (V,A))

        proof

          let v;

          assume v in D;

          then ex d be TypeSCNominativeData of V, A st v = d & d in ( dom ( denaming (V,A,z)));

          hence thesis;

        end;

        consider p be SCPartialNominativePredicate of V, A such that

         A2: ( dom p) = D & (for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE )) from PARTPR_2:sch 1( A1);

        take p;

        thus thesis by A2;

      end;

      uniqueness

      proof

        for p,q be SCPartialNominativePredicate of V, A st (( dom p) = D & (for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE ))) & (( dom q) = D & (for d be object st d in ( dom q) holds ( P[d] implies (q . d) = TRUE ) & ( not P[d] implies (q . d) = FALSE ))) holds p = q from PARTPR_2:sch 2;

        hence thesis;

      end;

    end

    definition

      let V, A, loc, n0, d;

      :: NOMIN_5:def18

      pred factorial_inv_pred A,loc,n0,d means ex d1 be 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 be Nat st I = (d1 . (loc /. 1)) & S = (d1 . (loc /. 4)) & S = (I ! );

    end

    definition

      let V, A, loc, n0;

      defpred P[ object] means factorial_inv_pred (A,loc,n0,$1);

      :: NOMIN_5:def19

      func factorial_inv (A,loc,n0) -> SCPartialNominativePredicate of V, A means

      : Def19: ( dom it ) = ( ND (V,A)) & for d be object st d in ( dom it ) holds ( factorial_inv_pred (A,loc,n0,d) implies (it . d) = TRUE ) & ( not factorial_inv_pred (A,loc,n0,d) implies (it . d) = FALSE );

      existence

      proof

        

         A1: ( ND (V,A)) c= ( ND (V,A));

        consider p be SCPartialNominativePredicate of V, A such that

         A2: ( dom p) = ( ND (V,A)) & (for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE )) from PARTPR_2:sch 1( A1);

        take p;

        thus thesis by A2;

      end;

      uniqueness

      proof

        for p,q be SCPartialNominativePredicate of V, A st (( dom p) = ( ND (V,A)) & (for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE ))) & (( dom q) = ( ND (V,A)) & (for d be object st d in ( dom q) holds ( P[d] implies (q . d) = TRUE ) & ( not P[d] implies (q . d) = FALSE ))) holds p = q from PARTPR_2:sch 2;

        hence thesis;

      end;

    end

    registration

      let V, A, loc, n0;

      cluster ( factorial_inv (A,loc,n0)) -> total;

      coherence by Def19;

    end

    definition

      let V, loc, val;

      :: NOMIN_5:def20

      pred loc,val are_compatible_wrt_4_locs means (val . 4) <> (loc /. 3) & (val . 4) <> (loc /. 2) & (val . 4) <> (loc /. 1) & (val . 3) <> (loc /. 2) & (val . 3) <> (loc /. 1) & (val . 2) <> (loc /. 1);

    end

    theorem :: NOMIN_5:6

    

     Th6: V is non empty & A is_without_nonatomicND_wrt V & ((loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)) are_mutually_distinct & (loc,val) are_compatible_wrt_4_locs implies <*( valid_factorial_input (V,A,val,n0)), ( factorial_var_init (A,loc,val)), ( factorial_inv (A,loc,n0))*> is SFHT of ( ND (V,A))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4);

      set i1 = (val . 1), j1 = (val . 2), n1 = (val . 3), s1 = (val . 4);

      set D = ( ND (V,A));

      set I = ( valid_factorial_input (V,A,val,n0));

      set F = ( factorial_var_init (A,loc,val));

      set inv = ( factorial_inv (A,loc,n0));

      set Di = ( denaming (V,A,i1));

      set Dj = ( denaming (V,A,j1));

      set Dn = ( denaming (V,A,n1));

      set Ds = ( denaming (V,A,s1));

      set asi = ( SC_assignment (Di,i));

      set asj = ( SC_assignment (Dj,j));

      set asn = ( SC_assignment (Dn,n));

      set ass = ( SC_assignment (Ds,s));

      set S1 = ( SC_Psuperpos (inv,Ds,s));

      set R1 = ( SC_Psuperpos (S1,Dn,n));

      set Q1 = ( SC_Psuperpos (R1,Dj,j));

      set P1 = ( SC_Psuperpos (Q1,Di,i));

      assume that

       A1: V is non empty and

       A2: A is_without_nonatomicND_wrt V and

       A3: (i,j,n,s) are_mutually_distinct and

       A4: (loc,val) are_compatible_wrt_4_locs ;

      

       A5: <*Q1, asj, R1*> is SFHT of D by NOMIN_3: 29;

      

       A6: <*R1, asn, S1*> is SFHT of D by NOMIN_3: 29;

      

       A7: <*S1, ass, inv*> is SFHT of D by NOMIN_3: 29;

      

       A8: <*P1, asi, Q1*> is SFHT of D by NOMIN_3: 29;

      I ||= P1

      proof

        let d be Element of D;

        assume d in ( dom I) & (I . d) = TRUE ;

        then valid_factorial_input_pred (V,A,val,n0,d) by Def15;

        then

        consider d1 be NonatomicND of V, A such that

         A9: d = d1 and

         A10: {i1, j1, n1, s1} c= ( dom d1) and

         A11: (d1 . i1) = 0 and

         A12: (d1 . j1) = 1 and

         A13: (d1 . n1) = n0 and

         A14: (d1 . s1) = 1;

        

         A15: i1 in {i1, j1, n1, s1} by ENUMSET1:def 2;

        

         A16: j1 in {i1, j1, n1, s1} by ENUMSET1:def 2;

        

         A17: n1 in {i1, j1, n1, s1} by ENUMSET1:def 2;

        

         A18: s1 in {i1, j1, n1, s1} by ENUMSET1:def 2;

        

         A20: ( dom Di) = { d where d be NonatomicND of V, A : i1 in ( dom d) } by NOMIN_1:def 18;

        

         A21: ( dom Dj) = { d where d be NonatomicND of V, A : j1 in ( dom d) } by NOMIN_1:def 18;

        

         A22: ( dom Dn) = { d where d be NonatomicND of V, A : n1 in ( dom d) } by NOMIN_1:def 18;

        

         A23: ( dom Ds) = { d where d be NonatomicND of V, A : s1 in ( dom d) } by NOMIN_1:def 18;

        

         A24: ( dom P1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(Di . d),i)) in ( dom Q1) & d in ( dom Di) } by NOMIN_2:def 11;

        

         A25: ( dom Q1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(Dj . d),j)) in ( dom R1) & d in ( dom Dj) } by NOMIN_2:def 11;

        

         A26: ( dom R1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(Dn . d),n)) in ( dom S1) & d in ( dom Dn) } by NOMIN_2:def 11;

        

         A27: ( dom S1) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(Ds . d),s)) in ( dom inv) & d in ( dom Ds) } by NOMIN_2:def 11;

        reconsider Li = ( local_overlapping (V,A,d1,(Di . d1),i)) as NonatomicND of V, A by NOMIN_2: 9;

        reconsider Lj = ( local_overlapping (V,A,Li,(Dj . Li),j)) as NonatomicND of V, A by NOMIN_2: 9;

        reconsider Ln = ( local_overlapping (V,A,Lj,(Dn . Lj),n)) as NonatomicND of V, A by NOMIN_2: 9;

        reconsider Ls = ( local_overlapping (V,A,Ln,(Ds . Ln),s)) as NonatomicND of V, A by NOMIN_2: 9;

        

         A28: d1 in ( dom Di) by A10, A15, A20;

        then

         A29: (Di . d1) is TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

        then

         A30: ( dom Li) = ( {i} \/ ( dom d1)) by A1, A2, NOMIN_4: 4;

        ( dom inv) = D by Def19;

        then

         A31: Ls in ( dom inv);

        

         A32: j1 in ( dom Li) by A10, A16, A30, XBOOLE_0:def 3;

        then

         A33: Li in ( dom Dj) by A21;

        then

         A34: (Dj . Li) is TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

        then

         A35: ( dom Lj) = ( {j} \/ ( dom Li)) by A1, A2, NOMIN_4: 4;

        

         A36: n1 in ( dom Li) by A10, A17, A30, XBOOLE_0:def 3;

        then

         A37: n1 in ( dom Lj) by A35, XBOOLE_0:def 3;

        then

         A38: Lj in ( dom Dn) by A22;

        then

         A39: (Dn . Lj) is TypeSCNominativeData of V, A by PARTFUN1: 4, NOMIN_1: 39;

        then

         A40: ( dom Ln) = ( {n} \/ ( dom Lj)) by A1, A2, NOMIN_4: 4;

        

         A41: s1 in ( dom Li) by A10, A18, A30, XBOOLE_0:def 3;

        then

         A42: s1 in ( dom Lj) by A35, XBOOLE_0:def 3;

        then

         A43: s1 in ( dom Ln) by A40, XBOOLE_0:def 3;

        then

         A44: Ln in ( dom Ds) by A23;

        then

         A45: Ln in ( dom S1) by A27, A31;

        

         A46: Lj in ( dom R1) by A26, A45, A38;

        then

         A47: Li in ( dom Q1) by A25, A33;

        hence

         A48: d in ( dom P1) by A9, A24, A28;

        

         A49: factorial_inv_pred (A,loc,n0,Ls)

        proof

          take Ls;

          thus Ls = Ls;

          

           A50: (Ds . Ln) is TypeSCNominativeData of V, A by A44, PARTFUN1: 4, NOMIN_1: 39;

          then

           A51: ( dom Ls) = ( {s} \/ ( dom Ln)) by A1, A2, NOMIN_4: 4;

          i in {i} by TARSKI:def 1;

          then

           A52: i in ( dom Li) by A30, XBOOLE_0:def 3;

          then

           A53: i in ( dom Lj) by A35, XBOOLE_0:def 3;

          then

           A54: i in ( dom Ln) by A40, XBOOLE_0:def 3;

          then

           A55: i in ( dom Ls) by A51, XBOOLE_0:def 3;

          j in {j} by TARSKI:def 1;

          then

           A56: j in ( dom Lj) by A35, XBOOLE_0:def 3;

          then

           A57: j in ( dom Ln) by A40, XBOOLE_0:def 3;

          then

           A58: j in ( dom Ls) by A51, XBOOLE_0:def 3;

          n in {n} by TARSKI:def 1;

          then

           A59: n in ( dom Ln) by A40, XBOOLE_0:def 3;

          then

           A60: n in ( dom Ls) by A51, XBOOLE_0:def 3;

          s in {s} by TARSKI:def 1;

          then s in ( dom Ls) by A51, XBOOLE_0:def 3;

          hence {i, j, n, s} c= ( dom Ls) by A55, A58, A60, ENUMSET1:def 2;

          

          thus (Ls . j) = (Ln . j) by A1, A2, A3, A50, A57, Th3

          .= (Lj . j) by A1, A2, A3, A39, A56, Th3

          .= (Dj . Li) by A1, A34, NOMIN_2: 10

          .= ( denaming (j1,Li)) by A33, NOMIN_1:def 18

          .= (Li . j1) by A32, NOMIN_1:def 12

          .= 1 by A1, A2, A4, A10, A16, A12, A29, Th3;

          

          thus (Ls . n) = (Ln . n) by A1, A2, A3, A50, A59, Th3

          .= (Dn . Lj) by A1, A39, NOMIN_2: 10

          .= ( denaming (n1,Lj)) by A38, NOMIN_1:def 18

          .= (Lj . n1) by A37, NOMIN_1:def 12

          .= (Li . n1) by A1, A2, A4, A34, A36, Th3

          .= n0 by A1, A2, A4, A10, A17, A13, A29, Th3;

          

           A61: (Ln . s1) = (Lj . s1) by A1, A2, A4, A42, A39, Th3

          .= (Li . s1) by A1, A2, A4, A34, A41, Th3

          .= 1 by A1, A2, A4, A10, A18, A14, A29, Th3;

          take 0 , 1;

          

          thus (Ls . i) = (Ln . i) by A1, A2, A3, A50, A54, Th3

          .= (Lj . i) by A1, A2, A3, A53, A39, Th3

          .= (Li . i) by A1, A2, A3, A34, A52, Th3

          .= (Di . d1) by A1, A29, NOMIN_2: 10

          .= ( denaming (i1,d1)) by A28, NOMIN_1:def 18

          .= 0 by A10, A11, A15, NOMIN_1:def 12;

          

          thus (Ls . s) = (Ds . Ln) by A1, A50, NOMIN_2: 10

          .= ( denaming (s1,Ln)) by A44, NOMIN_1:def 18

          .= 1 by A61, A43, NOMIN_1:def 12;

          thus 1 = ( 0 ! ) by NEWTON: 12;

        end;

        

        thus (P1 . d) = (Q1 . Li) by A9, A48, NOMIN_2: 35

        .= (R1 . Lj) by A47, NOMIN_2: 35

        .= (S1 . Ln) by A46, NOMIN_2: 35

        .= (inv . Ls) by A45, NOMIN_2: 35

        .= TRUE by A31, A49, Def19;

      end;

      then

       A62: <*I, asi, Q1*> is SFHT of D by A8, NOMIN_3: 15;

      

       A63: <*( PP_inversion Q1), asj, R1*> is SFHT of D by NOMIN_4: 16;

      

       A64: <*( PP_inversion R1), asn, S1*> is SFHT of D by NOMIN_4: 16;

       <*( PP_inversion S1), ass, inv*> is SFHT of D by NOMIN_4: 16;

      hence thesis by A62, A5, A6, A7, A63, A64, Th2;

    end;

    theorem :: NOMIN_5:7

    

     Th7: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & ((loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)) are_mutually_distinct implies <*( factorial_inv (A,loc,n0)), ( factorial_loop_body (A,loc)), ( factorial_inv (A,loc,n0))*> is SFHT of ( ND (V,A))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4);

      assume that

       A1: V is non empty and

       A2: A is complex-containing and

       A3: A is_without_nonatomicND_wrt V and

       A4: (i,j,n,s) are_mutually_distinct ;

      set D = ( ND (V,A));

      set inv = ( factorial_inv (A,loc,n0));

      set B = ( factorial_loop_body (A,loc));

      set add = ( addition (A,i,j));

      set mlt = ( multiplication (A,s,i));

      set f = ( SC_assignment (add,i));

      set g = ( SC_assignment (mlt,s));

      set Di = ( denaming (V,A,i));

      set Dj = ( denaming (V,A,j));

      set Dn = ( denaming (V,A,n));

      set Ds = ( denaming (V,A,s));

      now

        let d be TypeSCNominativeData of V, A such that

         A5: d in ( dom inv) and

         A6: (inv . d) = TRUE and

         A7: d in ( dom B) and

         A8: (B . d) in ( dom inv);

         factorial_inv_pred (A,loc,n0,d) by A5, A6, Def19;

        then

        consider d1 be NonatomicND of V, A such that

         A9: d = d1 and

         A10: {i, j, n, s} c= ( dom d1) and

         A11: (d1 . j) = 1 and

         A12: (d1 . n) = n0 and

         A13: ex I,S be Nat st I = (d1 . i) & S = (d1 . s) & S = (I ! );

        

         A14: i in {i, j, n, s} by ENUMSET1:def 2;

        

         A15: j in {i, j, n, s} by ENUMSET1:def 2;

        

         A16: n in {i, j, n, s} by ENUMSET1:def 2;

        

         A17: s in {i, j, n, s} by ENUMSET1:def 2;

        consider I,S be Nat such that

         A18: I = (d1 . i) and

         A19: S = (d1 . s) and

         A20: S = (I ! ) by A13;

        

         A21: ( dom f) = ( dom add) by NOMIN_2:def 7;

        

         A22: ( dom g) = ( dom mlt) by NOMIN_2:def 7;

        

         A23: ( PP_composition (f,g)) = (g * f) by PARTPR_2:def 1;

        then

         A24: d in ( dom f) by A7, FUNCT_1: 11;

        then

        reconsider Ad = (add . d1) as TypeSCNominativeData of V, A by A21, A9, PARTFUN1: 4, NOMIN_1: 39;

        reconsider La = ( local_overlapping (V,A,d1,Ad,i)) as NonatomicND of V, A by NOMIN_2: 9;

        reconsider Lm = ( local_overlapping (V,A,La,(mlt . La),s)) as NonatomicND of V, A by NOMIN_2: 9;

        B = (g * f) by PARTPR_2:def 1;

        then

         A25: (B . d) = (g . (f . d)) by A7, FUNCT_1: 12;

        

         A26: (f . d) = La by A9, A24, NOMIN_2:def 7;

        then

         A27: La in ( dom g) by A7, A23, FUNCT_1: 11;

        

         A28: (g . La) = Lm by A27, NOMIN_2:def 7;

         factorial_inv_pred (A,loc,n0,Lm)

        proof

          take Lm;

          thus Lm = Lm;

          

           A29: (mlt . La) is TypeSCNominativeData of V, A by A22, A27, PARTFUN1: 4, NOMIN_1: 39;

          

           A30: ( dom Lm) = (( dom La) \/ {s}) by A3, A1, A22, A27, A28, NOMIN_4: 5;

          

           A31: ( dom La) = ( {i} \/ ( dom d1)) by A3, A1, NOMIN_4: 4;

          i in {i} by TARSKI:def 1;

          then

           A32: i in ( dom La) by A31, XBOOLE_0:def 3;

          then

           A33: i in ( dom Lm) by A30, XBOOLE_0:def 3;

          

           A34: j in ( dom La) by A10, A15, A31, XBOOLE_0:def 3;

          then

           A35: j in ( dom Lm) by A30, XBOOLE_0:def 3;

          

           A36: n in ( dom La) by A10, A16, A31, XBOOLE_0:def 3;

          then

           A37: n in ( dom Lm) by A30, XBOOLE_0:def 3;

          s in {s} by TARSKI:def 1;

          then s in ( dom Lm) by A30, XBOOLE_0:def 3;

          hence {i, j, n, s} c= ( dom Lm) by A33, A35, A37, ENUMSET1:def 2;

          

          thus (Lm . j) = (La . j) by A1, A3, A4, A29, A34, Th3

          .= 1 by A3, A1, A10, A15, A11, A4, Th3;

          

          thus (Lm . n) = (La . n) by A4, A1, A29, A36, A3, Th3

          .= n0 by A3, A1, A4, A10, A16, A12, Th3;

          take I1 = (I + 1), S1 = (S * (I + 1));

          

           A38: (La . i) = Ad by A1, NOMIN_2: 10

          .= I1 by A14, A2, A18, A10, A11, A15, A9, A24, A21, Th4;

          hence (Lm . i) = I1 by A1, A29, A3, A4, A32, Th3;

          

           A39: s in ( dom La) by A10, A17, A31, XBOOLE_0:def 3;

          

           A40: (La . s) = (d1 . s) by A3, A1, A10, A4, A17, Th3;

          

          thus (Lm . s) = (mlt . La) by A1, A29, NOMIN_2: 10

          .= S1 by A32, A2, A19, A39, A22, A27, A38, A40, Th5;

          thus S1 = (I1 ! ) by A20, NEWTON: 15;

        end;

        hence (inv . (B . d)) = TRUE by A8, A25, A26, A28, Def19;

      end;

      hence thesis by NOMIN_3: 28;

    end;

    ::$Canceled

    theorem :: NOMIN_5:9

    

     Th9: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & ((loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)) are_mutually_distinct implies <*( factorial_inv (A,loc,n0)), ( factorial_main_loop (A,loc)), ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( factorial_inv (A,loc,n0))))*> is SFHT of ( ND (V,A))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4);

      set D = ( ND (V,A));

      set inv = ( factorial_inv (A,loc,n0));

      set B = ( factorial_loop_body (A,loc));

      set E = ( Equality (A,i,n));

      set N = ( PP_inversion inv);

      assume V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & (i,j,n,s) are_mutually_distinct ;

      then

       A1: <*inv, B, inv*> is SFHT of D by Th7;

      ( PP_and (( PP_not E),inv)) ||= inv by NOMIN_3: 3;

      then

       A2: <*( PP_and (( PP_not E),inv)), B, inv*> is SFHT of D by A1, NOMIN_3: 15;

      

       A3: <*N, B, inv*> is SFHT of D by NOMIN_3: 19;

      ( PP_and (( PP_not E),N)) ||= N by NOMIN_3: 3;

      then <*( PP_and (( PP_not E),N)), B, inv*> is SFHT of D by A3, NOMIN_3: 15;

      hence thesis by A2, NOMIN_3: 26;

    end;

    theorem :: NOMIN_5:10

    

     Th10: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & ((loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)) are_mutually_distinct & (loc,val) are_compatible_wrt_4_locs implies <*( valid_factorial_input (V,A,val,n0)), ( factorial_main_part (A,loc,val)), ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( factorial_inv (A,loc,n0))))*> is SFHT of ( ND (V,A))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4);

      set i1 = (val . 1), j1 = (val . 2), n1 = (val . 3), s1 = (val . 4);

      set D = ( ND (V,A));

      set p = ( valid_factorial_input (V,A,val,n0));

      set f = ( factorial_var_init (A,loc,val));

      set g = ( factorial_main_loop (A,loc));

      set q = ( factorial_inv (A,loc,n0));

      set r = ( PP_and (( Equality (A,i,n)),( factorial_inv (A,loc,n0))));

      assume

       A1: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & (i,j,n,s) are_mutually_distinct & (loc,val) are_compatible_wrt_4_locs ;

      then

       A2: <*p, f, q*> is SFHT of D by Th6;

      

       A3: <*q, g, r*> is SFHT of D by A1, Th9;

       <*( PP_inversion q), g, r*> is SFHT of D by NOMIN_3: 19;

      hence thesis by A2, A3, NOMIN_3: 25;

    end;

    theorem :: NOMIN_5:11

    

     Th11: V is non empty & A is_without_nonatomicND_wrt V & (for T holds (loc /. 1) is_a_value_on T & (loc /. 3) is_a_value_on T) implies ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( factorial_inv (A,loc,n0)))) ||= ( SC_Psuperpos (( valid_factorial_output (A,z,n0)),( denaming (V,A,(loc /. 4))),z))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4);

      set D = ( ND (V,A));

      set inv = ( factorial_inv (A,loc,n0));

      set Di = ( denaming (V,A,i));

      set Dn = ( denaming (V,A,n));

      set Ds = ( denaming (V,A,s));

      set Dz = ( denaming (V,A,z));

      set ass = ( SC_assignment (Ds,z));

      set out = ( valid_factorial_output (A,z,n0));

      set p = ( SC_Psuperpos (out,Ds,z));

      set E = ( Equality (A,i,n));

      assume that

       A1: V is non empty & A is_without_nonatomicND_wrt V and

       A2: for T holds i is_a_value_on T & n is_a_value_on T;

      let d be Element of D such that

       A3: d in ( dom ( PP_and (E,inv))) and

       A4: (( PP_and (E,inv)) . d) = TRUE ;

      

       A5: ( dom p) = { d where d be TypeSCNominativeData of V, A : ( local_overlapping (V,A,d,(Ds . d),z)) in ( dom out) & d in ( dom Ds) } by NOMIN_2:def 11;

      

       A6: ( dom out) = { d where d be TypeSCNominativeData of V, A : d in ( dom Dz) } by Def17;

      

       A7: ( dom Ds) = { d where d be NonatomicND of V, A : s in ( dom d) } by NOMIN_1:def 18;

      

       A8: ( dom Dz) = { d where d be NonatomicND of V, A : z in ( dom d) } by NOMIN_1:def 18;

      

       A9: d in ( dom E) by A3, A4, PARTPR_1: 23;

      

       A10: d in ( dom inv) by A3, A4, PARTPR_1: 23;

      

       A11: ( dom E) = (( dom Di) /\ ( dom Dn)) by A2, NOMIN_4: 11;

      then

       A12: d in ( dom Di) by A9, XBOOLE_0:def 4;

      (inv . d) = TRUE by A3, A4, PARTPR_1: 23;

      then factorial_inv_pred (A,loc,n0,d) by A10, Def19;

      then

      consider d1 be NonatomicND of V, A such that

       A13: d = d1 and

       A14: {i, j, n, s} c= ( dom d1) and (d1 . j) = 1 and

       A15: (d1 . n) = n0 and

       A16: ex I,S be Nat st I = (d1 . i) & S = (d1 . s) & S = (I ! );

      

       A17: i in {i, j, n, s} by ENUMSET1:def 2;

      

       A18: n in {i, j, n, s} by ENUMSET1:def 2;

      

       A19: s in {i, j, n, s} by ENUMSET1:def 2;

      reconsider dd = d as TypeSCNominativeData of V, A by NOMIN_1: 39;

      set L = ( local_overlapping (V,A,dd,(Ds . dd),z));

      

       A20: dd in ( dom Ds) by A7, A13, A14, A19;

      then (Ds . d1) in D by A13, PARTFUN1: 4;

      then

       A21: ex d2 be TypeSCNominativeData of V, A st (Ds . d1) = d2;

      then

       A22: L in ( dom Dz) by A1, A13, NOMIN_4: 6;

      then

       A23: L in ( dom out) by A6;

      hence

       A24: d in ( dom p) by A5, A20;

       valid_factorial_output_pred (A,z,n0,L)

      proof

        consider I,S be Nat such that

         A25: I = (d1 . i) and

         A26: S = (d1 . s) and

         A27: S = (I ! ) by A16;

        

         A28: ex d be NonatomicND of V, A st L = d & z in ( dom d) by A8, A22;

        then

        reconsider dlo = L as NonatomicND of V, A;

        take dlo;

        thus L = dlo;

        thus z in ( dom dlo) by A28;

        

         A29: i is_a_value_on dd by A2;

        

         A30: n is_a_value_on dd by A2;

        

         A31: ( dom <:Di, Dn:>) = (( dom Di) /\ ( dom Dn)) by FUNCT_3:def 7;

        d in ( dom <:Di, Dn:>) by A9, A11, FUNCT_3:def 7;

        then

         A32: (E . d) = (( Equality A) . ( <:Di, Dn:> . d)) by FUNCT_1: 13;

        

         A33: d in ( dom Dn) by A9, A11, XBOOLE_0:def 4;

        

         A34: ( <:Di, Dn:> . d) = [(Di . d), (Dn . d)] by A9, A11, A31, FUNCT_3:def 7;

        

         A35: (Di . d) = ( denaming (i,d1)) by A13, A12, NOMIN_1:def 18

        .= (d1 . i) by A14, A17, NOMIN_1:def 12;

        

         A36: (Dn . d) = ( denaming (n,d1)) by A13, A33, NOMIN_1:def 18

        .= (d1 . n) by A14, A18, NOMIN_1:def 12;

        

         A37: (Ds . d) = ( denaming (s,d1)) by A20, A13, NOMIN_1:def 18

        .= (d1 . s) by A14, A19, NOMIN_1:def 12;

        (( Equality A) . ((Di . d),(Dn . d))) <> FALSE by A3, A4, A32, A34, PARTPR_1: 23;

        then (Di . d) = (Dn . d) by A29, A30, NOMIN_4:def 9;

        hence (dlo . z) = (n0 ! ) by A1, A13, A15, A21, A25, A26, A27, A35, A36, A37, NOMIN_2: 10;

      end;

      

      hence TRUE = (out . L) by A23, Def17

      .= (p . d) by A24, NOMIN_2: 35;

    end;

    theorem :: NOMIN_5:12

    

     Th12: V is non empty & A is_without_nonatomicND_wrt V & (for T holds (loc /. 1) is_a_value_on T & (loc /. 3) is_a_value_on T) implies <*( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( factorial_inv (A,loc,n0)))), ( SC_assignment (( denaming (V,A,(loc /. 4))),z)), ( valid_factorial_output (A,z,n0))*> is SFHT of ( ND (V,A))

    proof

      set s = (loc /. 4);

       <*( SC_Psuperpos (( valid_factorial_output (A,z,n0)),( denaming (V,A,s)),z)), ( SC_assignment (( denaming (V,A,s)),z)), ( valid_factorial_output (A,z,n0))*> is SFHT of ( ND (V,A)) by NOMIN_3: 29;

      hence thesis by Th11, NOMIN_3: 15;

    end;

    theorem :: NOMIN_5:13

    

     Th13: (for T holds (loc /. 1) is_a_value_on T & (loc /. 3) is_a_value_on T) implies <*( PP_inversion ( PP_and (( Equality (A,(loc /. 1),(loc /. 3))),( factorial_inv (A,loc,n0))))), ( SC_assignment (( denaming (V,A,(loc /. 4))),z)), ( valid_factorial_output (A,z,n0))*> is SFHT of ( ND (V,A))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4);

      set D = ( ND (V,A));

      set inv = ( factorial_inv (A,loc,n0));

      set O = ( valid_factorial_output (A,z,n0));

      set Di = ( denaming (V,A,i));

      set Dn = ( denaming (V,A,n));

      set Ds = ( denaming (V,A,s));

      set g = ( SC_assignment (Ds,z));

      set E = ( Equality (A,i,n));

      set q = ( PP_and (E,inv));

      set N = ( PP_inversion q);

      assume

       A1: for T holds i is_a_value_on T & n is_a_value_on T;

      now

        let d be TypeSCNominativeData of V, A such that

         A2: d in ( dom N) and (N . d) = TRUE and d in ( dom g) and (g . d) in ( dom O);

        

         A3: ( dom q) = { d where d be Element of D : d in ( dom E) & (E . d) = FALSE or d in ( dom inv) & (inv . d) = FALSE or d in ( dom E) & (E . d) = TRUE & d in ( dom inv) & (inv . d) = TRUE } by PARTPR_1: 16;

        

         A4: ( dom Di) = { d where d be NonatomicND of V, A : i in ( dom d) } by NOMIN_1:def 18;

        

         A5: ( dom Dn) = { d where d be NonatomicND of V, A : n in ( dom d) } by NOMIN_1:def 18;

        

         A6: ( dom E) = (( dom Di) /\ ( dom Dn)) by A1, NOMIN_4: 11;

        

         A7: not d in ( dom q) by A2, PARTPR_2: 9;

        ( dom E) c= ( dom q) by PARTPR_2: 3;

        then not d in ( dom E) by A2, PARTPR_2: 9;

        then

         A8: not d in ( dom Di) or not d in ( dom Dn) by A6, XBOOLE_0:def 4;

        ( dom inv) = D by Def19;

        then

         A9: d in ( dom inv);

        then (inv . d) <> FALSE by A3, A7;

        then factorial_inv_pred (A,loc,n0,d) by A9, Def19;

        then

        consider d1 be NonatomicND of V, A such that

         A10: d = d1 and

         A11: {i, j, n, s} c= ( dom d1) and (d1 . (loc /. 2)) = 1 & (d1 . (loc /. 3)) = n0 & ex I,S be Nat st I = (d1 . (loc /. 1)) & S = (d1 . (loc /. 4)) & S = (I ! );

        i in {i, j, n, s} & n in {i, j, n, s} by ENUMSET1:def 2;

        hence (O . (g . d)) = TRUE by A4, A5, A8, A10, A11;

      end;

      hence thesis by NOMIN_3: 28;

    end;

    ::$Notion-Name

    theorem :: NOMIN_5:14

    V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & ((loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)) are_mutually_distinct & (loc,val) are_compatible_wrt_4_locs & (for T holds (loc /. 1) is_a_value_on T & (loc /. 3) is_a_value_on T) implies <*( valid_factorial_input (V,A,val,n0)), ( factorial_program (A,loc,val,z)), ( valid_factorial_output (A,z,n0))*> is SFHT of ( ND (V,A))

    proof

      set i = (loc /. 1), j = (loc /. 2), n = (loc /. 3), s = (loc /. 4);

      set i1 = (val . 1), j1 = (val . 2), n1 = (val . 3), s1 = (val . 4);

      set D = ( ND (V,A));

      set p = ( valid_factorial_input (V,A,val,n0));

      set f = ( factorial_main_part (A,loc,val));

      set g = ( SC_assignment (( denaming (V,A,s)),z));

      set q = ( valid_factorial_output (A,z,n0));

      set inv = ( factorial_inv (A,loc,n0));

      set E = ( Equality (A,i,n));

      assume that

       A1: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V and

       A2: (i,j,n,s) are_mutually_distinct and

       A3: (loc,val) are_compatible_wrt_4_locs and

       A4: for T holds i is_a_value_on T & n is_a_value_on T;

      

       A5: <*p, f, ( PP_and (E,inv))*> is SFHT of D by A1, A3, A2, Th10;

      

       A6: <*( PP_and (E,inv)), g, q*> is SFHT of D by A1, A4, Th12;

       <*( PP_inversion ( PP_and (E,inv))), g, q*> is SFHT of D by A4, Th13;

      hence thesis by A5, A6, NOMIN_3: 25;

    end;