nomin_6.miz



    begin

    definition

      let D be set;

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

      :: NOMIN_6:def1

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

      coherence ;

    end

    reserve D for non empty set;

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

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

    ::$Notion-Name

    theorem :: NOMIN_6:1

    

     Th1: <*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 implies <*p, ( PP_composition (f1,f2,f3,f4,f5)), u*> 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: <*t, f5, u*> is SFHT of D and

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

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

       A8: <*( PP_inversion w), f4, t*> is SFHT of D and

       A9: <*( PP_inversion t), f5, u*> is SFHT of D;

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

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

      then <*p, ( PP_composition (( PP_composition (f1,f2,f3)),f4)), t*> is SFHT of D by A4, A8, NOMIN_3: 25;

      hence thesis by A5, A9, NOMIN_3: 25;

    end;

    reserve d,v,v1 for object;

    reserve V,A for set;

    reserve i,j,b,n,s,z for Element of V;

    reserve i1,j1,b1,n1,s1 for object;

    reserve d1,Li,Lj,Lb,Ln,Ls for NonatomicND of V, A;

    reserve Di,Dj,Db,Dn,Ds for SCBinominativeFunction of V, A;

    theorem :: NOMIN_6:2

    

     Th2: V is non 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 implies (Ls . n) = (Ln . n)

    proof

      assume that

       A1: V is non empty and

       A2: A is_without_nonatomicND_wrt V and

       A3: 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)) and

       A4: j1 in ( dom d1) and

       A5: b1 in ( dom d1) and

       A6: n1 in ( dom d1) and

       A7: s1 in ( dom d1) and

       A8: d1 in ( dom Di) and

       A9: s <> n;

      

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

      

       A11: ( dom Db) = { d where d be NonatomicND of V, A : b1 in ( dom d) } by A3, NOMIN_1:def 18;

      

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

      

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

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

      then

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

      j1 in ( dom Li) by A4, A14, XBOOLE_0:def 3;

      then Li in ( dom Dj) by A10;

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

      then

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

      b1 in ( dom Li) by A5, A14, XBOOLE_0:def 3;

      then b1 in ( dom Lj) by A15, XBOOLE_0:def 3;

      then Lj in ( dom Db) by A11;

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

      then

       A16: ( dom Lb) = ( {b} \/ ( dom Lj)) by A1, A2, A3, NOMIN_4: 4;

      n1 in ( dom Li) by A6, A14, XBOOLE_0:def 3;

      then n1 in ( dom Lj) by A15, XBOOLE_0:def 3;

      then n1 in ( dom Lb) by A16, XBOOLE_0:def 3;

      then Lb in ( dom Dn) by A12;

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

      then

       A17: ( dom Ln) = ( {n} \/ ( dom Lb)) by A1, A2, A3, NOMIN_4: 4;

      s1 in ( dom Li) by A7, A14, XBOOLE_0:def 3;

      then s1 in ( dom Lj) by A15, XBOOLE_0:def 3;

      then s1 in ( dom Lb) by A16, XBOOLE_0:def 3;

      then s1 in ( dom Ln) by A17, XBOOLE_0:def 3;

      then

       A18: Ln in ( dom Ds) by A13;

      n in {n} by TARSKI:def 1;

      then

       A19: n in ( dom Ln) by A17, XBOOLE_0:def 3;

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

      hence (Ls . n) = (Ln . n) by A1, A2, A9, A19, A3, NOMIN_5: 3;

    end;

    theorem :: NOMIN_6:3

    

     Th3: V is non 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 implies (Ls . i) = (Ln . i)

    proof

      assume that

       A1: V is non empty and

       A2: A is_without_nonatomicND_wrt V and

       A3: 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)) and

       A4: j1 in ( dom d1) and

       A5: b1 in ( dom d1) and

       A6: n1 in ( dom d1) and

       A7: s1 in ( dom d1) and

       A8: d1 in ( dom Di) and

       A9: s <> i;

      

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

      

       A11: ( dom Db) = { d where d be NonatomicND of V, A : b1 in ( dom d) } by A3, NOMIN_1:def 18;

      

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

      

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

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

      then

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

      j1 in ( dom Li) by A4, A14, XBOOLE_0:def 3;

      then Li in ( dom Dj) by A10;

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

      then

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

      b1 in ( dom Li) by A5, A14, XBOOLE_0:def 3;

      then b1 in ( dom Lj) by A15, XBOOLE_0:def 3;

      then Lj in ( dom Db) by A11;

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

      then

       A16: ( dom Lb) = ( {b} \/ ( dom Lj)) by A1, A2, A3, NOMIN_4: 4;

      n1 in ( dom Li) by A6, A14, XBOOLE_0:def 3;

      then n1 in ( dom Lj) by A15, XBOOLE_0:def 3;

      then n1 in ( dom Lb) by A16, XBOOLE_0:def 3;

      then Lb in ( dom Dn) by A12;

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

      then

       A17: ( dom Ln) = ( {n} \/ ( dom Lb)) by A1, A2, A3, NOMIN_4: 4;

      s1 in ( dom Li) by A7, A14, XBOOLE_0:def 3;

      then s1 in ( dom Lj) by A15, XBOOLE_0:def 3;

      then s1 in ( dom Lb) by A16, XBOOLE_0:def 3;

      then s1 in ( dom Ln) by A17, XBOOLE_0:def 3;

      then

       A18: Ln in ( dom Ds) by A13;

      i in {i} by TARSKI:def 1;

      then i in ( dom Li) by A14, XBOOLE_0:def 3;

      then i in ( dom Lj) by A15, XBOOLE_0:def 3;

      then i in ( dom Lb) by A16, XBOOLE_0:def 3;

      then

       A19: i in ( dom Ln) by A17, XBOOLE_0:def 3;

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

      hence (Ls . i) = (Ln . i) by A1, A2, A9, A19, A3, NOMIN_5: 3;

    end;

    reserve f for SCBinominativeFunction of V, A;

    reserve T for TypeSCNominativeData of V, A;

    reserve loc for V -valued Function;

    reserve val for Function;

    definition

      let V, A, loc;

      :: NOMIN_6:def2

      func power_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 /. 5),(loc /. 3))),(loc /. 5)))));

      coherence ;

    end

    definition

      let V, A, loc;

      :: NOMIN_6:def3

      func power_main_loop (A,loc) -> SCBinominativeFunction of V, A equals ( PP_while (( PP_not ( Equality (A,(loc /. 1),(loc /. 4)))),( power_loop_body (A,loc))));

      coherence ;

    end

    definition

      let V, A, loc, val;

      :: NOMIN_6:def4

      func power_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))),( SC_assignment (( denaming (V,A,(val . 5))),(loc /. 5)))));

      coherence ;

    end

    definition

      let V, A, loc, val;

      :: NOMIN_6:def5

      func power_main_part (A,loc,val) -> SCBinominativeFunction of V, A equals ( PP_composition (( power_var_init (A,loc,val)),( power_main_loop (A,loc))));

      coherence ;

    end

    definition

      let V, A, loc, val, z;

      :: NOMIN_6:def6

      func power_program (A,loc,val,z) -> SCBinominativeFunction of V, A equals ( PP_composition (( power_main_part (A,loc,val)),( SC_assignment (( denaming (V,A,(loc /. 5))),z))));

      coherence ;

    end

    reserve n0 for Nat;

    reserve b0 for Complex;

    definition

      let V, A, val, b0, n0, d;

      :: NOMIN_6:def7

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

    end

    definition

      let V, A, val, b0, n0;

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

      :: NOMIN_6:def8

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

      : Def8: ( dom it ) = ( ND (V,A)) & for d be 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

      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, b0, n0;

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

      coherence by Def8;

    end

    definition

      let V, A, z, b0, n0, d;

      :: NOMIN_6:def9

      pred valid_power_output_pred A,z,b0,n0,d means ex d1 be NonatomicND of V, A st d = d1 & z in ( dom d1) & (d1 . z) = (b0 |^ n0);

    end

    definition

      let V, A, z, b0, n0;

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

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

      :: NOMIN_6:def10

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

      : Def10: ( 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_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

      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, b0, n0, d;

      :: NOMIN_6:def11

      pred power_inv_pred A,loc,b0,n0,d means ex d1 be 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 be Complex, I be Nat st I = (d1 . (loc /. 1)) & S = (d1 . (loc /. 5)) & S = (b0 |^ I);

    end

    definition

      let V, A, loc, b0, n0;

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

      :: NOMIN_6:def12

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

      : Def12: ( dom it ) = ( ND (V,A)) & for d be 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

      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, b0, n0;

      cluster ( power_inv (A,loc,b0,n0)) -> total;

      coherence by Def12;

    end

    definition

      let V, loc, val;

      :: NOMIN_6:def13

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

    end

    theorem :: NOMIN_6:4

    

     Th4: V is non 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 implies <*( 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

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

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

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

      set I = ( valid_power_input (V,A,val,b0,n0));

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

      set inv = ( power_inv (A,loc,b0,n0));

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

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

      set Db = ( denaming (V,A,b1));

      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 asb = ( SC_assignment (Db,b));

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

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

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

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

      set R1 = ( SC_Psuperpos (S1,Db,b));

      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,b,n,s) are_mutually_distinct and

       A4: (loc,val) are_compatible_wrt_5_locs ;

      

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

      

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

      

       A7: <*R1, asb, S1*> is SFHT of D by NOMIN_3: 29;

      

       A8: <*S1, asn, T1*> is SFHT of D by NOMIN_3: 29;

      

       A9: <*T1, ass, inv*> 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_power_input_pred (V,A,val,b0,n0,d) by Def8;

        then

        consider d1 be NonatomicND of V, A such that

         A10: d = d1 and

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

         A12: (d1 . i1) = 0 and

         A13: (d1 . j1) = 1 and

         A14: (d1 . b1) = b0 and

         A15: (d1 . n1) = n0 and

         A16: (d1 . s1) = 1;

        

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

        

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

        

         A19: b1 in {i1, j1, b1, n1, s1} by ENUMSET1:def 3;

        

         A20: n1 in {i1, j1, b1, n1, s1} by ENUMSET1:def 3;

        

         A21: s1 in {i1, j1, b1, n1, s1} by ENUMSET1:def 3;

        

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

        

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

        

         A25: ( dom Db) = { d where d be NonatomicND of V, A : b1 in ( dom d) } by NOMIN_1:def 18;

        

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

        

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

        

         A28: ( 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;

        

         A29: ( 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;

        

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

        

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

        

         A32: ( dom T1) = { 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 Lb = ( local_overlapping (V,A,Lj,(Db . Lj),b)) as NonatomicND of V, A by NOMIN_2: 9;

        reconsider Ln = ( local_overlapping (V,A,Lb,(Dn . Lb),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;

        

         A33: d1 in ( dom Di) by A11, A17, A23;

        then

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

        then

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

        ( dom inv) = D by Def12;

        then

         A36: Ls in ( dom inv);

        

         A37: j1 in ( dom Li) by A11, A18, A35, XBOOLE_0:def 3;

        then

         A38: Li in ( dom Dj) by A24;

        then

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

        then

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

        

         A41: b1 in ( dom Li) by A11, A19, A35, XBOOLE_0:def 3;

        then

         A42: b1 in ( dom Lj) by A40, XBOOLE_0:def 3;

        then

         A43: Lj in ( dom Db) by A25;

        then

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

        then

         A45: ( dom Lb) = ( {b} \/ ( dom Lj)) by A1, A2, NOMIN_4: 4;

        

         A46: n1 in ( dom Li) by A11, A20, A35, XBOOLE_0:def 3;

        then

         A47: n1 in ( dom Lj) by A40, XBOOLE_0:def 3;

        then

         A48: n1 in ( dom Lb) by A45, XBOOLE_0:def 3;

        then

         A49: Lb in ( dom Dn) by A26;

        then

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

        then

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

        

         A52: s1 in ( dom Li) by A11, A21, A35, XBOOLE_0:def 3;

        then

         A53: s1 in ( dom Lj) by A40, XBOOLE_0:def 3;

        then

         A54: s1 in ( dom Lb) by A45, XBOOLE_0:def 3;

        then

         A55: s1 in ( dom Ln) by A51, XBOOLE_0:def 3;

        then

         A56: Ln in ( dom Ds) by A27;

        then

         A57: Ln in ( dom T1) by A32, A36;

        then

         A58: Lb in ( dom S1) by A31, A49;

        then

         A59: Lj in ( dom R1) by A30, A43;

        then

         A60: Li in ( dom Q1) by A29, A38;

        hence

         A61: d in ( dom P1) by A10, A28, A33;

        

         A62: power_inv_pred (A,loc,b0,n0,Ls)

        proof

          take Ls;

          thus Ls = Ls;

          

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

          then

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

          i in {i} by TARSKI:def 1;

          then

           A65: i in ( dom Li) by A35, XBOOLE_0:def 3;

          then

           A66: i in ( dom Lj) by A40, XBOOLE_0:def 3;

          then

           A67: i in ( dom Lb) by A45, XBOOLE_0:def 3;

          then i in ( dom Ln) by A51, XBOOLE_0:def 3;

          then

           A68: i in ( dom Ls) by A64, XBOOLE_0:def 3;

          j in {j} by TARSKI:def 1;

          then

           A69: j in ( dom Lj) by A40, XBOOLE_0:def 3;

          then

           A70: j in ( dom Lb) by A45, XBOOLE_0:def 3;

          then

           A71: j in ( dom Ln) by A51, XBOOLE_0:def 3;

          then

           A72: j in ( dom Ls) by A64, XBOOLE_0:def 3;

          b in {b} by TARSKI:def 1;

          then

           A73: b in ( dom Lb) by A45, XBOOLE_0:def 3;

          then

           A74: b in ( dom Ln) by A51, XBOOLE_0:def 3;

          then

           A75: b in ( dom Ls) by A64, XBOOLE_0:def 3;

          n in {n} by TARSKI:def 1;

          then n in ( dom Ln) by A51, XBOOLE_0:def 3;

          then

           A76: n in ( dom Ls) by A64, XBOOLE_0:def 3;

          s in {s} by TARSKI:def 1;

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

          hence {i, j, b, n, s} c= ( dom Ls) by A68, A72, A75, A76, ENUMSET1:def 3;

          

          thus (Ls . j) = (Ln . j) by A1, A2, A3, A63, A71, NOMIN_5: 3

          .= (Lb . j) by A1, A2, A3, A50, A70, NOMIN_5: 3

          .= (Lj . j) by A1, A2, A3, A44, A69, NOMIN_5: 3

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

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

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

          .= 1 by A1, A2, A11, A4, A18, A13, A34, NOMIN_5: 3;

          

          thus (Ls . b) = (Ln . b) by A1, A2, A3, A63, A74, NOMIN_5: 3

          .= (Lb . b) by A1, A2, A3, A50, A73, NOMIN_5: 3

          .= (Db . Lj) by A1, A44, NOMIN_2: 10

          .= ( denaming (b1,Lj)) by A43, NOMIN_1:def 18

          .= (Lj . b1) by A42, NOMIN_1:def 12

          .= (Li . b1) by A1, A2, A4, A39, A41, NOMIN_5: 3

          .= b0 by A1, A2, A11, A19, A14, A34, A4, NOMIN_5: 3;

          

          thus (Ls . n) = (Ln . n) by A1, A2, A3, A11, A18, A19, A20, A21, A33, Th2

          .= (Dn . Lb) by A1, A50, NOMIN_2: 10

          .= ( denaming (n1,Lb)) by A49, NOMIN_1:def 18

          .= (Lb . n1) by A48, NOMIN_1:def 12

          .= (Lj . n1) by A1, A2, A4, A44, A47, NOMIN_5: 3

          .= (Li . n1) by A1, A2, A4, A39, A46, NOMIN_5: 3

          .= n0 by A1, A2, A11, A20, A15, A4, A34, NOMIN_5: 3;

          

           A78: (Ln . s1) = (Lb . s1) by A1, A2, A4, A50, A54, NOMIN_5: 3

          .= (Lj . s1) by A1, A2, A4, A44, A53, NOMIN_5: 3

          .= (Li . s1) by A1, A2, A39, A4, A52, NOMIN_5: 3

          .= 1 by A1, A2, A11, A21, A16, A34, A4, NOMIN_5: 3;

          take 1, 0 ;

          

          thus (Ls . i) = (Ln . i) by A1, A2, A11, A3, A18, A19, A20, A21, A33, Th3

          .= (Lb . i) by A1, A2, A50, A3, A67, NOMIN_5: 3

          .= (Lj . i) by A1, A2, A66, A3, A44, NOMIN_5: 3

          .= (Li . i) by A1, A2, A39, A3, A65, NOMIN_5: 3

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

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

          .= 0 by A11, A12, A17, NOMIN_1:def 12;

          

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

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

          .= 1 by A78, A55, NOMIN_1:def 12;

          thus 1 = (b0 |^ 0 ) by NEWTON: 4;

        end;

        

        thus (P1 . d) = (Q1 . Li) by A10, A61, NOMIN_2: 35

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

        .= (S1 . Lb) by A59, NOMIN_2: 35

        .= (T1 . Ln) by A58, NOMIN_2: 35

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

        .= TRUE by A36, A62, Def12;

      end;

      then

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

      

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

      

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

      

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

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

      hence thesis by A79, A6, A7, A8, A9, A80, A81, A82, Th1;

    end;

    theorem :: NOMIN_6:5

    

     Th5: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & ((loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)) are_mutually_distinct implies <*( power_inv (A,loc,b0,n0)), ( power_loop_body (A,loc)), ( power_inv (A,loc,b0,n0))*> is SFHT of ( ND (V,A))

    proof

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

      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,b,n,s) are_mutually_distinct ;

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

      set inv = ( power_inv (A,loc,b0,n0));

      set L = ( power_loop_body (A,loc));

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

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

      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 Db = ( denaming (V,A,b));

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

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

         power_inv_pred (A,loc,b0,n0,d) by A5, A6, Def12;

        then

        consider d1 be NonatomicND of V, A such that

         A9: d = d1 and

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

         A11: (d1 . j) = 1 and

         A12: (d1 . b) = b0 and

         A13: (d1 . n) = n0 and

         A14: ex S be Complex, I be Nat st I = (d1 . i) & S = (d1 . s) & S = (b0 |^ I);

        

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

        

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

        

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

        

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

        

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

        consider S be Complex, I be Nat such that

         A20: I = (d1 . i) and

         A22: S = (d1 . s) and

         A23: S = (b0 |^ I) by A14;

        

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

        

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

        

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

        then

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

        then

        reconsider Ad = (add . d1) as TypeSCNominativeData of V, A by A24, 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;

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

        then

         A28: (L . d) = (g . (f . d)) by A7, FUNCT_1: 12;

        

         A29: (f . d) = La by A9, A27, NOMIN_2:def 7;

        then

         A30: La in ( dom g) by A7, A26, FUNCT_1: 11;

        

         A31: (g . La) = Lm by A30, NOMIN_2:def 7;

         power_inv_pred (A,loc,b0,n0,Lm)

        proof

          take Lm;

          thus Lm = Lm;

          

           A32: (mlt . La) is TypeSCNominativeData of V, A by A25, A30, PARTFUN1: 4, NOMIN_1: 39;

          

           A33: ( dom Lm) = (( dom La) \/ {s}) by A3, A1, A25, A30, A31, NOMIN_4: 5;

          

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

          i in {i} by TARSKI:def 1;

          then

           A35: i in ( dom La) by A34, XBOOLE_0:def 3;

          then

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

          

           A37: j in ( dom La) by A10, A16, A34, XBOOLE_0:def 3;

          then

           A38: j in ( dom Lm) by A33, XBOOLE_0:def 3;

          

           A39: b in ( dom La) by A17, A10, A34, XBOOLE_0:def 3;

          then

           A40: b in ( dom Lm) by A33, XBOOLE_0:def 3;

          

           A41: n in ( dom La) by A10, A18, A34, XBOOLE_0:def 3;

          then

           A42: n in ( dom Lm) by A33, XBOOLE_0:def 3;

          s in {s} by TARSKI:def 1;

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

          hence {i, j, b, n, s} c= ( dom Lm) by A36, A38, A40, A42, ENUMSET1:def 3;

          

          thus (Lm . j) = (La . j) by A1, A32, A3, A4, A37, NOMIN_5: 3

          .= 1 by A3, A1, A10, A16, A11, A4, NOMIN_5: 3;

          

          thus (Lm . b) = (La . b) by A1, A4, A32, A39, A3, NOMIN_5: 3

          .= b0 by A3, A1, A10, A4, A17, A12, NOMIN_5: 3;

          

          thus (Lm . n) = (La . n) by A4, A1, A32, A41, A3, NOMIN_5: 3

          .= n0 by A10, A3, A1, A4, A18, A13, NOMIN_5: 3;

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

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

          .= I1 by A15, A2, A10, A20, A11, A16, A9, A27, A24, NOMIN_5: 4;

          hence (Lm . i) = I1 by A1, A32, A3, A4, A35, NOMIN_5: 3;

          

           A43: s in ( dom La) by A10, A19, A34, XBOOLE_0:def 3;

          

           A44: (La . s) = (d1 . s) by A3, A1, A10, A4, A19, NOMIN_5: 3;

          

           A45: (La . b) = (d1 . b) by A3, A1, A10, A4, A17, NOMIN_5: 3;

          

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

          .= S1 by A39, A12, A45, A2, A22, A43, A25, A30, A44, NOMIN_5: 5;

          thus S1 = (b0 |^ I1) by A23, NEWTON: 6;

        end;

        hence (inv . (L . d)) = TRUE by A8, A28, A29, A31, Def12;

      end;

      hence thesis by NOMIN_3: 28;

    end;

    ::$Canceled

    theorem :: NOMIN_6:7

    

     Th7: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & ((loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)) are_mutually_distinct implies <*( 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

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

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

      set inv = ( power_inv (A,loc,b0,n0));

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

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

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

      then

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

      ( 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: <*( PP_inversion inv), B, inv*> is SFHT of D by NOMIN_3: 19;

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

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

      hence thesis by A2, NOMIN_3: 26;

    end;

    theorem :: NOMIN_6:8

    

     Th8: V is non 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 implies <*( 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

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

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

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

      set p = ( valid_power_input (V,A,val,b0,n0));

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

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

      set q = ( power_inv (A,loc,b0,n0));

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

      assume

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

      then

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

      

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

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

      hence thesis by A2, A3, NOMIN_3: 25;

    end;

    theorem :: NOMIN_6:9

    

     Th9: V is non empty & A is_without_nonatomicND_wrt V & (for T holds (loc /. 1) is_a_value_on T) & (for T holds (loc /. 4) is_a_value_on T) implies ( 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

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

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

      set inv = ( power_inv (A,loc,b0,n0));

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

      set Db = ( denaming (V,A,b));

      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_power_output (A,z,b0,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 and

       A3: for T holds n is_a_value_on T;

      let d be Element of D such that

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

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

      

       A6: ( 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;

      

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

      

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

      

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

      

       A10: d in ( dom E) by A4, A5, PARTPR_1: 23;

      

       A11: d in ( dom inv) by A4, A5, PARTPR_1: 23;

      

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

      then

       A13: d in ( dom Di) by A10, XBOOLE_0:def 4;

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

      then power_inv_pred (A,loc,b0,n0,d) by A11, Def12;

      then

      consider d1 be NonatomicND of V, A such that

       A14: d = d1 and

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

       A16: (d1 . n) = n0 and (d1 . b) = b0 and

       A18: ex S be Complex, I be Nat st I = (d1 . i) & S = (d1 . s) & S = (b0 |^ I);

      

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

      

       A20: n in {i, j, b, n, s} by ENUMSET1:def 3;

      

       A21: s in {i, j, b, n, s} by ENUMSET1:def 3;

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

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

      

       A22: dd in ( dom Ds) by A15, A8, A14, A21;

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

      then

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

      then

       A24: L in ( dom Dz) by A1, A14, NOMIN_4: 6;

      then

       A25: L in ( dom out) by A7;

      hence

       A26: d in ( dom p) by A6, A22;

       valid_power_output_pred (A,z,b0,n0,L)

      proof

        consider S be Complex, I be Nat such that

         A27: I = (d1 . i) and

         A29: S = (d1 . s) and

         A30: S = (b0 |^ I) by A18;

        

         A31: ex d be NonatomicND of V, A st L = d & z in ( dom d) by A9, A24;

        then

        reconsider dlo = L as NonatomicND of V, A;

        take dlo;

        thus L = dlo;

        thus z in ( dom dlo) by A31;

        

         A32: i is_a_value_on dd by A2;

        

         A33: n is_a_value_on dd by A3;

        

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

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

        then

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

        

         A36: d in ( dom Dn) by A10, A12, XBOOLE_0:def 4;

        

         A37: ( <:Di, Dn:> . d) = [(Di . d), (Dn . d)] by A10, A12, A34, FUNCT_3:def 7;

        

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

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

        

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

        .= (d1 . n) by A15, A20, NOMIN_1:def 12;

        

         A40: (Ds . d) = ( denaming (s,d1)) by A22, A14, NOMIN_1:def 18

        .= (d1 . s) by A15, A21, NOMIN_1:def 12;

        (( Equality A) . ((Di . d),(Dn . d))) <> FALSE by A4, A5, A35, A37, PARTPR_1: 23;

        then (Di . d) = (Dn . d) by A32, A33, NOMIN_4:def 9;

        hence (dlo . z) = (b0 |^ n0) by A1, A14, A16, A23, A27, A29, A30, A38, A39, A40, NOMIN_2: 10;

      end;

      

      hence TRUE = (out . L) by A25, Def10

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

    end;

    theorem :: NOMIN_6:10

    

     Th10: V is non empty & A is_without_nonatomicND_wrt V & (for T holds (loc /. 1) is_a_value_on T) & (for T holds (loc /. 4) is_a_value_on T) implies <*( 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

      set s = (loc /. 5);

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

      hence thesis by Th9, NOMIN_3: 15;

    end;

    theorem :: NOMIN_6:11

    

     Th11: (for T holds (loc /. 1) is_a_value_on T) & (for T holds (loc /. 4) is_a_value_on T) implies <*( 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

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

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

      set inv = ( power_inv (A,loc,b0,n0));

      set O = ( valid_power_output (A,z,b0,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 P = ( PP_inversion q);

      assume

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

      now

        let d be TypeSCNominativeData of V, A such that

         A2: d in ( dom P) and (P . 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 Def12;

        then

         A9: d in ( dom inv);

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

        then power_inv_pred (A,loc,b0,n0,d) by A9, Def12;

        then

        consider d1 be NonatomicND of V, A such that

         A10: d = d1 & {i, j, b, n, s} c= ( dom d1) and (d1 . (loc /. 2)) = 1 & (d1 . (loc /. 3)) = b0 & (d1 . (loc /. 4)) = n0 & ex S be Complex, I be Nat st I = (d1 . (loc /. 1)) & S = (d1 . (loc /. 5)) & S = (b0 |^ I);

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

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

      end;

      hence thesis by NOMIN_3: 28;

    end;

    ::$Notion-Name

    theorem :: NOMIN_6:12

    V is non 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 holds (loc /. 1) is_a_value_on T) & (for T holds (loc /. 4) is_a_value_on T) implies <*( 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

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

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

      set p = ( valid_power_input (V,A,val,b0,n0));

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

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

      set q = ( valid_power_output (A,z,b0,n0));

      set inv = ( power_inv (A,loc,b0,n0));

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

      assume that

       A1: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & (i,j,b,n,s) are_mutually_distinct and

       A2: (loc,val) are_compatible_wrt_5_locs and

       A3: (for T holds i is_a_value_on T) & (for T holds n is_a_value_on T);

      

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

      

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

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

      hence thesis by A4, A5, NOMIN_3: 25;

    end;