partpr_2.miz



    begin

    reserve x for object;

    reserve n for Nat;

    registration

      let X,Y be set;

      cluster -> X -defined for Element of ( PFuncs (X,Y));

      coherence ;

      cluster -> Y -valued for Element of ( PFuncs (X,Y));

      coherence ;

    end

    theorem :: PARTPR_2:1

    

     Th1: for X,Y,Z,T be set holds for x,y,z be object holds for f be Function of [:X, Y, Z:], T st x in X & y in Y & z in Z & T <> {} holds (f . (x,y,z)) in T

    proof

      let X,Y,Z,T be set;

      let x,y,z be object;

      let f be Function of [:X, Y, Z:], T;

      assume x in X & y in Y & z in Z;

      then [x, y, z] in [:X, Y, Z:] by MCART_1: 69;

      hence thesis by FUNCT_2: 5;

    end;

    registration

      cluster non empty non with_non-empty_elements for set;

      existence

      proof

        take { {} };

        thus { {} } is non empty;

        thus {} in { {} } by TARSKI:def 1;

      end;

    end

    definition

      let A,B,C be set;

      :: PARTPR_2:def1

      func PFcompos (A,B,C) -> Function of [:( PFuncs (A,B)), ( PFuncs (B,C)):], ( PFuncs (A,C)) means

      : D1: for f be PartFunc of A, B holds for g be PartFunc of B, C holds (it . (f,g)) = (g * f);

      existence

      proof

        defpred P[ Function, Function, object] means $3 = ($2 * $1);

        

         A1: for f be Element of ( PFuncs (A,B)) holds for g be Element of ( PFuncs (B,C)) holds ex y be Element of ( PFuncs (A,C)) st P[f, g, y]

        proof

          let f be Element of ( PFuncs (A,B));

          let g be Element of ( PFuncs (B,C));

          reconsider h = (g * f) as Element of ( PFuncs (A,C)) by PARTFUN1: 45;

          take h;

          thus thesis;

        end;

        consider F be Function of [:( PFuncs (A,B)), ( PFuncs (B,C)):], ( PFuncs (A,C)) such that

         A2: for x be Element of ( PFuncs (A,B)) holds for y be Element of ( PFuncs (B,C)) holds P[x, y, (F . (x,y))] from BINOP_1:sch 3( A1);

        take F;

        let f be PartFunc of A, B;

        let g be PartFunc of B, C;

        f in ( PFuncs (A,B)) & g in ( PFuncs (B,C)) by PARTFUN1: 45;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let F,G be Function of [:( PFuncs (A,B)), ( PFuncs (B,C)):], ( PFuncs (A,C)) such that

         A3: for f be PartFunc of A, B holds for g be PartFunc of B, C holds (F . (f,g)) = (g * f) and

         A4: for f be PartFunc of A, B holds for g be PartFunc of B, C holds (G . (f,g)) = (g * f);

        let x,y be set;

        assume x in ( PFuncs (A,B));

        then

        reconsider f = x as PartFunc of A, B by PARTFUN1: 46;

        assume y in ( PFuncs (B,C));

        then

        reconsider g = y as PartFunc of B, C by PARTFUN1: 46;

        

        thus (F . (x,y)) = (g * f) by A3

        .= (G . (x,y)) by A4;

      end;

    end

    reserve D for non empty set;

    reserve p,q for PartialPredicate of D;

    theorem :: PARTPR_2:2

    q is total implies ( dom p) c= ( dom ( PP_or (p,q)))

    proof

      assume

       A1: q is total;

      set a = ( PP_or (p,q));

      let x;

      assume

       A2: x in ( dom p);

      

       A3: ( dom a) = { d where d be Element of D : d in ( dom p) & (p . d) = TRUE or d in ( dom q) & (q . d) = TRUE or d in ( dom p) & (p . d) = FALSE & d in ( dom q) & (q . d) = FALSE } by PARTPR_1:def 4;

      per cases by A2, PARTPR_1: 3;

        suppose

         A4: (p . x) = FALSE ;

        (q . x) = TRUE or (q . x) = FALSE by A1, A2, PARTPR_1: 3;

        hence thesis by A1, A2, A3, A4;

      end;

        suppose (p . x) = TRUE ;

        hence thesis by A2, A3;

      end;

    end;

    theorem :: PARTPR_2:3

    q is total implies ( dom p) c= ( dom ( PP_and (p,q)))

    proof

      assume

       A1: q is total;

      set a = ( PP_and (p,q));

      let x;

      assume

       A2: x in ( dom p);

      

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

      per cases by A2, PARTPR_1: 3;

        suppose

         A4: (p . x) = TRUE ;

        (q . x) = TRUE or (q . x) = FALSE by A1, A2, PARTPR_1: 3;

        hence thesis by A1, A2, A3, A4;

      end;

        suppose (p . x) = FALSE ;

        hence thesis by A2, A3;

      end;

    end;

    theorem :: PARTPR_2:4

    q is total implies ( dom p) c= ( dom ( PP_imp (p,q)))

    proof

      assume

       A1: q is total;

      set a = ( PP_imp (p,q));

      let x;

      assume

       A2: x in ( dom p);

      

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

      per cases by A2, PARTPR_1: 3;

        suppose

         A4: (p . x) = TRUE ;

        (q . x) = TRUE or (q . x) = FALSE by A1, A2, PARTPR_1: 3;

        hence thesis by A1, A2, A3, A4;

      end;

        suppose (p . x) = FALSE ;

        hence thesis by A2, A3;

      end;

    end;

    begin

    reserve D for set;

    definition

      let D;

      :: PARTPR_2:def2

      func FPrg (D) -> set equals ( PFuncs (D,D));

      coherence ;

    end

    registration

      let D;

      cluster ( FPrg D) -> non empty functional;

      coherence ;

    end

    definition

      let D;

      mode BinominativeFunction of D is PartFunc of D, D;

    end

    theorem :: PARTPR_2:5

    for D be non empty set, f be BinominativeFunction of D holds ( id ( field f)) is BinominativeFunction of D

    proof

      let D be non empty set, f be BinominativeFunction of D;

      ( dom f) c= D & ( rng f) c= D by RELAT_1:def 19;

      then

      reconsider X = ( field f) as Subset of D by XBOOLE_1: 8;

      ( id X) is BinominativeFunction of D;

      hence thesis;

    end;

    reserve p,q for PartialPredicate of D;

    reserve f,g for BinominativeFunction of D;

    registration

      let D, p;

      let F be Function of ( Pr D), ( Pr D);

      cluster (F . p) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D;

      let F be Function of ( Pr D), ( Pr D);

      let p be Element of ( Pr D);

      cluster (F . p) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D, p, q;

      let F be Function of [:( Pr D), ( Pr D):], ( Pr D);

      cluster (F . (p,q)) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D;

      let F be Function of [:( Pr D), ( Pr D):], ( Pr D);

      let p,q be Element of ( Pr D);

      cluster (F . (p,q)) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D;

      let F be Function of [:( Pr D), ( Pr D):], ( Pr D);

      let x be Element of [:( Pr D), ( Pr D):];

      cluster (F . x) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D, f;

      let F be Function of ( FPrg D), ( FPrg D);

      cluster (F . f) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D, p, f, g;

      let F be Function of [:( Pr D), ( FPrg D), ( FPrg D):], ( FPrg D);

      cluster (F . (p,f,g)) -> Function-like Relation-like;

      coherence ;

      cluster (F . [p, f, g]) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D, p, q, f;

      let F be Function of [:( Pr D), ( FPrg D), ( Pr D):], ( Pr D);

      cluster (F . (p,f,q)) -> Function-like Relation-like;

      coherence ;

      cluster (F . [p, f, q]) -> Function-like Relation-like;

      coherence ;

    end

    ::$Notion-Name

    notation

      let D be set;

      synonym PPid (D) for id D;

    end

    definition

      let D be set;

      :: original: PPid

      redefine

      func PPid (D) -> BinominativeFunction of D ;

      coherence

      proof

        ( id D) is BinominativeFunction of D;

        hence thesis;

      end;

    end

    ::$Notion-Name

    definition

      let D be non empty set, d be Element of D;

      :: PARTPR_2:def3

      func PP_id (d) -> Element of D equals (( PPid D) . d);

      coherence ;

    end

    ::$Notion-Name

    definition

      let D;

      :: PARTPR_2:def4

      func PPcomposition (D) -> Function of [:( FPrg D), ( FPrg D):], ( FPrg D) equals ( PFcompos (D,D,D));

      coherence ;

    end

    ::$Notion-Name

    definition

      let D, f, g;

      :: PARTPR_2:def5

      func PP_composition (f,g) -> BinominativeFunction of D equals (( PPcomposition D) . (f,g));

      coherence

      proof

        f in ( FPrg D) & g in ( FPrg D) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, BINOP_1: 17;

      end;

    end

    ::$Notion-Name

    definition

      let D;

      :: PARTPR_2:def6

      func PPprediction (D) -> Function of [:( FPrg D), ( Pr D):], ( Pr D) equals ( PFcompos (D,D, BOOLEAN ));

      coherence ;

    end

    ::$Notion-Name

    definition

      let D, f, p;

      :: PARTPR_2:def7

      func PP_prediction (f,p) -> PartialPredicate of D equals (( PPprediction D) . (f,p));

      coherence

      proof

        f in ( FPrg D) & p in ( Pr D) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, BINOP_1: 17;

      end;

    end

    registration

      let D;

      let F be Function of [:( Pr D), ( FPrg D), ( FPrg D):], ( FPrg D);

      let p be PartialPredicate of D;

      let f,g be BinominativeFunction of D;

      cluster (F . (p,f,g)) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: PARTPR_2:6

    x in ( dom ( PP_prediction (f,p))) implies x in ( dom (p * f)) & (((p * f) . x) = TRUE or ((p * f) . x) = FALSE )

    proof

      assume x in ( dom ( PP_prediction (f,p)));

      then x in ( dom (p * f)) by D1;

      hence thesis by PARTPR_1: 3;

    end;

    scheme :: PARTPR_2:sch1

    PredToNomPredEx { D() -> set , Dom() -> set , P[ object] } :

ex p be PartialPredicate of D() st ( dom p) = Dom() & (for d be object st d in ( dom p) holds (P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE ))

      provided

       A1: Dom() c= D();

      defpred Q[ object, object] means (P[$1] & $2 = TRUE ) or ( not P[$1] & $2 = FALSE );

      

       A2: for d be object st d in Dom() holds ex z be object st z in BOOLEAN & Q[d, z]

      proof

        let d be object such that d in Dom();

        per cases ;

          suppose

           A3: Q[d, TRUE ];

          take TRUE ;

          thus thesis by A3;

        end;

          suppose

           A4: Q[d, FALSE ];

          take FALSE ;

          thus thesis by A4;

        end;

      end;

      consider p be Function of Dom(), BOOLEAN such that

       A5: for d be object st d in Dom() holds Q[d, (p . d)] from FUNCT_2:sch 1( A2);

      

       A6: p in ( PFuncs (Dom(), BOOLEAN )) by PARTFUN1: 45;

      ( PFuncs (Dom(), BOOLEAN )) c= ( PFuncs (D(), BOOLEAN )) by A1, PARTFUN1: 50;

      then

      reconsider p as PartialPredicate of D() by A6, PARTFUN1: 46;

      take p;

      ( dom p) = Dom() by FUNCT_2:def 1;

      hence thesis by A5;

    end;

    scheme :: PARTPR_2:sch2

    PredToNomPredUnique { D() -> set , Dom() -> set , P[ object] } :

for p,q be PartialPredicate of D() st (( dom p) = Dom() & (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) = Dom() & (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;

      let p,q be PartialPredicate of D() such that

       A1: (( dom p) = Dom() & (for d be object st d in ( dom p) holds (P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE ))) and

       A2: (( dom q) = Dom() & (for d be object st d in ( dom q) holds (P[d] implies (q . d) = TRUE ) & ( not P[d] implies (q . d) = FALSE )));

      for d be object st d in ( dom p) holds (p . d) = (q . d)

      proof

        let d be object such that

         A3: d in ( dom p);

        (p . d) = (q . d)

        proof

          per cases ;

            suppose

             A4: P[d];

            

            hence (p . d) = TRUE by A1, A3

            .= (q . d) by A1, A2, A3, A4;

          end;

            suppose

             A5: not P[d];

            

            hence (p . d) = FALSE by A1, A3

            .= (q . d) by A1, A2, A3, A5;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    ::$Notion-Name

    definition

      let D;

      defpred P[ object] means $1 = {} ;

      :: PARTPR_2:def8

      func PPisEmpty (D) -> PartialPredicate of D means ( dom it ) = D & for d be object st d in ( dom it ) holds (d = {} implies (it . d) = TRUE ) & (d <> {} implies (it . d) = FALSE );

      existence

      proof

        

         A1: D c= D;

        consider p be PartialPredicate of D such that

         A2: ( dom p) = D and

         A3: for d be object st d in ( dom p) holds ( P[d] implies (p . d) = TRUE ) & ( not P[d] implies (p . d) = FALSE ) from PredToNomPredEx( A1);

        take p;

        thus thesis by A2, A3;

      end;

      uniqueness

      proof

        for p,q be PartialPredicate of D 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 PredToNomPredUnique;

        hence thesis;

      end;

    end

    ::$Notion-Name

    definition

      let D be non with_non-empty_elements set;

      :: PARTPR_2:def9

      func PPEmpty (D) -> BinominativeFunction of D equals (D --> {} );

      coherence

      proof

        set f = (D --> {} );

        

         A1: ( dom f) = D;

        

         A2: ( rng f) = { {} } by FUNCOP_1: 8;

        ( rng f) c= D

        proof

          let x;

          assume x in ( rng f);

          then x = {} by A2, TARSKI:def 1;

          hence thesis by SETFAM_1:def 8;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    ::$Notion-Name

    definition

      let D;

      :: PARTPR_2:def10

      func PPBottomFunc (D) -> BinominativeFunction of D equals {} ;

      coherence by RELSET_1: 12;

    end

    reserve D for non empty set;

    reserve p,q for PartialPredicate of D;

    reserve f,g,h for BinominativeFunction of D;

    ::$Notion-Name

    definition

      let D;

      defpred D1[ object, Function, Function] means $1 in ( dom $2) & ($2 . $1) = TRUE & $1 in ( dom $3);

      defpred D2[ object, Function, Function] means $1 in ( dom $2) & ($2 . $1) = FALSE & $1 in ( dom $3);

      deffunc D( Function, Function, Function) = { d where d be Element of D : D1[d, $1, $2] or D2[d, $1, $3] };

      :: PARTPR_2:def11

      func PPIF (D) -> Function of [:( Pr D), ( FPrg D), ( FPrg D):], ( FPrg D) means

      : Def13: for p be PartialPredicate of D holds for f,g be BinominativeFunction of D holds ( dom (it . (p,f,g))) = { d where d be Element of D : d in ( dom p) & (p . d) = TRUE & d in ( dom f) or d in ( dom p) & (p . d) = FALSE & d in ( dom g) } & for d be object holds (d in ( dom p) & (p . d) = TRUE & d in ( dom f) implies ((it . (p,f,g)) . d) = (f . d)) & (d in ( dom p) & (p . d) = FALSE & d in ( dom g) implies ((it . (p,f,g)) . d) = (g . d));

      existence

      proof

        defpred P[ object, object, object, object] means for p be PartialPredicate of D holds for f,g be BinominativeFunction of D st p = $1 & f = $2 & g = $3 holds for h be Function st h = $4 holds ( dom h) = D(p,f,g) & for d be object holds ( D1[d, p, f] implies (h . d) = (f . d)) & ( D2[d, p, g] implies (h . d) = (g . d));

        

         A1: for x1 be Element of ( Pr D) holds for x2,x3 be Element of ( FPrg D) holds ex y be Element of ( FPrg D) st P[x1, x2, x3, y]

        proof

          let x1 be Element of ( Pr D);

          let x2,x3 be Element of ( FPrg D);

          reconsider X1 = x1 as PartFunc of D, BOOLEAN by PARTFUN1: 46;

          reconsider X2 = x2, X3 = x3 as PartFunc of D, D by PARTFUN1: 46;

          defpred Q[ object, object] means for d be object st d = $1 holds ( D1[d, X1, X2] implies $2 = (X2 . d)) & ( D2[d, X1, X3] implies $2 = (X3 . d));

          

           A2: for a be object st a in D(X1,X2,X3) holds ex b be object st b in D & Q[a, b]

          proof

            let a be object;

            assume a in D(X1,X2,X3);

            then

            consider d be Element of D such that

             A3: d = a and

             A4: D1[d, X1, X2] or D2[d, X1, X3];

            per cases by A4;

              suppose

               A5: D1[d, X1, X2];

              take (X2 . d);

              thus thesis by A3, A5, PARTFUN1: 4;

            end;

              suppose

               A6: D2[d, X1, X3];

              take (X3 . d);

              thus thesis by A3, A6, PARTFUN1: 4;

            end;

          end;

          consider H be Function such that

           A7: ( dom H) = D(X1,X2,X3) and

           A8: ( rng H) c= D and

           A9: for x be object st x in D(X1,X2,X3) holds Q[x, (H . x)] from FUNCT_1:sch 6( A2);

           D(X1,X2,X3) c= D

          proof

            let x;

            assume x in D(X1,X2,X3);

            then ex d be Element of D st d = x & ( D1[d, X1, X2] or D2[d, X1, X3]);

            hence thesis;

          end;

          then H is PartFunc of D, D by A7, A8, RELSET_1: 4;

          then

          reconsider H as Element of ( FPrg D) by PARTFUN1: 45;

          take H;

          let p be PartialPredicate of D;

          let f,g be BinominativeFunction of D such that

           A10: x1 = p & x2 = f & x3 = g;

          let h be Function such that

           A11: h = H;

          thus ( dom h) = D(p,f,g) by A7, A10, A11;

          let d be object;

          hereby

            assume

             A12: D1[d, p, f];

            then d in ( dom p);

            then d in D(X1,X2,X3) by A10, A12;

            hence (h . d) = (f . d) by A9, A10, A11, A12;

          end;

          assume

           A13: D2[d, p, g];

          then d in ( dom p);

          then d in D(X1,X2,X3) by A10, A13;

          hence (h . d) = (g . d) by A9, A10, A11, A13;

        end;

        consider F be Function of [:( Pr D), ( FPrg D), ( FPrg D):], ( FPrg D) such that

         A14: for x be Element of ( Pr D) holds for y,z be Element of ( FPrg D) holds P[x, y, z, (F . [x, y, z])] from MULTOP_1:sch 1( A1);

        take F;

        let p be PartialPredicate of D;

        let f,g be BinominativeFunction of D;

        p in ( Pr D) & f in ( FPrg D) & g in ( FPrg D) by PARTFUN1: 45;

        hence thesis by A14;

      end;

      uniqueness

      proof

        let F,G be Function of [:( Pr D), ( FPrg D), ( FPrg D):], ( FPrg D) such that

         A15: for p be PartialPredicate of D holds for f,g be BinominativeFunction of D holds ( dom (F . (p,f,g))) = D(p,f,g) & for d be object holds ( D1[d, p, f] implies ((F . (p,f,g)) . d) = (f . d)) & ( D2[d, p, g] implies ((F . (p,f,g)) . d) = (g . d)) and

         A16: for p be PartialPredicate of D holds for f,g be BinominativeFunction of D holds ( dom (G . (p,f,g))) = D(p,f,g) & for d be object holds ( D1[d, p, f] implies ((G . (p,f,g)) . d) = (f . d)) & ( D2[d, p, g] implies ((G . (p,f,g)) . d) = (g . d));

        now

          let x1,x2,x3 be object such that

           A17: x1 in ( Pr D) and

           A18: x2 in ( FPrg D) and

           A19: x3 in ( FPrg D);

          reconsider p1 = x1 as PartialPredicate of D by A17, PARTFUN1: 46;

          reconsider f2 = x2, f3 = x3 as BinominativeFunction of D by A18, A19, PARTFUN1: 46;

          thus (F . [x1, x2, x3]) = (G . [x1, x2, x3])

          proof

            

             A20: (G . [x1, x2, x3]) = (G . (x1,x2,x3));

            (F . [x1, x2, x3]) = (F . (x1,x2,x3));

            then

             A21: ( dom (F . [x1, x2, x3])) = D(p1,f2,f3) by A15;

            hence ( dom (F . [x1, x2, x3])) = ( dom (G . [x1, x2, x3])) by A16, A20;

            let a be object;

            assume a in ( dom (F . [x1, x2, x3]));

            then

            consider d be Element of D such that

             A22: a = d and

             A23: D1[d, p1, f2] or D2[d, p1, f3] by A21;

            per cases by A23;

              suppose

               A24: D1[d, p1, f2];

              

              thus ((F . [x1, x2, x3]) . a) = ((F . (p1,f2,f3)) . a)

              .= (f2 . d) by A15, A22, A24

              .= ((G . (p1,f2,f3)) . a) by A16, A22, A24

              .= ((G . [x1, x2, x3]) . a);

            end;

              suppose

               A25: D2[d, p1, f3];

              

              thus ((F . [x1, x2, x3]) . a) = ((F . (p1,f2,f3)) . a)

              .= (f3 . d) by A15, A22, A25

              .= ((G . (p1,f2,f3)) . a) by A16, A22, A25

              .= ((G . [x1, x2, x3]) . a);

            end;

          end;

        end;

        hence thesis by MULTOP_1: 1;

      end;

    end

    ::$Notion-Name

    definition

      let D, p, f, g;

      :: PARTPR_2:def12

      func PP_IF (p,f,g) -> BinominativeFunction of D equals (( PPIF D) . (p,f,g));

      coherence

      proof

        p in ( Pr D) & f in ( FPrg D) & g in ( FPrg D) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, Th1;

      end;

    end

    theorem :: PARTPR_2:7

    x in ( dom ( PP_IF (p,f,g))) implies x in ( dom p) & (p . x) = TRUE & x in ( dom f) or x in ( dom p) & (p . x) = FALSE & x in ( dom g)

    proof

      assume

       A1: x in ( dom ( PP_IF (p,f,g)));

      ( dom ( PP_IF (p,f,g))) = { d where d be Element of D : d in ( dom p) & (p . d) = TRUE & d in ( dom f) or d in ( dom p) & (p . d) = FALSE & d in ( dom g) } by Def13;

      then ex d1 be Element of D st d1 = x & (d1 in ( dom p) & (p . d1) = TRUE & d1 in ( dom f) or d1 in ( dom p) & (p . d1) = FALSE & d1 in ( dom g)) by A1;

      hence thesis;

    end;

    ::$Notion-Name

    definition

      let D;

      defpred D1[ object, Function, Function, Function] means $1 in ( dom $2) & ($2 . $1) = FALSE or $1 in ( dom ($4 * $3)) & (($4 * $3) . $1) = TRUE ;

      defpred D2[ object, Function, Function, Function] means $1 in ( dom $2) & ($2 . $1) = TRUE & $1 in ( dom ($4 * $3)) & (($4 * $3) . $1) = FALSE ;

      deffunc D( Function, Function, Function) = { d where d be Element of D : D1[d, $1, $2, $3] or D2[d, $1, $2, $3] };

      :: PARTPR_2:def13

      func PPFH (D) -> Function of [:( Pr D), ( FPrg D), ( Pr D):], ( Pr D) means

      : Def15: for p,q be PartialPredicate of D holds for f be BinominativeFunction of D holds ( dom (it . (p,f,q))) = { d where d be Element of D : d in ( dom p) & (p . d) = FALSE or d in ( dom (q * f)) & ((q * f) . d) = TRUE or d in ( dom p) & (p . d) = TRUE & d in ( dom (q * f)) & ((q * f) . d) = FALSE } & for d be object holds (d in ( dom p) & (p . d) = FALSE or d in ( dom (q * f)) & ((q * f) . d) = TRUE implies ((it . (p,f,q)) . d) = TRUE ) & (d in ( dom p) & (p . d) = TRUE & d in ( dom (q * f)) & ((q * f) . d) = FALSE implies ((it . (p,f,q)) . d) = FALSE );

      existence

      proof

        defpred P[ object, object, object, object] means for p,q be PartialPredicate of D holds for f be BinominativeFunction of D st p = $1 & f = $2 & q = $3 holds for h be Function st h = $4 holds ( dom h) = D(p,f,q) & for d be object holds ( D1[d, p, f, q] implies (h . d) = TRUE ) & ( D2[d, p, f, q] implies (h . d) = FALSE );

        

         A1: for x1 be Element of ( Pr D) holds for x2 be Element of ( FPrg D) holds for x3 be Element of ( Pr D) holds ex y be Element of ( Pr D) st P[x1, x2, x3, y]

        proof

          let x1 be Element of ( Pr D);

          let x2 be Element of ( FPrg D);

          let x3 be Element of ( Pr D);

          reconsider X1 = x1, X3 = x3 as PartFunc of D, BOOLEAN by PARTFUN1: 46;

          reconsider X2 = x2 as PartFunc of D, D by PARTFUN1: 46;

          defpred Q[ object, object] means for d be object st d = $1 holds ( D1[d, X1, X2, X3] implies $2 = TRUE ) & ( D2[d, X1, X2, X3] implies $2 = FALSE );

          

           A2: for a be object st a in D(X1,X2,X3) holds ex b be object st b in BOOLEAN & Q[a, b]

          proof

            let a be object;

            assume a in D(X1,X2,X3);

            then

            consider d be Element of D such that

             A3: d = a and

             A4: D1[d, X1, X2, X3] or D2[d, X1, X2, X3];

            per cases by A4;

              suppose

               A5: D1[d, X1, X2, X3];

              take TRUE ;

              thus thesis by A3, A5;

            end;

              suppose

               A6: D2[d, X1, X2, X3];

              take FALSE ;

              thus thesis by A3, A6;

            end;

          end;

          consider g be Function such that

           A7: ( dom g) = D(X1,X2,X3) and

           A8: ( rng g) c= BOOLEAN and

           A9: for x be object st x in D(X1,X2,X3) holds Q[x, (g . x)] from FUNCT_1:sch 6( A2);

           D(X1,X2,X3) c= D

          proof

            let x;

            assume x in D(X1,X2,X3);

            then ex d be Element of D st d = x & ( D1[d, X1, X2, X3] or D2[d, X1, X2, X3]);

            hence thesis;

          end;

          then g is PartFunc of D, BOOLEAN by A7, A8, RELSET_1: 4;

          then

          reconsider g as Element of ( Pr D) by PARTFUN1: 45;

          take g;

          let p,q be PartialPredicate of D;

          let f be BinominativeFunction of D such that

           A10: x1 = p & x2 = f & x3 = q;

          let h be Function such that

           A11: h = g;

          thus ( dom h) = D(p,f,q) by A7, A10, A11;

          let d be object;

          hereby

            assume

             A12: D1[d, p, f, q];

            then d in ( dom p) or d in ( dom (q * f));

            then d in D(X1,X2,X3) by A10, A12;

            hence (h . d) = TRUE by A9, A10, A11, A12;

          end;

          assume

           A13: D2[d, p, f, q];

          then d in ( dom p);

          then d in D(X1,X2,X3) by A10, A13;

          hence (h . d) = FALSE by A9, A10, A11, A13;

        end;

        consider F be Function of [:( Pr D), ( FPrg D), ( Pr D):], ( Pr D) such that

         A14: for x be Element of ( Pr D) holds for y be Element of ( FPrg D) holds for z be Element of ( Pr D) holds P[x, y, z, (F . [x, y, z])] from MULTOP_1:sch 1( A1);

        take F;

        let p,q be PartialPredicate of D;

        let f be BinominativeFunction of D;

        p in ( Pr D) & f in ( FPrg D) & q in ( Pr D) by PARTFUN1: 45;

        hence thesis by A14;

      end;

      uniqueness

      proof

        let F,G be Function of [:( Pr D), ( FPrg D), ( Pr D):], ( Pr D) such that

         A15: for p,q be PartialPredicate of D holds for f be BinominativeFunction of D holds ( dom (F . (p,f,q))) = D(p,f,q) & for d be object holds ( D1[d, p, f, q] implies ((F . (p,f,q)) . d) = TRUE ) & ( D2[d, p, f, q] implies ((F . (p,f,q)) . d) = FALSE ) and

         A16: for p,q be PartialPredicate of D holds for f be BinominativeFunction of D holds ( dom (G . (p,f,q))) = D(p,f,q) & for d be object holds ( D1[d, p, f, q] implies ((G . (p,f,q)) . d) = TRUE ) & ( D2[d, p, f, q] implies ((G . (p,f,q)) . d) = FALSE );

        now

          let x1,x2,x3 be object such that

           A17: x1 in ( Pr D) and

           A18: x2 in ( FPrg D) and

           A19: x3 in ( Pr D);

          reconsider p1 = x1, p3 = x3 as PartialPredicate of D by A17, A19, PARTFUN1: 46;

          reconsider f2 = x2 as BinominativeFunction of D by A18, PARTFUN1: 46;

          thus (F . [x1, x2, x3]) = (G . [x1, x2, x3])

          proof

            

             A20: (G . [x1, x2, x3]) = (G . (x1,x2,x3));

            (F . [x1, x2, x3]) = (F . (x1,x2,x3));

            then

             A21: ( dom (F . [x1, x2, x3])) = D(p1,f2,p3) by A15;

            hence ( dom (F . [x1, x2, x3])) = ( dom (G . [x1, x2, x3])) by A16, A20;

            let a be object;

            assume a in ( dom (F . [x1, x2, x3]));

            then

            consider d be Element of D such that

             A22: a = d and

             A23: D1[d, p1, f2, p3] or D2[d, p1, f2, p3] by A21;

            per cases by A23;

              suppose

               A24: D1[d, p1, f2, p3];

              

              thus ((F . [x1, x2, x3]) . a) = ((F . (p1,f2,p3)) . a)

              .= TRUE by A15, A22, A24

              .= ((G . (p1,f2,p3)) . a) by A16, A22, A24

              .= ((G . [x1, x2, x3]) . a);

            end;

              suppose

               A25: D2[d, p1, f2, p3];

              

              thus ((F . [x1, x2, x3]) . a) = ((F . (p1,f2,p3)) . a)

              .= FALSE by A15, A22, A25

              .= ((G . (p1,f2,p3)) . a) by A16, A22, A25

              .= ((G . [x1, x2, x3]) . a);

            end;

          end;

        end;

        hence thesis by MULTOP_1: 1;

      end;

    end

    ::$Notion-Name

    definition

      let D, p, q, f;

      :: PARTPR_2:def14

      func PP_FH (p,f,q) -> PartialPredicate of D equals (( PPFH D) . (p,f,q));

      coherence

      proof

        p in ( Pr D) & f in ( FPrg D) & q in ( Pr D) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, Th1;

      end;

    end

    theorem :: PARTPR_2:8

    x in ( dom ( PP_FH (p,f,q))) implies x in ( dom p) & (p . x) = FALSE or x in ( dom (q * f)) & ((q * f) . x) = TRUE or x in ( dom p) & (p . x) = TRUE & x in ( dom (q * f)) & ((q * f) . x) = FALSE

    proof

      assume

       A1: x in ( dom ( PP_FH (p,f,q)));

      ( dom ( PP_FH (p,f,q))) = { d where d be Element of D : d in ( dom p) & (p . d) = FALSE or d in ( dom (q * f)) & ((q * f) . d) = TRUE or d in ( dom p) & (p . d) = TRUE & d in ( dom (q * f)) & ((q * f) . d) = FALSE } by Def15;

      then ex d1 be Element of D st d1 = x & (d1 in ( dom p) & (p . d1) = FALSE or d1 in ( dom (q * f)) & ((q * f) . d1) = TRUE or d1 in ( dom p) & (p . d1) = TRUE & d1 in ( dom (q * f)) & ((q * f) . d1) = FALSE ) by A1;

      hence thesis;

    end;

    ::$Notion-Name

    definition

      let D;

      defpred D1[ object, Function, Function, Nat] means (for i be Nat st i <= ($4 - 1) holds $1 in ( dom ($2 * ( iter ($3,i)))) & (($2 * ( iter ($3,i))) . $1) = TRUE ) & $1 in ( dom ($2 * ( iter ($3,$4)))) & (($2 * ( iter ($3,$4))) . $1) = FALSE ;

      deffunc D( Function, Function) = { d where d be Element of D : ex n st D1[d, $1, $2, n] };

      :: PARTPR_2:def15

      func PPwhile (D) -> Function of [:( Pr D), ( FPrg D):], ( FPrg D) means for p be PartialPredicate of D holds for f be BinominativeFunction of D holds ( dom (it . (p,f))) = { d where d be Element of D : ex n be Nat st (for i be Nat st i <= (n - 1) holds d in ( dom (p * ( iter (f,i)))) & ((p * ( iter (f,i))) . d) = TRUE ) & d in ( dom (p * ( iter (f,n)))) & ((p * ( iter (f,n))) . d) = FALSE } & for d be object st d in ( dom (it . (p,f))) holds ex n be Nat st (for i be Nat st i <= (n - 1) holds d in ( dom (p * ( iter (f,i)))) & ((p * ( iter (f,i))) . d) = TRUE ) & d in ( dom (p * ( iter (f,n)))) & ((p * ( iter (f,n))) . d) = FALSE & ((it . (p,f)) . d) = (( iter (f,n)) . d);

      existence

      proof

        defpred P[ object, object, object] means for p be PartialPredicate of D holds for f be BinominativeFunction of D st $1 = p & $2 = f holds for h be Function st h = $3 holds ( dom h) = D(p,f) & for d be object st d in ( dom h) holds ex n st D1[d, p, f, n] & (h . d) = (( iter (f,n)) . d);

        

         A1: for x1,x2 be object st x1 in ( Pr D) & x2 in ( FPrg D) holds ex y be object st y in ( FPrg D) & P[x1, x2, y]

        proof

          let x1,x2 be object;

          assume x1 in ( Pr D);

          then

          reconsider X1 = x1 as PartFunc of D, BOOLEAN by PARTFUN1: 46;

          assume x2 in ( FPrg D);

          then

          reconsider X2 = x2 as PartFunc of D, D by PARTFUN1: 46;

          defpred Q[ object, object] means for d be object st d = $1 holds ex n st D1[d, X1, X2, n] & $2 = (( iter (X2,n)) . d);

          

           A2: for a be object st a in D(X1,X2) holds ex b be object st b in D & Q[a, b]

          proof

            let a be object;

            assume a in D(X1,X2);

            then

            consider d be Element of D such that

             A3: d = a and

             A4: ex n st D1[d, X1, X2, n];

            consider n such that

             A5: D1[d, X1, X2, n] by A4;

            take (( iter (X2,n)) . d);

            

             A6: ( iter (X2,n)) is PartFunc of D, D by FUNCT_7: 86;

            ( dom (X1 * ( iter (X2,n)))) c= ( dom ( iter (X2,n))) by RELAT_1: 25;

            hence (( iter (X2,n)) . d) in D by A5, A6, PARTFUN1: 4;

            thus thesis by A3, A5;

          end;

          consider K be Function such that

           A7: ( dom K) = D(X1,X2) and

           A8: ( rng K) c= D and

           A9: for x be object st x in D(X1,X2) holds Q[x, (K . x)] from FUNCT_1:sch 6( A2);

          take K;

           D(X1,X2) c= D

          proof

            let x;

            assume x in D(X1,X2);

            then ex d be Element of D st d = x & ex n st D1[d, X1, X2, n];

            hence thesis;

          end;

          then K is PartFunc of D, D by A7, A8, RELSET_1: 4;

          hence K in ( FPrg D) by PARTFUN1: 45;

          thus thesis by A7, A9;

        end;

        consider F be Function of [:( Pr D), ( FPrg D):], ( FPrg D) such that

         A10: for x,y be object st x in ( Pr D) & y in ( FPrg D) holds P[x, y, (F . (x,y))] from BINOP_1:sch 1( A1);

        take F;

        let p be PartialPredicate of D;

        let f be BinominativeFunction of D;

        

         A11: p in ( Pr D) & f in ( FPrg D) by PARTFUN1: 45;

        hence ( dom (F . (p,f))) = D(p,f) by A10;

        let d be object;

        assume d in ( dom (F . (p,f)));

        then

        consider n be Nat such that

         A12: D1[d, p, f, n] & ((F . (p,f)) . d) = (( iter (f,n)) . d) by A10, A11;

        take n;

        thus thesis by A12;

      end;

      uniqueness

      proof

        let F,G be Function of [:( Pr D), ( FPrg D):], ( FPrg D) such that

         A13: for p be PartialPredicate of D holds for f be BinominativeFunction of D holds ( dom (F . (p,f))) = D(p,f) & for d be object st d in ( dom (F . (p,f))) holds ex n be Nat st (for i be Nat st i <= (n - 1) holds d in ( dom (p * ( iter (f,i)))) & ((p * ( iter (f,i))) . d) = TRUE ) & d in ( dom (p * ( iter (f,n)))) & ((p * ( iter (f,n))) . d) = FALSE & ((F . (p,f)) . d) = (( iter (f,n)) . d) and

         A14: for p be PartialPredicate of D holds for f be BinominativeFunction of D holds ( dom (G . (p,f))) = D(p,f) & for d be object st d in ( dom (G . (p,f))) holds ex n be Nat st (for i be Nat st i <= (n - 1) holds d in ( dom (p * ( iter (f,i)))) & ((p * ( iter (f,i))) . d) = TRUE ) & d in ( dom (p * ( iter (f,n)))) & ((p * ( iter (f,n))) . d) = FALSE & ((G . (p,f)) . d) = (( iter (f,n)) . d);

        let a,b be set;

        assume

         A15: a in ( Pr D);

        then

        reconsider p = a as PartialPredicate of D by PARTFUN1: 46;

        assume

         A16: b in ( FPrg D);

        then

        reconsider f = b as BinominativeFunction of D by PARTFUN1: 46;

        (F . (a,b)) in ( FPrg D) by A15, A16, BINOP_1: 17;

        then

         A17: ( dom (F . (a,b))) c= D by RELAT_1:def 18;

        

        thus

         A18: ( dom (F . (a,b))) = D(p,f) by A13

        .= ( dom (G . (a,b))) by A14;

        let z be object;

        assume

         A19: z in ( dom (F . (a,b)));

        then

        reconsider d = z as Element of D by A17;

        consider n be Nat such that

         A20: for i be Nat st i <= (n - 1) holds d in ( dom (p * ( iter (f,i)))) & ((p * ( iter (f,i))) . d) = TRUE and

         A21: d in ( dom (p * ( iter (f,n)))) & ((p * ( iter (f,n))) . d) = FALSE and

         A22: ((F . (p,f)) . d) = (( iter (f,n)) . d) by A13, A19;

        consider m be Nat such that

         A23: for i be Nat st i <= (m - 1) holds d in ( dom (p * ( iter (f,i)))) & ((p * ( iter (f,i))) . d) = TRUE and

         A24: d in ( dom (p * ( iter (f,m)))) & ((p * ( iter (f,m))) . d) = FALSE and

         A25: ((G . (p,f)) . d) = (( iter (f,m)) . d) by A14, A18, A19;

        m = n

        proof

          assume m <> n;

          per cases by XXREAL_0: 1;

            suppose m < n;

            then m <= (n - 1) by INT_1: 52;

            hence contradiction by A20, A24;

          end;

            suppose m > n;

            then n <= (m - 1) by INT_1: 52;

            hence contradiction by A21, A23;

          end;

        end;

        hence thesis by A22, A25;

      end;

    end

    ::$Notion-Name

    definition

      let D, p, f;

      :: PARTPR_2:def16

      func PP_while (p,f) -> BinominativeFunction of D equals (( PPwhile D) . (p,f));

      coherence

      proof

        p in ( Pr D) & f in ( FPrg D) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, BINOP_1: 17;

      end;

    end

    definition

      let D;

      defpred Dn[ object, Function] means $1 in ( dom $2);

      deffunc DM( Function) = { d where d be Element of D : not d in ( dom $1) };

      :: PARTPR_2:def17

      func PPinversion (D) -> Function of ( Pr D), ( Pr D) means

      : Def19: for p be PartialPredicate of D holds ( dom (it . p)) = { d where d be Element of D : not d in ( dom p) } & for d be Element of D holds not d in ( dom p) implies ((it . p) . d) = TRUE ;

      existence

      proof

        defpred P[ object, object] means for p be PartialPredicate of D st p = $1 holds for f be Function st f = $2 holds DM(p) = ( dom f) & for d be Element of D holds not Dn[d, p] implies (f . d) = TRUE ;

        

         A1: for x be object st x in ( Pr D) holds ex y be object st y in ( Pr D) & P[x, y]

        proof

          let x;

          assume x in ( Pr D);

          then

          reconsider X = x as PartFunc of D, BOOLEAN by PARTFUN1: 46;

          defpred Q[ object, object] means for d be Element of D st d = $1 holds not Dn[d, X] implies $2 = TRUE ;

          

           A2: DM(X) c= D

          proof

            let x;

            assume x in DM(X);

            then ex d be Element of D st x = d & not d in ( dom X);

            hence thesis;

          end;

          

           A3: for a be object st a in DM(X) holds ex b be object st b in BOOLEAN & Q[a, b]

          proof

            let a be object;

            assume a in DM(X);

            take TRUE ;

            thus thesis;

          end;

          consider g be Function such that

           A4: ( dom g) = DM(X) and

           A5: ( rng g) c= BOOLEAN and

           A6: for x be object st x in DM(X) holds Q[x, (g . x)] from FUNCT_1:sch 6( A3);

          take g;

          g is PartFunc of D, BOOLEAN by A2, A4, A5, RELSET_1: 4;

          hence g in ( Pr D) by PARTFUN1: 45;

          let p be PartialPredicate of D such that

           A7: p = x;

          let f be Function such that

           A8: f = g;

          thus DM(p) = ( dom f) by A4, A7, A8;

          let d be Element of D;

          assume

           A9: not Dn[d, p];

          then d in DM(X) by A7;

          hence (f . d) = TRUE by A6, A7, A8, A9;

        end;

        consider F be Function of ( Pr D), ( Pr D) such that

         A10: for x be object st x in ( Pr D) holds P[x, (F . x)] from FUNCT_2:sch 1( A1);

        take F;

        let p be PartialPredicate of D;

        p in ( Pr D) by PARTFUN1: 45;

        hence thesis by A10;

      end;

      uniqueness

      proof

        let f,g be Function of ( Pr D), ( Pr D) such that

         A11: for p be PartialPredicate of D holds ( dom (f . p)) = DM(p) & for d be Element of D holds not Dn[d, p] implies ((f . p) . d) = TRUE and

         A12: for p be PartialPredicate of D holds ( dom (g . p)) = DM(p) & for d be Element of D holds not Dn[d, p] implies ((g . p) . d) = TRUE ;

        let x be Element of ( Pr D);

        reconsider p = x as PartialPredicate of D by PARTFUN1: 46;

        

        thus ( dom (f . x)) = DM(p) by A11

        .= ( dom (g . x)) by A12;

        let a be object;

        assume a in ( dom (f . x));

        then a in DM(p) by A11;

        then

         A13: ex d be Element of D st a = d & not d in ( dom p);

        

        hence ((f . x) . a) = TRUE by A11

        .= ((g . x) . a) by A12, A13;

      end;

    end

    definition

      let D be non empty set;

      let p be PartialPredicate of D;

      :: PARTPR_2:def18

      func PP_inversion (p) -> PartialPredicate of D equals (( PPinversion D) . p);

      coherence

      proof

        p in ( Pr D) by PARTFUN1: 45;

        hence thesis by PARTFUN1: 46, FUNCT_2: 5;

      end;

    end

    theorem :: PARTPR_2:9

    for d be Element of D holds d in ( dom p) iff not d in ( dom ( PP_inversion p))

    proof

      let d be Element of D;

      

       A1: ( dom ( PP_inversion p)) = { d where d be Element of D : not d in ( dom p) } by Def19;

      thus d in ( dom p) implies not d in ( dom ( PP_inversion p))

      proof

        assume

         A2: d in ( dom p);

        assume d in ( dom ( PP_inversion p));

        then ex d1 be Element of D st d = d1 & not d1 in ( dom p) by A1;

        hence thesis by A2;

      end;

      thus thesis by A1;

    end;

    theorem :: PARTPR_2:10

    p is total implies ( dom ( PP_inversion p)) = {}

    proof

      set q = ( PP_inversion p);

      assume

       A1: ( dom p) = D;

      

       A2: ( dom q) = { d where d be Element of D : not d in ( dom p) } by Def19;

      thus ( dom q) c= {}

      proof

        let x;

        assume x in ( dom q);

        then ex d be Element of D st x = d & not d in ( dom p) by A2;

        hence thesis by A1;

      end;

      thus thesis by XBOOLE_1: 2;

    end;