:: by Taneli Huuskonen

::

:: Received April 30, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

definition

let D be non empty set ;

let P, Q be Subset of (D *);

{ (p ^ q) where p, q is FinSequence of D : ( p in P & q in Q ) } is Subset of (D *)

end;
let P, Q be Subset of (D *);

func ^ (D,P,Q) -> Subset of (D *) equals :: POLNOT_1:def 1

{ (p ^ q) where p, q is FinSequence of D : ( p in P & q in Q ) } ;

coherence { (p ^ q) where p, q is FinSequence of D : ( p in P & q in Q ) } ;

{ (p ^ q) where p, q is FinSequence of D : ( p in P & q in Q ) } is Subset of (D *)

proof end;

:: deftheorem defines ^ POLNOT_1:def 1 :

for D being non empty set

for P, Q being Subset of (D *) holds ^ (D,P,Q) = { (p ^ q) where p, q is FinSequence of D : ( p in P & q in Q ) } ;

for D being non empty set

for P, Q being Subset of (D *) holds ^ (D,P,Q) = { (p ^ q) where p, q is FinSequence of D : ( p in P & q in Q ) } ;

definition

let P, Q be FinSequence-membered set ;

ex b_{1} being FinSequence-membered set st

for a being object holds

( a in b_{1} iff ex p, q being FinSequence st

( a = p ^ q & p in P & q in Q ) )

for b_{1}, b_{2} being FinSequence-membered set st ( for a being object holds

( a in b_{1} iff ex p, q being FinSequence st

( a = p ^ q & p in P & q in Q ) ) ) & ( for a being object holds

( a in b_{2} iff ex p, q being FinSequence st

( a = p ^ q & p in P & q in Q ) ) ) holds

b_{1} = b_{2}

end;
func P ^ Q -> FinSequence-membered set means :Def2: :: POLNOT_1:def 2

for a being object holds

( a in it iff ex p, q being FinSequence st

( a = p ^ q & p in P & q in Q ) );

existence for a being object holds

( a in it iff ex p, q being FinSequence st

( a = p ^ q & p in P & q in Q ) );

ex b

for a being object holds

( a in b

( a = p ^ q & p in P & q in Q ) )

proof end;

uniqueness for b

( a in b

( a = p ^ q & p in P & q in Q ) ) ) & ( for a being object holds

( a in b

( a = p ^ q & p in P & q in Q ) ) ) holds

b

proof end;

:: deftheorem Def2 defines ^ POLNOT_1:def 2 :

for P, Q, b_{3} being FinSequence-membered set holds

( b_{3} = P ^ Q iff for a being object holds

( a in b_{3} iff ex p, q being FinSequence st

( a = p ^ q & p in P & q in Q ) ) );

for P, Q, b

( b

( a in b

( a = p ^ q & p in P & q in Q ) ) );

registration

let E be empty set ;

let P be FinSequence-membered set ;

coherence

E ^ P is empty

P ^ E is empty

end;
let P be FinSequence-membered set ;

coherence

E ^ P is empty

proof end;

coherence P ^ E is empty

proof end;

registration
end;

theorem TH1: :: POLNOT_1:1

for p, q, r, s being FinSequence st p ^ q = r ^ s holds

ex t being FinSequence st

( p ^ t = r or p = r ^ t )

ex t being FinSequence st

( p ^ t = r or p = r ^ t )

proof end;

definition

let P be FinSequence-membered set ;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st

( Q = b_{1} . n & b_{1} . (n + 1) = Q ^ P ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & b_{1} . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st

( Q = b_{1} . n & b_{1} . (n + 1) = Q ^ P ) ) & dom b_{2} = NAT & b_{2} . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st

( Q = b_{2} . n & b_{2} . (n + 1) = Q ^ P ) ) holds

b_{1} = b_{2}

end;
func P ^^ -> Function means :Def3: :: POLNOT_1:def 3

( dom it = NAT & it . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st

( Q = it . n & it . (n + 1) = Q ^ P ) ) );

existence ( dom it = NAT & it . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st

( Q = it . n & it . (n + 1) = Q ^ P ) ) );

ex b

( dom b

( Q = b

proof end;

uniqueness for b

( Q = b

( Q = b

b

proof end;

:: deftheorem Def3 defines ^^ POLNOT_1:def 3 :

for P being FinSequence-membered set

for b_{2} being Function holds

( b_{2} = P ^^ iff ( dom b_{2} = NAT & b_{2} . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st

( Q = b_{2} . n & b_{2} . (n + 1) = Q ^ P ) ) ) );

for P being FinSequence-membered set

for b

( b

( Q = b

definition

let P be FinSequence-membered set ;

let n be Nat;

coherence

(P ^^) . n is FinSequence-membered set

end;
let n be Nat;

coherence

(P ^^) . n is FinSequence-membered set

proof end;

:: deftheorem defines ^^ POLNOT_1:def 4 :

for P being FinSequence-membered set

for n being Nat holds P ^^ n = (P ^^) . n;

for P being FinSequence-membered set

for n being Nat holds P ^^ n = (P ^^) . n;

registration
end;

definition

let P be FinSequence-membered set ;

union { (P ^^ n) where n is Nat : verum } is non empty FinSequence-membered set

end;
func P * -> non empty FinSequence-membered set equals :: POLNOT_1:def 5

union { (P ^^ n) where n is Nat : verum } ;

coherence union { (P ^^ n) where n is Nat : verum } ;

union { (P ^^ n) where n is Nat : verum } is non empty FinSequence-membered set

proof end;

:: deftheorem defines * POLNOT_1:def 5 :

for P being FinSequence-membered set holds P * = union { (P ^^ n) where n is Nat : verum } ;

for P being FinSequence-membered set holds P * = union { (P ^^ n) where n is Nat : verum } ;

theorem Th6: :: POLNOT_1:5

for P being FinSequence-membered set

for a being object holds

( a in P * iff ex n being Nat st a in P ^^ n )

for a being object holds

( a in P * iff ex n being Nat st a in P ^^ n )

proof end;

theorem Th7: :: POLNOT_1:6

for P being FinSequence-membered set holds

( P ^^ 0 = {{}} & ( for n being Nat holds P ^^ (n + 1) = (P ^^ n) ^ P ) )

( P ^^ 0 = {{}} & ( for n being Nat holds P ^^ (n + 1) = (P ^^ n) ^ P ) )

proof end;

theorem Th12: :: POLNOT_1:11

for P being FinSequence-membered set

for p, q being FinSequence

for m, n being Nat st p in P ^^ m & q in P ^^ n holds

p ^ q in P ^^ (m + n)

for p, q being FinSequence

for m, n being Nat st p in P ^^ m & q in P ^^ n holds

p ^ q in P ^^ (m + n)

proof end;

theorem Th13: :: POLNOT_1:12

for P being FinSequence-membered set

for p, q being FinSequence st p in P * & q in P * holds

p ^ q in P *

for p, q being FinSequence st p in P * & q in P * holds

p ^ q in P *

proof end;

registration

let S be non empty FinSequence-membered set ;

let n be Nat;

coherence

( not S ^^ n is empty & S ^^ n is FinSequence-membered )

end;
let n be Nat;

coherence

( not S ^^ n is empty & S ^^ n is FinSequence-membered )

proof end;

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

let U be Subset of (P *);

ex b_{1} being Subset of (P *) st

for a being object holds

( a in b_{1} iff ( a in P * & ex p, q being FinSequence ex n being Nat st

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) )

for b_{1}, b_{2} being Subset of (P *) st ( for a being object holds

( a in b_{1} iff ( a in P * & ex p, q being FinSequence ex n being Nat st

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) ) & ( for a being object holds

( a in b_{2} iff ( a in P * & ex p, q being FinSequence ex n being Nat st

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) ) holds

b_{1} = b_{2}

end;
let A be Function of P,NAT;

let U be Subset of (P *);

func Polish-expression-layer (P,A,U) -> Subset of (P *) means :Def8: :: POLNOT_1:def 6

for a being object holds

( a in it iff ( a in P * & ex p, q being FinSequence ex n being Nat st

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) );

existence for a being object holds

( a in it iff ( a in P * & ex p, q being FinSequence ex n being Nat st

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) );

ex b

for a being object holds

( a in b

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) )

proof end;

uniqueness for b

( a in b

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) ) & ( for a being object holds

( a in b

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) ) holds

b

proof end;

:: deftheorem Def8 defines Polish-expression-layer POLNOT_1:def 6 :

for P being FinSequence-membered set

for A being Function of P,NAT

for U, b_{4} being Subset of (P *) holds

( b_{4} = Polish-expression-layer (P,A,U) iff for a being object holds

( a in b_{4} iff ( a in P * & ex p, q being FinSequence ex n being Nat st

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) );

for P being FinSequence-membered set

for A being Function of P,NAT

for U, b

( b

( a in b

( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) );

theorem Th20: :: POLNOT_1:18

for P being FinSequence-membered set

for A being Function of P,NAT

for U being Subset of (P *)

for n being Nat

for p, q being FinSequence st p in P & n = A . p & q in U ^^ n holds

p ^ q in Polish-expression-layer (P,A,U)

for A being Function of P,NAT

for U being Subset of (P *)

for n being Nat

for p, q being FinSequence st p in P & n = A . p & q in U ^^ n holds

p ^ q in Polish-expression-layer (P,A,U)

proof end;

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

ex b_{1} being Subset of (P *) st

for a being object holds

( a in b_{1} iff ( a in P & A . a = 0 ) )

for b_{1}, b_{2} being Subset of (P *) st ( for a being object holds

( a in b_{1} iff ( a in P & A . a = 0 ) ) ) & ( for a being object holds

( a in b_{2} iff ( a in P & A . a = 0 ) ) ) holds

b_{1} = b_{2}

{ t where t is Element of P * : ( t in P & A . t <> 0 ) } is Subset of P

end;
let A be Function of P,NAT;

func Polish-atoms (P,A) -> Subset of (P *) means :Def9: :: POLNOT_1:def 7

for a being object holds

( a in it iff ( a in P & A . a = 0 ) );

existence for a being object holds

( a in it iff ( a in P & A . a = 0 ) );

ex b

for a being object holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

func Polish-operations (P,A) -> Subset of P equals :: POLNOT_1:def 8

{ t where t is Element of P * : ( t in P & A . t <> 0 ) } ;

coherence { t where t is Element of P * : ( t in P & A . t <> 0 ) } ;

{ t where t is Element of P * : ( t in P & A . t <> 0 ) } is Subset of P

proof end;

:: deftheorem Def9 defines Polish-atoms POLNOT_1:def 7 :

for P being FinSequence-membered set

for A being Function of P,NAT

for b_{3} being Subset of (P *) holds

( b_{3} = Polish-atoms (P,A) iff for a being object holds

( a in b_{3} iff ( a in P & A . a = 0 ) ) );

for P being FinSequence-membered set

for A being Function of P,NAT

for b

( b

( a in b

:: deftheorem defines Polish-operations POLNOT_1:def 8 :

for P being FinSequence-membered set

for A being Function of P,NAT holds Polish-operations (P,A) = { t where t is Element of P * : ( t in P & A . t <> 0 ) } ;

for P being FinSequence-membered set

for A being Function of P,NAT holds Polish-operations (P,A) = { t where t is Element of P * : ( t in P & A . t <> 0 ) } ;

theorem Th26: :: POLNOT_1:19

for P being FinSequence-membered set

for A being Function of P,NAT

for U being Subset of (P *) holds Polish-atoms (P,A) c= Polish-expression-layer (P,A,U)

for A being Function of P,NAT

for U being Subset of (P *) holds Polish-atoms (P,A) c= Polish-expression-layer (P,A,U)

proof end;

theorem Th27: :: POLNOT_1:20

for P being FinSequence-membered set

for A being Function of P,NAT

for U, V being Subset of (P *) st U c= V holds

Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V)

for A being Function of P,NAT

for U, V being Subset of (P *) st U c= V holds

Polish-expression-layer (P,A,U) c= Polish-expression-layer (P,A,V)

proof end;

theorem TH21: :: POLNOT_1:21

for P being FinSequence-membered set

for A being Function of P,NAT

for U being Subset of (P *)

for u being FinSequence st u in Polish-expression-layer (P,A,U) holds

ex p, q being FinSequence st

( p in P & u = p ^ q )

for A being Function of P,NAT

for U being Subset of (P *)

for u being FinSequence st u in Polish-expression-layer (P,A,U) holds

ex p, q being FinSequence st

( p in P & u = p ^ q )

proof end;

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st

( U = b_{1} . n & b_{1} . (n + 1) = Polish-expression-layer (P,A,U) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & b_{1} . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st

( U = b_{1} . n & b_{1} . (n + 1) = Polish-expression-layer (P,A,U) ) ) & dom b_{2} = NAT & b_{2} . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st

( U = b_{2} . n & b_{2} . (n + 1) = Polish-expression-layer (P,A,U) ) ) holds

b_{1} = b_{2}

end;
let A be Function of P,NAT;

func Polish-expression-hierarchy (P,A) -> Function means :Def10: :: POLNOT_1:def 9

( dom it = NAT & it . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st

( U = it . n & it . (n + 1) = Polish-expression-layer (P,A,U) ) ) );

existence ( dom it = NAT & it . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st

( U = it . n & it . (n + 1) = Polish-expression-layer (P,A,U) ) ) );

ex b

( dom b

( U = b

proof end;

uniqueness for b

( U = b

( U = b

b

proof end;

:: deftheorem Def10 defines Polish-expression-hierarchy POLNOT_1:def 9 :

for P being FinSequence-membered set

for A being Function of P,NAT

for b_{3} being Function holds

( b_{3} = Polish-expression-hierarchy (P,A) iff ( dom b_{3} = NAT & b_{3} . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st

( U = b_{3} . n & b_{3} . (n + 1) = Polish-expression-layer (P,A,U) ) ) ) );

for P being FinSequence-membered set

for A being Function of P,NAT

for b

( b

( U = b

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

let n be Nat;

(Polish-expression-hierarchy (P,A)) . n is Subset of (P *)

end;
let A be Function of P,NAT;

let n be Nat;

func Polish-expression-hierarchy (P,A,n) -> Subset of (P *) equals :: POLNOT_1:def 10

(Polish-expression-hierarchy (P,A)) . n;

coherence (Polish-expression-hierarchy (P,A)) . n;

(Polish-expression-hierarchy (P,A)) . n is Subset of (P *)

proof end;

:: deftheorem defines Polish-expression-hierarchy POLNOT_1:def 10 :

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,n) = (Polish-expression-hierarchy (P,A)) . n;

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,n) = (Polish-expression-hierarchy (P,A)) . n;

theorem TH22: :: POLNOT_1:22

for P being FinSequence-membered set

for A being Function of P,NAT holds Polish-expression-hierarchy (P,A,0) = Polish-atoms (P,A) by Def10;

for A being Function of P,NAT holds Polish-expression-hierarchy (P,A,0) = Polish-atoms (P,A) by Def10;

theorem Th31: :: POLNOT_1:23

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,(n + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,n)))

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,(n + 1)) = Polish-expression-layer (P,A,(Polish-expression-hierarchy (P,A,n)))

proof end;

theorem Th33: :: POLNOT_1:24

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-hierarchy (P,A,(n + 1))

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-hierarchy (P,A,(n + 1))

proof end;

theorem Th34: :: POLNOT_1:25

for P being FinSequence-membered set

for A being Function of P,NAT

for n, m being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-hierarchy (P,A,(n + m))

for A being Function of P,NAT

for n, m being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-hierarchy (P,A,(n + m))

proof end;

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } is Subset of (P *)

end;
let A be Function of P,NAT;

func Polish-expression-set (P,A) -> Subset of (P *) equals :: POLNOT_1:def 11

union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;

coherence union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;

union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } is Subset of (P *)

proof end;

:: deftheorem defines Polish-expression-set POLNOT_1:def 11 :

for P being FinSequence-membered set

for A being Function of P,NAT holds Polish-expression-set (P,A) = union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;

for P being FinSequence-membered set

for A being Function of P,NAT holds Polish-expression-set (P,A) = union { (Polish-expression-hierarchy (P,A,n)) where n is Nat : verum } ;

theorem Th35: :: POLNOT_1:26

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-set (P,A)

for A being Function of P,NAT

for n being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-set (P,A)

proof end;

theorem Th36: :: POLNOT_1:27

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat

for q being FinSequence st q in (Polish-expression-set (P,A)) ^^ n holds

ex m being Nat st q in (Polish-expression-hierarchy (P,A,m)) ^^ n

for A being Function of P,NAT

for n being Nat

for q being FinSequence st q in (Polish-expression-set (P,A)) ^^ n holds

ex m being Nat st q in (Polish-expression-hierarchy (P,A,m)) ^^ n

proof end;

theorem Th37: :: POLNOT_1:28

for P being FinSequence-membered set

for A being Function of P,NAT

for a being object st a in Polish-expression-set (P,A) holds

ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1))

for A being Function of P,NAT

for a being object st a in Polish-expression-set (P,A) holds

ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1))

proof end;

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

mode Polish-expression of P,A is Element of Polish-expression-set (P,A);

end;
let A be Function of P,NAT;

mode Polish-expression of P,A is Element of Polish-expression-set (P,A);

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

let n be Nat;

let t be FinSequence;

assume A0: t in P ;

ex b_{1} being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) st

for q being FinSequence st q in dom b_{1} holds

b_{1} . q = t ^ q

for b_{1}, b_{2} being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) st ( for q being FinSequence st q in dom b_{1} holds

b_{1} . q = t ^ q ) & ( for q being FinSequence st q in dom b_{2} holds

b_{2} . q = t ^ q ) holds

b_{1} = b_{2}

end;
let A be Function of P,NAT;

let n be Nat;

let t be FinSequence;

assume A0: t in P ;

func Polish-operation (P,A,n,t) -> Function of ((Polish-expression-set (P,A)) ^^ n),(P *) means :Def13: :: POLNOT_1:def 12

for q being FinSequence st q in dom it holds

it . q = t ^ q;

existence for q being FinSequence st q in dom it holds

it . q = t ^ q;

ex b

for q being FinSequence st q in dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines Polish-operation POLNOT_1:def 12 :

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat

for t being FinSequence st t in P holds

for b_{5} being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) holds

( b_{5} = Polish-operation (P,A,n,t) iff for q being FinSequence st q in dom b_{5} holds

b_{5} . q = t ^ q );

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat

for t being FinSequence st t in P holds

for b

( b

b

definition

let X, Y be set ;

let F be PartFunc of X,(bool Y);

( F is disjoint_valued iff for a, b being object st a in dom F & b in dom F & a <> b holds

F . a misses F . b )

end;
let F be PartFunc of X,(bool Y);

:: original: disjoint_valued

redefine attr F is disjoint_valued means :Def21: :: POLNOT_1:def 13

for a, b being object st a in dom F & b in dom F & a <> b holds

F . a misses F . b;

compatibility redefine attr F is disjoint_valued means :Def21: :: POLNOT_1:def 13

for a, b being object st a in dom F & b in dom F & a <> b holds

F . a misses F . b;

( F is disjoint_valued iff for a, b being object st a in dom F & b in dom F & a <> b holds

F . a misses F . b )

proof end;

:: deftheorem Def21 defines disjoint_valued POLNOT_1:def 13 :

for X, Y being set

for F being PartFunc of X,(bool Y) holds

( F is disjoint_valued iff for a, b being object st a in dom F & b in dom F & a <> b holds

F . a misses F . b );

for X, Y being set

for F being PartFunc of X,(bool Y) holds

( F is disjoint_valued iff for a, b being object st a in dom F & b in dom F & a <> b holds

F . a misses F . b );

registration

let X be set ;

not for b_{1} being FinSequence of bool X holds b_{1} is V107()

end;
cluster Relation-like NAT -defined bool X -valued Function-like V38() FinSequence-like FinSubsequence-like V107() for FinSequence of bool X;

existence not for b

proof end;

theorem Th40: :: POLNOT_1:29

for X being set

for B being V107() FinSequence of bool X

for a, b, c being object st a in B . b & a in B . c holds

( b = c & b in dom B )

for B being V107() FinSequence of bool X

for a, b, c being object st a in B . b & a in B . c holds

( b = c & b in dom B )

proof end;

definition

let X be set ;

let B be V107() FinSequence of bool X;

ex b_{1} being Function of X,NAT st

for a being object holds

( not a in X or ( ex n being Nat st a in B . n & a in B . (b_{1} . a) ) or ( ( for n being Nat holds not a in B . n ) & b_{1} . a = 0 ) )

for b_{1}, b_{2} being Function of X,NAT st ( for a being object holds

( not a in X or ( ex n being Nat st a in B . n & a in B . (b_{1} . a) ) or ( ( for n being Nat holds not a in B . n ) & b_{1} . a = 0 ) ) ) & ( for a being object holds

( not a in X or ( ex n being Nat st a in B . n & a in B . (b_{2} . a) ) or ( ( for n being Nat holds not a in B . n ) & b_{2} . a = 0 ) ) ) holds

b_{1} = b_{2}

end;
let B be V107() FinSequence of bool X;

func arity-from-list B -> Function of X,NAT means :Def22: :: POLNOT_1:def 14

for a being object holds

( not a in X or ( ex n being Nat st a in B . n & a in B . (it . a) ) or ( ( for n being Nat holds not a in B . n ) & it . a = 0 ) );

existence for a being object holds

( not a in X or ( ex n being Nat st a in B . n & a in B . (it . a) ) or ( ( for n being Nat holds not a in B . n ) & it . a = 0 ) );

ex b

for a being object holds

( not a in X or ( ex n being Nat st a in B . n & a in B . (b

proof end;

uniqueness for b

( not a in X or ( ex n being Nat st a in B . n & a in B . (b

( not a in X or ( ex n being Nat st a in B . n & a in B . (b

b

proof end;

:: deftheorem Def22 defines arity-from-list POLNOT_1:def 14 :

for X being set

for B being V107() FinSequence of bool X

for b_{3} being Function of X,NAT holds

( b_{3} = arity-from-list B iff for a being object holds

( not a in X or ( ex n being Nat st a in B . n & a in B . (b_{3} . a) ) or ( ( for n being Nat holds not a in B . n ) & b_{3} . a = 0 ) ) );

for X being set

for B being V107() FinSequence of bool X

for b

( b

( not a in X or ( ex n being Nat st a in B . n & a in B . (b

theorem TH30: :: POLNOT_1:30

for X being set

for B being V107() FinSequence of bool X

for a being object st a in X holds

( (arity-from-list B) . a <> 0 iff ex n being Nat st a in B . n )

for B being V107() FinSequence of bool X

for a being object st a in X holds

( (arity-from-list B) . a <> 0 iff ex n being Nat st a in B . n )

proof end;

theorem :: POLNOT_1:31

for X being set

for B being V107() FinSequence of bool X

for a being object

for n being Nat st a in B . n holds

(arity-from-list B) . a = n

for B being V107() FinSequence of bool X

for a being object

for n being Nat st a in B . n holds

(arity-from-list B) . a = n

proof end;

theorem TH32: :: POLNOT_1:32

for P being FinSequence-membered set

for A being Function of P,NAT

for r being FinSequence st r in Polish-expression-set (P,A) holds

ex n being Nat ex p, q being FinSequence st

( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )

for A being Function of P,NAT

for r being FinSequence st r in Polish-expression-set (P,A) holds

ex n being Nat ex p, q being FinSequence st

( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )

proof end;

definition

let P be FinSequence-membered set ;

let A be Function of P,NAT;

let Q be FinSequence-membered set ;

end;
let A be Function of P,NAT;

let Q be FinSequence-membered set ;

attr Q is A -closed means :: POLNOT_1:def 15

for p being FinSequence

for n being Nat

for q being FinSequence st p in P & n = A . p & q in Q ^^ n holds

p ^ q in Q;

for p being FinSequence

for n being Nat

for q being FinSequence st p in P & n = A . p & q in Q ^^ n holds

p ^ q in Q;

:: deftheorem defines -closed POLNOT_1:def 15 :

for P being FinSequence-membered set

for A being Function of P,NAT

for Q being FinSequence-membered set holds

( Q is A -closed iff for p being FinSequence

for n being Nat

for q being FinSequence st p in P & n = A . p & q in Q ^^ n holds

p ^ q in Q );

for P being FinSequence-membered set

for A being Function of P,NAT

for Q being FinSequence-membered set holds

( Q is A -closed iff for p being FinSequence

for n being Nat

for q being FinSequence st p in P & n = A . p & q in Q ^^ n holds

p ^ q in Q );

theorem TH51: :: POLNOT_1:33

for P being FinSequence-membered set

for A being Function of P,NAT holds Polish-expression-set (P,A) is A -closed

for A being Function of P,NAT holds Polish-expression-set (P,A) is A -closed

proof end;

theorem Th52: :: POLNOT_1:34

for P being FinSequence-membered set

for A being Function of P,NAT

for Q being FinSequence-membered set st Q is A -closed holds

Polish-atoms (P,A) c= Q

for A being Function of P,NAT

for Q being FinSequence-membered set st Q is A -closed holds

Polish-atoms (P,A) c= Q

proof end;

theorem Th53: :: POLNOT_1:35

for P being FinSequence-membered set

for A being Function of P,NAT

for Q being FinSequence-membered set

for n being Nat st Q is A -closed holds

Polish-expression-hierarchy (P,A,n) c= Q

for A being Function of P,NAT

for Q being FinSequence-membered set

for n being Nat st Q is A -closed holds

Polish-expression-hierarchy (P,A,n) c= Q

proof end;

theorem TH36: :: POLNOT_1:36

for P being FinSequence-membered set

for A being Function of P,NAT holds Polish-atoms (P,A) c= Polish-expression-set (P,A)

for A being Function of P,NAT holds Polish-atoms (P,A) c= Polish-expression-set (P,A)

proof end;

theorem Th55: :: POLNOT_1:37

for P being FinSequence-membered set

for A being Function of P,NAT

for Q being FinSequence-membered set st Q is A -closed holds

Polish-expression-set (P,A) c= Q

for A being Function of P,NAT

for Q being FinSequence-membered set st Q is A -closed holds

Polish-expression-set (P,A) c= Q

proof end;

theorem :: POLNOT_1:38

for P being FinSequence-membered set

for A being Function of P,NAT

for r being FinSequence st r in Polish-expression-set (P,A) holds

ex n being Nat ex t, q being FinSequence st

( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q )

for A being Function of P,NAT

for r being FinSequence st r in Polish-expression-set (P,A) holds

ex n being Nat ex t, q being FinSequence st

( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q )

proof end;

theorem TH39: :: POLNOT_1:39

for P being FinSequence-membered set

for A being Function of P,NAT

for n being Nat

for p, q being FinSequence st p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n holds

(Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)

for A being Function of P,NAT

for n being Nat

for p, q being FinSequence st p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n holds

(Polish-operation (P,A,n,p)) . q in Polish-expression-set (P,A)

proof end;

scheme :: POLNOT_1:sch 1

AInd{ F_{1}() -> FinSequence-membered set , F_{2}() -> Function of F_{1}(),NAT, P_{1}[ object ] } :

provided

AInd{ F

provided

A1:
for p, q being FinSequence

for n being Nat st p in F_{1}() & n = F_{2}() . p & q in (Polish-expression-set (F_{1}(),F_{2}())) ^^ n holds

P_{1}[p ^ q]

for n being Nat st p in F

P

proof end;

definition

let P be FinSequence-membered set ;

end;
attr P is antichain-like means :Def1: :: POLNOT_1:def 16

for p, q being FinSequence st p in P & p ^ q in P holds

q = {} ;

for p, q being FinSequence st p in P & p ^ q in P holds

q = {} ;

:: deftheorem Def1 defines antichain-like POLNOT_1:def 16 :

for P being FinSequence-membered set holds

( P is antichain-like iff for p, q being FinSequence st p in P & p ^ q in P holds

q = {} );

for P being FinSequence-membered set holds

( P is antichain-like iff for p, q being FinSequence st p in P & p ^ q in P holds

q = {} );

theorem Th1: :: POLNOT_1:40

for P being FinSequence-membered set holds

( P is antichain-like iff for p, q being FinSequence st p in P & p ^ q in P holds

p = p ^ q )

( P is antichain-like iff for p, q being FinSequence st p in P & p ^ q in P holds

p = p ^ q )

proof end;

registration

coherence

for b_{1} being FinSequence-membered set st b_{1} is trivial holds

b_{1} is antichain-like

end;
for b

b

proof end;

theorem :: POLNOT_1:42

registration

existence

ex b_{1} being non empty FinSequence-membered set st b_{1} is antichain-like

for b_{1} being FinSequence-membered set st b_{1} is empty holds

b_{1} is antichain-like
;

end;
ex b

proof end;

coherence for b

b

registration

let B be antichain;

coherence

for b_{1} being Subset of B holds

( b_{1} is antichain-like & b_{1} is FinSequence-membered )
by TH2;

end;
coherence

for b

( b

definition

let D be non empty set ;

let G be Subset of (D *);

( G is antichain-like iff for g, h being FinSequence of D st g in G & g ^ h in G holds

h = <*> D )

end;
let G be Subset of (D *);

:: original: antichain-like

redefine attr G is antichain-like means :: POLNOT_1:def 17

for g, h being FinSequence of D st g in G & g ^ h in G holds

h = <*> D;

compatibility redefine attr G is antichain-like means :: POLNOT_1:def 17

for g, h being FinSequence of D st g in G & g ^ h in G holds

h = <*> D;

( G is antichain-like iff for g, h being FinSequence of D st g in G & g ^ h in G holds

h = <*> D )

proof end;

:: deftheorem defines antichain-like POLNOT_1:def 17 :

for D being non empty set

for G being Subset of (D *) holds

( G is antichain-like iff for g, h being FinSequence of D st g in G & g ^ h in G holds

h = <*> D );

for D being non empty set

for G being Subset of (D *) holds

( G is antichain-like iff for g, h being FinSequence of D st g in G & g ^ h in G holds

h = <*> D );

theorem TH4: :: POLNOT_1:43

for B being antichain

for p, q, r, s being FinSequence st p ^ q = r ^ s & p in B & r in B holds

( p = r & q = s )

for p, q, r, s being FinSequence st p ^ q = r ^ s & p in B & r in B holds

( p = r & q = s )

proof end;

Th5: for B, C being antichain holds B ^ C is antichain-like

proof end;

theorem Th6: :: POLNOT_1:44

for P being FinSequence-membered set st ( for p, q being FinSequence st p in P & q in P holds

dom p = dom q ) holds

P is antichain-like

dom p = dom q ) holds

P is antichain-like

proof end;

theorem TH7: :: POLNOT_1:45

for P being FinSequence-membered set

for a being object st ( for p being FinSequence st p in P holds

dom p = a ) holds

P is antichain-like

for a being object st ( for p being FinSequence st p in P holds

dom p = a ) holds

P is antichain-like

proof end;

registration

let T be Polish-language;

existence

ex b_{1} being Subset of (T *) st

( not b_{1} is empty & b_{1} is antichain-like )

coherence

not T ^^ n is empty ;

end;
existence

ex b

( not b

proof end;

let n be Nat;coherence

not T ^^ n is empty ;

definition

let T be Polish-language;

mode Polish-language of T is non empty antichain-like Subset of (T *);

ex b_{1} being Function of T,NAT ex a being object st

( a in T & b_{1} . a = 0 )

end;
mode Polish-language of T is non empty antichain-like Subset of (T *);

mode Polish-arity-function of T -> Function of T,NAT means :Def5: :: POLNOT_1:def 18

ex a being object st

( a in T & it . a = 0 );

existence ex a being object st

( a in T & it . a = 0 );

ex b

( a in T & b

proof end;

:: deftheorem Def5 defines Polish-arity-function POLNOT_1:def 18 :

for T being Polish-language

for b_{2} being Function of T,NAT holds

( b_{2} is Polish-arity-function of T iff ex a being object st

( a in T & b_{2} . a = 0 ) );

for T being Polish-language

for b

( b

( a in T & b

registration

let T be Polish-language;

coherence

for b_{1} being Polish-language of T holds

( not b_{1} is empty & b_{1} is antichain-like & b_{1} is FinSequence-membered )
;

end;
coherence

for b

( not b

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let t be Element of T;

:: original: .

redefine func A . t -> Nat;

coherence

A . t is Nat by FUNCT_2:5, ORDINAL1:def 12;

end;
let A be Polish-arity-function of T;

let t be Element of T;

:: original: .

redefine func A . t -> Nat;

coherence

A . t is Nat by FUNCT_2:5, ORDINAL1:def 12;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let U be Polish-language of T;

for b_{1} being Subset of (T *) holds

( b_{1} = Polish-expression-layer (T,A,U) iff for a being object holds

( a in b_{1} iff ex t being Element of T ex u being Element of T * st

( a = t ^ u & u in U ^^ (A . t) ) ) )

end;
let A be Polish-arity-function of T;

let U be Polish-language of T;

redefine func Polish-expression-layer (T,A,U) means :Def6: :: POLNOT_1:def 19

for a being object holds

( a in it iff ex t being Element of T ex u being Element of T * st

( a = t ^ u & u in U ^^ (A . t) ) );

compatibility for a being object holds

( a in it iff ex t being Element of T ex u being Element of T * st

( a = t ^ u & u in U ^^ (A . t) ) );

for b

( b

( a in b

( a = t ^ u & u in U ^^ (A . t) ) ) )

proof end;

:: deftheorem Def6 defines Polish-expression-layer POLNOT_1:def 19 :

for T being Polish-language

for A being Polish-arity-function of T

for U being Polish-language of T

for b_{4} being Subset of (T *) holds

( b_{4} = Polish-expression-layer (T,A,U) iff for a being object holds

( a in b_{4} iff ex t being Element of T ex u being Element of T * st

( a = t ^ u & u in U ^^ (A . t) ) ) );

for T being Polish-language

for A being Polish-arity-function of T

for U being Polish-language of T

for b

( b

( a in b

( a = t ^ u & u in U ^^ (A . t) ) ) );

:: deftheorem defines -headed POLNOT_1:def 20 :

for B being antichain

for p being FinSequence holds

( p is B -headed iff ex q, r being FinSequence st

( q in B & p = q ^ r ) );

for B being antichain

for p being FinSequence holds

( p is B -headed iff ex q, r being FinSequence st

( q in B & p = q ^ r ) );

definition

let B be antichain;

let P be FinSequence-membered set ;

end;
let P be FinSequence-membered set ;

attr P is B -headed means :Def8: :: POLNOT_1:def 21

for p being FinSequence st p in P holds

p is B -headed ;

for p being FinSequence st p in P holds

p is B -headed ;

:: deftheorem Def8 defines -headed POLNOT_1:def 21 :

for B being antichain

for P being FinSequence-membered set holds

( P is B -headed iff for p being FinSequence st p in P holds

p is B -headed );

for B being antichain

for P being FinSequence-membered set holds

( P is B -headed iff for p being FinSequence st p in P holds

p is B -headed );

theorem :: POLNOT_1:48

Th13: for B being antichain

for P being FinSequence-membered set holds B ^ P is B -headed

proof end;

registration
end;

registration

let B be antichain;

existence

ex b_{1} being FinSequence-membered set st b_{1} is B -headed

end;
existence

ex b

proof end;

registration

let B be antichain;

let P be FinSequence-membered B -headed set ;

coherence

for b_{1} being Subset of P holds b_{1} is B -headed
by Def8;

end;
let P be FinSequence-membered B -headed set ;

coherence

for b

registration

let S be Polish-language;

existence

ex b_{1} being FinSequence-membered set st

( not b_{1} is empty & b_{1} is S -headed )

end;
existence

ex b

( not b

proof end;

definition

let S be Polish-language;

let p be FinSequence;

for b_{1} being FinSequence holds verum
;

existence

( ( p is S -headed implies ex b_{1} being FinSequence st

( b_{1} in S & ex r being FinSequence st p = b_{1} ^ r ) ) & ( not p is S -headed implies ex b_{1} being FinSequence st b_{1} = {} ) )
;

uniqueness

for b_{1}, b_{2} being FinSequence holds

( ( p is S -headed & b_{1} in S & ex r being FinSequence st p = b_{1} ^ r & b_{2} in S & ex r being FinSequence st p = b_{2} ^ r implies b_{1} = b_{2} ) & ( not p is S -headed & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )
by TH4;

end;
let p be FinSequence;

func S -head p -> FinSequence means :Def9a: :: POLNOT_1:def 22

( it in S & ex r being FinSequence st p = it ^ r ) if p is S -headed

otherwise it = {} ;

consistency ( it in S & ex r being FinSequence st p = it ^ r ) if p is S -headed

otherwise it = {} ;

for b

existence

( ( p is S -headed implies ex b

( b

uniqueness

for b

( ( p is S -headed & b

:: deftheorem Def9a defines -head POLNOT_1:def 22 :

for S being Polish-language

for p, b_{3} being FinSequence holds

( ( p is S -headed implies ( b_{3} = S -head p iff ( b_{3} in S & ex r being FinSequence st p = b_{3} ^ r ) ) ) & ( not p is S -headed implies ( b_{3} = S -head p iff b_{3} = {} ) ) );

for S being Polish-language

for p, b

( ( p is S -headed implies ( b

definition

let S be Polish-language;

let p be FinSequence;

existence

ex b_{1} being FinSequence st p = (S -head p) ^ b_{1}

for b_{1}, b_{2} being FinSequence st p = (S -head p) ^ b_{1} & p = (S -head p) ^ b_{2} holds

b_{1} = b_{2}
by FINSEQ_1:33;

end;
let p be FinSequence;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines -tail POLNOT_1:def 23 :

for S being Polish-language

for p, b_{3} being FinSequence holds

( b_{3} = S -tail p iff p = (S -head p) ^ b_{3} );

for S being Polish-language

for p, b

( b

theorem Th17: :: POLNOT_1:52

for S being Polish-language

for s, t being FinSequence st s in S holds

( S -head (s ^ t) = s & S -tail (s ^ t) = t )

for s, t being FinSequence st s in S holds

( S -head (s ^ t) = s & S -tail (s ^ t) = t )

proof end;

theorem Th18: :: POLNOT_1:53

for S being Polish-language

for s being FinSequence st s in S holds

( S -head s = s & S -tail s = {} )

for s being FinSequence st s in S holds

( S -head s = s & S -tail s = {} )

proof end;

theorem Th19: :: POLNOT_1:54

for S, T being Polish-language

for u being FinSequence st u in S ^ T holds

( S -head u in S & S -tail u in T )

for u being FinSequence st u in S ^ T holds

( S -head u in S & S -tail u in T )

proof end;

theorem Th20: :: POLNOT_1:55

for S, T being Polish-language

for u being FinSequence st S c= T & u is S -headed holds

( S -head u = T -head u & S -tail u = T -tail u )

for u being FinSequence st S c= T & u is S -headed holds

( S -head u = T -head u & S -tail u = T -tail u )

proof end;

theorem Th21: :: POLNOT_1:56

for S being Polish-language

for s, t being FinSequence st s is S -headed holds

( s ^ t is S -headed & S -head (s ^ t) = S -head s & S -tail (s ^ t) = (S -tail s) ^ t )

for s, t being FinSequence st s is S -headed holds

( s ^ t is S -headed & S -head (s ^ t) = S -head s & S -tail (s ^ t) = (S -tail s) ^ t )

proof end;

theorem Th22: :: POLNOT_1:57

for S being Polish-language

for m, n being Nat

for s being FinSequence st m + 1 <= n & s in S ^^ n holds

( s is S ^^ m -headed & (S ^^ m) -tail s is S -headed )

for m, n being Nat

for s being FinSequence st m + 1 <= n & s in S ^^ n holds

( s is S ^^ m -headed & (S ^^ m) -tail s is S -headed )

proof end;

theorem Th23: :: POLNOT_1:58

for S being Polish-language

for s being FinSequence holds

( s is S ^^ 0 -headed & (S ^^ 0) -head s = {} & (S ^^ 0) -tail s = s )

for s being FinSequence holds

( s is S ^^ 0 -headed & (S ^^ 0) -head s = {} & (S ^^ 0) -tail s = s )

proof end;

registration

let T be Polish-language;

let A be Polish-arity-function of T;

coherence

( not Polish-atoms (T,A) is empty & Polish-atoms (T,A) is antichain-like )

coherence

( not Polish-expression-layer (T,A,U) is empty & Polish-expression-layer (T,A,U) is antichain-like )

end;
let A be Polish-arity-function of T;

coherence

( not Polish-atoms (T,A) is empty & Polish-atoms (T,A) is antichain-like )

proof end;

let U be Polish-language of T;coherence

( not Polish-expression-layer (T,A,U) is empty & Polish-expression-layer (T,A,U) is antichain-like )

proof end;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let U be Polish-language of T;

:: original: Polish-expression-layer

redefine func Polish-expression-layer (T,A,U) -> Polish-language of T;

coherence

Polish-expression-layer (T,A,U) is Polish-language of T ;

end;
let A be Polish-arity-function of T;

let U be Polish-language of T;

:: original: Polish-expression-layer

redefine func Polish-expression-layer (T,A,U) -> Polish-language of T;

coherence

Polish-expression-layer (T,A,U) is Polish-language of T ;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

{ t where t is Element of T : A . t <> 0 } is Subset of T

end;
let A be Polish-arity-function of T;

func Polish-operations (T,A) -> Subset of T equals :: POLNOT_1:def 24

{ t where t is Element of T : A . t <> 0 } ;

coherence { t where t is Element of T : A . t <> 0 } ;

{ t where t is Element of T : A . t <> 0 } is Subset of T

proof end;

:: deftheorem defines Polish-operations POLNOT_1:def 24 :

for T being Polish-language

for A being Polish-arity-function of T holds Polish-operations (T,A) = { t where t is Element of T : A . t <> 0 } ;

for T being Polish-language

for A being Polish-arity-function of T holds Polish-operations (T,A) = { t where t is Element of T : A . t <> 0 } ;

registration

let T be Polish-language;

let A be Polish-arity-function of T;

let n be Nat;

coherence

( Polish-expression-hierarchy (T,A,n) is antichain-like & not Polish-expression-hierarchy (T,A,n) is empty )

end;
let A be Polish-arity-function of T;

let n be Nat;

coherence

( Polish-expression-hierarchy (T,A,n) is antichain-like & not Polish-expression-hierarchy (T,A,n) is empty )

proof end;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let n be Nat;

:: original: Polish-expression-hierarchy

redefine func Polish-expression-hierarchy (T,A,n) -> Polish-language of T;

coherence

Polish-expression-hierarchy (T,A,n) is Polish-language of T ;

end;
let A be Polish-arity-function of T;

let n be Nat;

:: original: Polish-expression-hierarchy

redefine func Polish-expression-hierarchy (T,A,n) -> Polish-language of T;

coherence

Polish-expression-hierarchy (T,A,n) is Polish-language of T ;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

Polish-expression-set (T,A) is Polish-language of T

end;
let A be Polish-arity-function of T;

func Polish-WFF-set (T,A) -> Polish-language of T equals :: POLNOT_1:def 25

Polish-expression-set (T,A);

coherence Polish-expression-set (T,A);

Polish-expression-set (T,A) is Polish-language of T

proof end;

:: deftheorem defines Polish-WFF-set POLNOT_1:def 25 :

for T being Polish-language

for A being Polish-arity-function of T holds Polish-WFF-set (T,A) = Polish-expression-set (T,A);

for T being Polish-language

for A being Polish-arity-function of T holds Polish-WFF-set (T,A) = Polish-expression-set (T,A);

definition

let T be Polish-language;

let A be Polish-arity-function of T;

mode Polish-WFF of T,A is Element of Polish-WFF-set (T,A);

end;
let A be Polish-arity-function of T;

mode Polish-WFF of T,A is Element of Polish-WFF-set (T,A);

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let t be Element of T;

Polish-operation (T,A,(A . t),t) is Function of ((Polish-WFF-set (T,A)) ^^ (A . t)),(Polish-WFF-set (T,A))

end;
let A be Polish-arity-function of T;

let t be Element of T;

func Polish-operation (T,A,t) -> Function of ((Polish-WFF-set (T,A)) ^^ (A . t)),(Polish-WFF-set (T,A)) equals :: POLNOT_1:def 26

Polish-operation (T,A,(A . t),t);

coherence Polish-operation (T,A,(A . t),t);

Polish-operation (T,A,(A . t),t) is Function of ((Polish-WFF-set (T,A)) ^^ (A . t)),(Polish-WFF-set (T,A))

proof end;

:: deftheorem defines Polish-operation POLNOT_1:def 26 :

for T being Polish-language

for A being Polish-arity-function of T

for t being Element of T holds Polish-operation (T,A,t) = Polish-operation (T,A,(A . t),t);

for T being Polish-language

for A being Polish-arity-function of T

for t being Element of T holds Polish-operation (T,A,t) = Polish-operation (T,A,(A . t),t);

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let t be Element of T;

assume A1: A . t = 1 ;

Polish-operation (T,A,t) is UnOp of (Polish-WFF-set (T,A))

end;
let A be Polish-arity-function of T;

let t be Element of T;

assume A1: A . t = 1 ;

func Polish-unOp (T,A,t) -> UnOp of (Polish-WFF-set (T,A)) equals :Def21: :: POLNOT_1:def 27

Polish-operation (T,A,t);

coherence Polish-operation (T,A,t);

Polish-operation (T,A,t) is UnOp of (Polish-WFF-set (T,A))

proof end;

:: deftheorem Def21 defines Polish-unOp POLNOT_1:def 27 :

for T being Polish-language

for A being Polish-arity-function of T

for t being Element of T st A . t = 1 holds

Polish-unOp (T,A,t) = Polish-operation (T,A,t);

for T being Polish-language

for A being Polish-arity-function of T

for t being Element of T st A . t = 1 holds

Polish-unOp (T,A,t) = Polish-operation (T,A,t);

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let t be Element of T;

assume A1: A . t = 2 ;

ex b_{1} being BinOp of (Polish-WFF-set (T,A)) st

for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds

b_{1} . (u,v) = (Polish-operation (T,A,t)) . (u ^ v)

for b_{1}, b_{2} being BinOp of (Polish-WFF-set (T,A)) st ( for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds

b_{1} . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ) & ( for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds

b_{2} . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ) holds

b_{1} = b_{2}

end;
let A be Polish-arity-function of T;

let t be Element of T;

assume A1: A . t = 2 ;

func Polish-binOp (T,A,t) -> BinOp of (Polish-WFF-set (T,A)) means :Def22: :: POLNOT_1:def 28

for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds

it . (u,v) = (Polish-operation (T,A,t)) . (u ^ v);

existence for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds

it . (u,v) = (Polish-operation (T,A,t)) . (u ^ v);

ex b

for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def22 defines Polish-binOp POLNOT_1:def 28 :

for T being Polish-language

for A being Polish-arity-function of T

for t being Element of T st A . t = 2 holds

for b_{4} being BinOp of (Polish-WFF-set (T,A)) holds

( b_{4} = Polish-binOp (T,A,t) iff for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds

b_{4} . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) );

for T being Polish-language

for A being Polish-arity-function of T

for t being Element of T st A . t = 2 holds

for b

( b

b

definition

let X, Y be set ;

let F be PartFunc of X,(bool Y);

end;
let F be PartFunc of X,(bool Y);

attr F is exhaustive means :: POLNOT_1:def 29

for a being object st a in Y holds

ex b being object st

( b in dom F & a in F . b );

for a being object st a in Y holds

ex b being object st

( b in dom F & a in F . b );

:: deftheorem defines exhaustive POLNOT_1:def 29 :

for X, Y being set

for F being PartFunc of X,(bool Y) holds

( F is exhaustive iff for a being object st a in Y holds

ex b being object st

( b in dom F & a in F . b ) );

for X, Y being set

for F being PartFunc of X,(bool Y) holds

( F is exhaustive iff for a being object st a in Y holds

ex b being object st

( b in dom F & a in F . b ) );

registration

let X be non empty set ;

ex b_{1} being FinSequence of bool X st

( not b_{1} is exhaustive & b_{1} is V107() )

end;
cluster Relation-like NAT -defined bool X -valued Function-like V38() FinSequence-like FinSubsequence-like V107() non exhaustive for FinSequence of bool X;

existence ex b

( not b

proof end;

definition

let T be Polish-language;

let B be V107() non exhaustive FinSequence of bool T;

arity-from-list B is Polish-arity-function of T

end;
let B be V107() non exhaustive FinSequence of bool T;

func Polish-arity-from-list B -> Polish-arity-function of T equals :: POLNOT_1:def 30

arity-from-list B;

coherence arity-from-list B;

arity-from-list B is Polish-arity-function of T

proof end;

:: deftheorem defines Polish-arity-from-list POLNOT_1:def 30 :

for T being Polish-language

for B being V107() non exhaustive FinSequence of bool T holds Polish-arity-from-list B = arity-from-list B;

for T being Polish-language

for B being V107() non exhaustive FinSequence of bool T holds Polish-arity-from-list B = arity-from-list B;

registration

existence

ex b_{1} being FinSequence-membered antichain-like set st b_{1} is with_non-empty_elements

not for b_{1} being Polish-language holds b_{1} is trivial

end;
ex b

proof end;

existence not for b

proof end;

registration

for b_{1} being FinSequence-membered antichain-like set st not b_{1} is trivial holds

b_{1} is with_non-empty_elements
by TH8, SETFAM_1:def 8;

end;

cluster non trivial FinSequence-membered antichain-like -> FinSequence-membered with_non-empty_elements antichain-like for set ;

coherence for b

b

definition

let S be Polish-language;

let n, m be Nat;

let p be Element of S ^^ ((n + 1) + m);

coherence

S -head ((S ^^ n) -tail p) is Element of S

end;
let n, m be Nat;

let p be Element of S ^^ ((n + 1) + m);

coherence

S -head ((S ^^ n) -tail p) is Element of S

proof end;

:: deftheorem defines decomp POLNOT_1:def 31 :

for S being Polish-language

for n, m being Nat

for p being Element of S ^^ ((n + 1) + m) holds decomp (S,n,m,p) = S -head ((S ^^ n) -tail p);

for S being Polish-language

for n, m being Nat

for p being Element of S ^^ ((n + 1) + m) holds decomp (S,n,m,p) = S -head ((S ^^ n) -tail p);

definition

let S be Polish-language;

let n be Nat;

let p be Element of S ^^ n;

ex b_{1} being FinSequence of S st

( dom b_{1} = Seg n & ( for m being Nat st m in Seg n holds

ex k being Nat st

( m = k + 1 & b_{1} . m = S -head ((S ^^ k) -tail p) ) ) )

for b_{1}, b_{2} being FinSequence of S st dom b_{1} = Seg n & ( for m being Nat st m in Seg n holds

ex k being Nat st

( m = k + 1 & b_{1} . m = S -head ((S ^^ k) -tail p) ) ) & dom b_{2} = Seg n & ( for m being Nat st m in Seg n holds

ex k being Nat st

( m = k + 1 & b_{2} . m = S -head ((S ^^ k) -tail p) ) ) holds

b_{1} = b_{2}

end;
let n be Nat;

let p be Element of S ^^ n;

func decomp (S,n,p) -> FinSequence of S means :Def32: :: POLNOT_1:def 32

( dom it = Seg n & ( for m being Nat st m in Seg n holds

ex k being Nat st

( m = k + 1 & it . m = S -head ((S ^^ k) -tail p) ) ) );

existence ( dom it = Seg n & ( for m being Nat st m in Seg n holds

ex k being Nat st

( m = k + 1 & it . m = S -head ((S ^^ k) -tail p) ) ) );

ex b

( dom b

ex k being Nat st

( m = k + 1 & b

proof end;

uniqueness for b

ex k being Nat st

( m = k + 1 & b

ex k being Nat st

( m = k + 1 & b

b

proof end;

:: deftheorem Def32 defines decomp POLNOT_1:def 32 :

for S being Polish-language

for n being Nat

for p being Element of S ^^ n

for b_{4} being FinSequence of S holds

( b_{4} = decomp (S,n,p) iff ( dom b_{4} = Seg n & ( for m being Nat st m in Seg n holds

ex k being Nat st

( m = k + 1 & b_{4} . m = S -head ((S ^^ k) -tail p) ) ) ) );

for S being Polish-language

for n being Nat

for p being Element of S ^^ n

for b

( b

ex k being Nat st

( m = k + 1 & b

theorem Th50: :: POLNOT_1:60

for S, T being Polish-language

for n being Nat

for s being Element of S ^^ n

for t being Element of T ^^ n st S c= T & s = t holds

decomp (S,n,s) = decomp (T,n,t)

for n being Nat

for s being Element of S ^^ n

for t being Element of T ^^ n st S c= T & s = t holds

decomp (S,n,s) = decomp (T,n,t)

proof end;

theorem Th54: :: POLNOT_1:62

for S being Polish-language

for n being Nat

for q being Element of S ^^ n holds len (decomp (S,n,q)) = n

for n being Nat

for q being Element of S ^^ n holds len (decomp (S,n,q)) = n

proof end;

theorem Th56: :: POLNOT_1:64

for S being Polish-language

for p, q being Element of S

for r being Element of S ^^ 2 st r = p ^ q holds

decomp (S,2,r) = <*p,q*>

for p, q being Element of S

for r being Element of S ^^ 2 st r = p ^ q holds

decomp (S,2,r) = <*p,q*>

proof end;

theorem Th60: :: POLNOT_1:65

for T being Polish-language

for A being Polish-arity-function of T holds Polish-WFF-set (T,A) is T -headed

for A being Polish-arity-function of T holds Polish-WFF-set (T,A) is T -headed

proof end;

theorem Th61: :: POLNOT_1:66

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat holds Polish-expression-hierarchy (T,A,n) is T -headed

for A being Polish-arity-function of T

for n being Nat holds Polish-expression-hierarchy (T,A,n) is T -headed

proof end;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

coherence

T -head F is Element of T

end;
let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

coherence

T -head F is Element of T

proof end;

:: deftheorem defines Polish-WFF-head POLNOT_1:def 33 :

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds Polish-WFF-head F = T -head F;

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds Polish-WFF-head F = T -head F;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,n);

coherence

T -head F is Element of T

end;
let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,n);

coherence

T -head F is Element of T

proof end;

:: deftheorem defines Polish-WFF-head POLNOT_1:def 34 :

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,n) holds Polish-WFF-head F = T -head F;

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,n) holds Polish-WFF-head F = T -head F;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

coherence

A . (Polish-WFF-head F) is Nat ;

end;
let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

coherence

A . (Polish-WFF-head F) is Nat ;

:: deftheorem defines Polish-arity POLNOT_1:def 35 :

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds Polish-arity F = A . (Polish-WFF-head F);

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds Polish-arity F = A . (Polish-WFF-head F);

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,n);

coherence

A . (Polish-WFF-head F) is Nat ;

end;
let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,n);

coherence

A . (Polish-WFF-head F) is Nat ;

:: deftheorem defines Polish-arity POLNOT_1:def 36 :

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,n) holds Polish-arity F = A . (Polish-WFF-head F);

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,n) holds Polish-arity F = A . (Polish-WFF-head F);

theorem Th62: :: POLNOT_1:67

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F)

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F)

proof end;

theorem Th63: :: POLNOT_1:68

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds T -tail F in (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F)

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds T -tail F in (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F)

proof end;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

T -tail F is Element of (Polish-WFF-set (T,A)) ^^ (Polish-arity F) by Th62;

end;
let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

func (T,A) -tail F -> Element of (Polish-WFF-set (T,A)) ^^ (Polish-arity F) equals :: POLNOT_1:def 37

T -tail F;

coherence T -tail F;

T -tail F is Element of (Polish-WFF-set (T,A)) ^^ (Polish-arity F) by Th62;

:: deftheorem defines -tail POLNOT_1:def 37 :

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds (T,A) -tail F = T -tail F;

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds (T,A) -tail F = T -tail F;

theorem :: POLNOT_1:69

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A st T -head F in Polish-atoms (T,A) holds

F = T -head F

for A being Polish-arity-function of T

for F being Polish-WFF of T,A st T -head F in Polish-atoms (T,A) holds

F = T -head F

proof end;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,(n + 1));

T -tail F is Element of (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F) by Th63;

end;
let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,(n + 1));

func (T,A) -tail F -> Element of (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F) equals :: POLNOT_1:def 38

T -tail F;

coherence T -tail F;

T -tail F is Element of (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F) by Th63;

:: deftheorem defines -tail POLNOT_1:def 38 :

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds (T,A) -tail F = T -tail F;

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds (T,A) -tail F = T -tail F;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

decomp ((Polish-WFF-set (T,A)),(Polish-arity F),((T,A) -tail F)) is FinSequence of Polish-WFF-set (T,A) ;

end;
let A be Polish-arity-function of T;

let F be Polish-WFF of T,A;

func Polish-WFF-args F -> FinSequence of Polish-WFF-set (T,A) equals :: POLNOT_1:def 39

decomp ((Polish-WFF-set (T,A)),(Polish-arity F),((T,A) -tail F));

coherence decomp ((Polish-WFF-set (T,A)),(Polish-arity F),((T,A) -tail F));

decomp ((Polish-WFF-set (T,A)),(Polish-arity F),((T,A) -tail F)) is FinSequence of Polish-WFF-set (T,A) ;

:: deftheorem defines Polish-WFF-args POLNOT_1:def 39 :

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds Polish-WFF-args F = decomp ((Polish-WFF-set (T,A)),(Polish-arity F),((T,A) -tail F));

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A holds Polish-WFF-args F = decomp ((Polish-WFF-set (T,A)),(Polish-arity F),((T,A) -tail F));

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,(n + 1));

decomp ((Polish-expression-hierarchy (T,A,n)),(Polish-arity F),((T,A) -tail F)) is FinSequence of Polish-expression-hierarchy (T,A,n) ;

end;
let A be Polish-arity-function of T;

let n be Nat;

let F be Element of Polish-expression-hierarchy (T,A,(n + 1));

func Polish-WFF-args F -> FinSequence of Polish-expression-hierarchy (T,A,n) equals :: POLNOT_1:def 40

decomp ((Polish-expression-hierarchy (T,A,n)),(Polish-arity F),((T,A) -tail F));

coherence decomp ((Polish-expression-hierarchy (T,A,n)),(Polish-arity F),((T,A) -tail F));

decomp ((Polish-expression-hierarchy (T,A,n)),(Polish-arity F),((T,A) -tail F)) is FinSequence of Polish-expression-hierarchy (T,A,n) ;

:: deftheorem defines Polish-WFF-args POLNOT_1:def 40 :

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds Polish-WFF-args F = decomp ((Polish-expression-hierarchy (T,A,n)),(Polish-arity F),((T,A) -tail F));

for T being Polish-language

for A being Polish-arity-function of T

for n being Nat

for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds Polish-WFF-args F = decomp ((Polish-expression-hierarchy (T,A,n)),(Polish-arity F),((T,A) -tail F));

theorem Th65: :: POLNOT_1:70

for T being Polish-language

for A being Polish-arity-function of T

for t being Element of T

for u being FinSequence st u in (Polish-WFF-set (T,A)) ^^ (A . t) holds

T -tail ((Polish-operation (T,A,t)) . u) = u

for A being Polish-arity-function of T

for t being Element of T

for u being FinSequence st u in (Polish-WFF-set (T,A)) ^^ (A . t) holds

T -tail ((Polish-operation (T,A,t)) . u) = u

proof end;

theorem Th67: :: POLNOT_1:71

for T being Polish-language

for A being Polish-arity-function of T

for F being Polish-WFF of T,A

for n being Nat st F in Polish-expression-hierarchy (T,A,(n + 1)) holds

rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n)

for A being Polish-arity-function of T

for F being Polish-WFF of T,A

for n being Nat st F in Polish-expression-hierarchy (T,A,(n + 1)) holds

rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n)

proof end;

theorem Th68: :: POLNOT_1:72

for Y, Z being set

for D being non empty set

for p being FinSequence

for f being Function of Y,D

for g being Function of Z,D st rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds

f . a = g . a ) holds

f * p = g * p

for D being non empty set

for p being FinSequence

for f being Function of Y,D

for g being Function of Z,D st rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds

f . a = g . a ) holds

f * p = g * p

proof end;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let D be non empty set ;

{ [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } is Subset of [:T,(D *):]

end;
let A be Polish-arity-function of T;

let D be non empty set ;

func Polish-recursion-domain (A,D) -> Subset of [:T,(D *):] equals :: POLNOT_1:def 41

{ [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ;

coherence { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ;

{ [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } is Subset of [:T,(D *):]

proof end;

:: deftheorem defines Polish-recursion-domain POLNOT_1:def 41 :

for T being Polish-language

for A being Polish-arity-function of T

for D being non empty set holds Polish-recursion-domain (A,D) = { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ;

for T being Polish-language

for A being Polish-arity-function of T

for D being non empty set holds Polish-recursion-domain (A,D) = { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let D be non empty set ;

mode Polish-recursion-function of A,D is Function of (Polish-recursion-domain (A,D)),D;

end;
let A be Polish-arity-function of T;

let D be non empty set ;

mode Polish-recursion-function of A,D is Function of (Polish-recursion-domain (A,D)),D;

definition

let T be Polish-language;

let A be Polish-arity-function of T;

let D be non empty set ;

let f be Polish-recursion-function of A,D;

let K be Function of (Polish-WFF-set (T,A)),D;

end;
let A be Polish-arity-function of T;

let D be non empty set ;

let f be Polish-recursion-function of A,D;

let K be Function of (Polish-WFF-set (T,A)),D;

attr K is f -recursive means :: POLNOT_1:def 42

for F being Polish-WFF of T,A holds K . F = f . [(T -head F),(K * (Polish-WFF-args F))];

for F being Polish-WFF of T,A holds K . F = f . [(T -head F),(K * (Polish-WFF-args F))];

:: deftheorem defines -recursive POLNOT_1:def 42 :

for T being Polish-language

for A being Polish-arity-function of T

for D being non empty set

for f being Polish-recursion-function of A,D

for K being Function of (Polish-WFF-set (T,A)),D holds

( K is f -recursive iff for F being Polish-WFF of T,A holds K . F = f . [(T -head F),(K * (Polish-WFF-args F))] );

for T being Polish-language

for A being Polish-arity-function of T

for D being non empty set

for f being Polish-recursion-function of A,D

for K being Function of (Polish-WFF-set (T,A)),D holds

( K is f -recursive iff for F being Polish-WFF of T,A holds K . F = f . [(T -head F),(K * (Polish-WFF-args F))] );

Lm71: for T being Polish-language

for A being Polish-arity-function of T

for D being non empty set

for f being Polish-recursion-function of A,D

for K1, K2 being Function of (Polish-WFF-set (T,A)),D

for F being Polish-WFF of T,A st K1 is f -recursive & K2 is f -recursive & F in Polish-atoms (T,A) holds

K1 . F = K2 . F

proof end;

theorem Th72: :: POLNOT_1:73

for T being Polish-language

for A being Polish-arity-function of T

for D being non empty set

for f being Polish-recursion-function of A,D

for K1, K2 being Function of (Polish-WFF-set (T,A)),D st K1 is f -recursive & K2 is f -recursive holds

K1 = K2

for A being Polish-arity-function of T

for D being non empty set

for f being Polish-recursion-function of A,D

for K1, K2 being Function of (Polish-WFF-set (T,A)),D st K1 is f -recursive & K2 is f -recursive holds

K1 = K2

proof end;

definition

let L be non trivial Polish-language;

let E be Polish-arity-function of L;

let D be non empty set ;

let g be Polish-recursion-function of E,D;

let J be Subset of (Polish-WFF-set (L,E));

let H be Function of J,D;

end;
let E be Polish-arity-function of L;

let D be non empty set ;

let g be Polish-recursion-function of E,D;

let J be Subset of (Polish-WFF-set (L,E));

let H be Function of J,D;

attr H is g -recursive means :: POLNOT_1:def 43

for F being Polish-WFF of L,E st F in J & rng (Polish-WFF-args F) c= J holds

H . F = g . [(L -head F),(H * (Polish-WFF-args F))];

for F being Polish-WFF of L,E st F in J & rng (Polish-WFF-args F) c= J holds

H . F = g . [(L -head F),(H * (Polish-WFF-args F))];

:: deftheorem defines -recursive POLNOT_1:def 43 :

for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D holds

( H is g -recursive iff for F being Polish-WFF of L,E st F in J & rng (Polish-WFF-args F) c= J holds

H . F = g . [(L -head F),(H * (Polish-WFF-args F))] );

for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D holds

( H is g -recursive iff for F being Polish-WFF of L,E st F in J & rng (Polish-WFF-args F) c= J holds

H . F = g . [(L -head F),(H * (Polish-WFF-args F))] );

Lm72: for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st

( J = Polish-expression-hierarchy (L,E,0) & H is g -recursive )

proof end;

Lm73: for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for n being Nat

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D

for J1 being Subset of (Polish-WFF-set (L,E))

for H1 being Function of J1,D st J = Polish-expression-hierarchy (L,E,n) & J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H is g -recursive & ( for F being Polish-WFF of L,E st F in J1 holds

H1 . F = g . [(L -head F),(H * (Polish-WFF-args F))] ) holds

H1 is g -recursive

proof end;

Lm74: for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for n being Nat

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D

for J1 being Subset of (Polish-WFF-set (L,E))

for H1 being Function of J1,D

for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds

H . a = H1 . a

proof end;

Lm75: for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for n being Nat

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive holds

ex J1 being Subset of (Polish-WFF-set (L,E)) ex H1 being Function of J1,D st

( J1 = Polish-expression-hierarchy (L,E,(n + 1)) & H1 is g -recursive )

proof end;

theorem Th75: :: POLNOT_1:74

for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st

( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st

( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )

proof end;

Lm79: for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for n being Nat

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D

for m being Nat

for J1 being Subset of (Polish-WFF-set (L,E))

for H1 being Function of J1,D

for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,(n + m)) & H1 is g -recursive & a in J holds

H . a = H1 . a

by Th34, Lm74;

Lm80: for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for n being Nat

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D

for m being Nat

for J1 being Subset of (Polish-WFF-set (L,E))

for H1 being Function of J1,D

for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J1 = Polish-expression-hierarchy (L,E,m) & H1 is g -recursive & a in J & a in J1 holds

H . a = H1 . a

proof end;

Lm82: for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for J being Subset of (Polish-WFF-set (L,E))

for H being Function of J,D st ( for a being object st a in J holds

ex n being Nat ex J1 being Subset of (Polish-WFF-set (L,E)) ex H1 being Function of J1,D st

( J1 = Polish-expression-hierarchy (L,E,n) & H1 is g -recursive & a in J1 & H . a = H1 . a ) ) holds

H is g -recursive

proof end;

theorem Th77: :: POLNOT_1:75

for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D ex K being Function of (Polish-WFF-set (L,E)),D st K is g -recursive

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D ex K being Function of (Polish-WFF-set (L,E)),D st K is g -recursive

proof end;

theorem :: POLNOT_1:76

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t being Element of L holds Polish-operation (L,E,t) is one-to-one

for E being Polish-arity-function of L

for t being Element of L holds Polish-operation (L,E,t) is one-to-one

proof end;

theorem :: POLNOT_1:77

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t, u being Element of L st rng (Polish-operation (L,E,t)) meets rng (Polish-operation (L,E,u)) holds

t = u

for E being Polish-arity-function of L

for t, u being Element of L st rng (Polish-operation (L,E,t)) meets rng (Polish-operation (L,E,u)) holds

t = u

proof end;

theorem :: POLNOT_1:78

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t being Element of L

for a being object st a in dom (Polish-operation (L,E,t)) holds

ex p being FinSequence st

( p = (Polish-operation (L,E,t)) . a & L -head p = t )

for E being Polish-arity-function of L

for t being Element of L

for a being object st a in dom (Polish-operation (L,E,t)) holds

ex p being FinSequence st

( p = (Polish-operation (L,E,t)) . a & L -head p = t )

proof end;

theorem Th91: :: POLNOT_1:79

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t being Element of L

for F being Polish-WFF of L,E holds

( Polish-WFF-head F = t iff ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u )

for E being Polish-arity-function of L

for t being Element of L

for F being Polish-WFF of L,E holds

( Polish-WFF-head F = t iff ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u )

proof end;

theorem :: POLNOT_1:80

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t being Element of L st E . t = 1 holds

for F being Polish-WFF of L,E st Polish-WFF-head F = t holds

ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G

for E being Polish-arity-function of L

for t being Element of L st E . t = 1 holds

for F being Polish-WFF of L,E st Polish-WFF-head F = t holds

ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G

proof end;

theorem Th93: :: POLNOT_1:81

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t being Element of L st E . t = 1 holds

for F being Polish-WFF of L,E holds

( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> )

for E being Polish-arity-function of L

for t being Element of L st E . t = 1 holds

for F being Polish-WFF of L,E holds

( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> )

proof end;

theorem :: POLNOT_1:82

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t being Element of L st E . t = 2 holds

for F being Polish-WFF of L,E st Polish-WFF-head F = t holds

ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H)

for E being Polish-arity-function of L

for t being Element of L st E . t = 2 holds

for F being Polish-WFF of L,E st Polish-WFF-head F = t holds

ex G, H being Polish-WFF of L,E st F = (Polish-binOp (L,E,t)) . (G,H)

proof end;

theorem :: POLNOT_1:83

for L being non trivial Polish-language

for E being Polish-arity-function of L

for t being Element of L st E . t = 2 holds

for F, G being Polish-WFF of L,E holds

( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> )

for E being Polish-arity-function of L

for t being Element of L st E . t = 2 holds

for F, G being Polish-WFF of L,E holds

( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> )

proof end;

theorem :: POLNOT_1:84

for L being non trivial Polish-language

for E being Polish-arity-function of L

for F being Polish-WFF of L,E holds

( F in Polish-atoms (L,E) iff Polish-arity F = 0 )

for E being Polish-arity-function of L

for F being Polish-WFF of L,E holds

( F in Polish-atoms (L,E) iff Polish-arity F = 0 )

proof end;

theorem :: POLNOT_1:85

for L being non trivial Polish-language

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for K being Function of (Polish-WFF-set (L,E)),D

for t being Element of L

for F being Polish-WFF of L,E st K is g -recursive & E . t = 1 holds

K . ((Polish-unOp (L,E,t)) . F) = g . (t,<*(K . F)*>)

for E being Polish-arity-function of L

for D being non empty set

for g being Polish-recursion-function of E,D

for K being Function of (Polish-WFF-set (L,E)),D

for t being Element of L

for F being Polish-WFF of L,E st K is g -recursive & E . t = 1 holds

K . ((Polish-unOp (L,E,t)) . F) = g . (t,<*(K . F)*>)

proof end;

definition

let S be Polish-language;

let p be FinSequence of S;

ex b_{1} being Element of S ^^ (len p) st decomp (S,(len p),b_{1}) = p

for b_{1}, b_{2} being Element of S ^^ (len p) st decomp (S,(len p),b_{1}) = p & decomp (S,(len p),b_{2}) = p holds

b_{1} = b_{2}

end;
let p be FinSequence of S;

func FlattenSeq p -> Element of S ^^ (len p) means :Def102: :: POLNOT_1:def 44

decomp (S,(len p),it) = p;

existence decomp (S,(len p),it) = p;

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def102 defines FlattenSeq POLNOT_1:def 44 :

for S being Polish-language

for p being FinSequence of S

for b_{3} being Element of S ^^ (len p) holds

( b_{3} = FlattenSeq p iff decomp (S,(len p),b_{3}) = p );

for S being Polish-language

for p being FinSequence of S

for b

( b

definition

let L be non trivial Polish-language;

let E be Polish-arity-function of L;

mode Substitution of L,E is PartFunc of (Polish-atoms (L,E)),(Polish-WFF-set (L,E));

end;
let E be Polish-arity-function of L;

mode Substitution of L,E is PartFunc of (Polish-atoms (L,E)),(Polish-WFF-set (L,E));

definition

let L be non trivial Polish-language;

let E be Polish-arity-function of L;

let s be Substitution of L,E;

ex b_{1} being Polish-recursion-function of E,(Polish-WFF-set (L,E)) st

for t being Element of L

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b_{1} . (t,p) = s . t ) & ( not t in dom s implies b_{1} . (t,p) = t ^ (FlattenSeq p) ) )

for b_{1}, b_{2} being Polish-recursion-function of E,(Polish-WFF-set (L,E)) st ( for t being Element of L

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b_{1} . (t,p) = s . t ) & ( not t in dom s implies b_{1} . (t,p) = t ^ (FlattenSeq p) ) ) ) & ( for t being Element of L

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b_{2} . (t,p) = s . t ) & ( not t in dom s implies b_{2} . (t,p) = t ^ (FlattenSeq p) ) ) ) holds

b_{1} = b_{2}

end;
let E be Polish-arity-function of L;

let s be Substitution of L,E;

func Subst s -> Polish-recursion-function of E,(Polish-WFF-set (L,E)) means :Def103: :: POLNOT_1:def 45

for t being Element of L

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies it . (t,p) = s . t ) & ( not t in dom s implies it . (t,p) = t ^ (FlattenSeq p) ) );

existence for t being Element of L

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies it . (t,p) = s . t ) & ( not t in dom s implies it . (t,p) = t ^ (FlattenSeq p) ) );

ex b

for t being Element of L

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b

proof end;

uniqueness for b

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b

b

proof end;

:: deftheorem Def103 defines Subst POLNOT_1:def 45 :

for L being non trivial Polish-language

for E being Polish-arity-function of L

for s being Substitution of L,E

for b_{4} being Polish-recursion-function of E,(Polish-WFF-set (L,E)) holds

( b_{4} = Subst s iff for t being Element of L

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b_{4} . (t,p) = s . t ) & ( not t in dom s implies b_{4} . (t,p) = t ^ (FlattenSeq p) ) ) );

for L being non trivial Polish-language

for E being Polish-arity-function of L

for s being Substitution of L,E

for b

( b

for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds

( ( t in dom s implies b

definition

let L be non trivial Polish-language;

let E be Polish-arity-function of L;

let s be Substitution of L,E;

let F be Polish-WFF of L,E;

ex b_{1} being Polish-WFF of L,E ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st

( H is Subst s -recursive & b_{1} = H . F )

for b_{1}, b_{2} being Polish-WFF of L,E st ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st

( H is Subst s -recursive & b_{1} = H . F ) & ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st

( H is Subst s -recursive & b_{2} = H . F ) holds

b_{1} = b_{2}
by Th72;

end;
let E be Polish-arity-function of L;

let s be Substitution of L,E;

let F be Polish-WFF of L,E;

func Subst (s,F) -> Polish-WFF of L,E means :Def104: :: POLNOT_1:def 46

ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st

( H is Subst s -recursive & it = H . F );

existence ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st

( H is Subst s -recursive & it = H . F );

ex b

( H is Subst s -recursive & b

proof end;

uniqueness for b

( H is Subst s -recursive & b

( H is Subst s -recursive & b

b

:: deftheorem Def104 defines Subst POLNOT_1:def 46 :

for L being non trivial Polish-language

for E being Polish-arity-function of L

for s being Substitution of L,E

for F, b_{5} being Polish-WFF of L,E holds

( b_{5} = Subst (s,F) iff ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st

( H is Subst s -recursive & b_{5} = H . F ) );

for L being non trivial Polish-language

for E being Polish-arity-function of L

for s being Substitution of L,E

for F, b

( b

( H is Subst s -recursive & b

theorem :: POLNOT_1:86

for L being non trivial Polish-language

for E being Polish-arity-function of L

for s being Substitution of L,E

for F being Polish-WFF of L,E st s = {} holds

Subst (s,F) = F

for E being Polish-arity-function of L

for s being Substitution of L,E

for F being Polish-WFF of L,E st s = {} holds

Subst (s,F) = F

proof end;

:: String and Set Operations for Polish Notation

::