:: Polish Notation
:: by Taneli Huuskonen
::
:: Received April 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


::
:: String and Set Operations for Polish Notation
::
definition
let D be non empty set ;
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 ) } is Subset of (D *)
proof end;
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 ) } ;

definition
let P, Q be FinSequence-membered set ;
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
ex b1 being FinSequence-membered set st
for a being object holds
( a in b1 iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) )
proof end;
uniqueness
for b1, b2 being FinSequence-membered set st ( for a being object holds
( a in b1 iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) ) & ( for a being object holds
( a in b2 iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ^ POLNOT_1:def 2 :
for P, Q, b3 being FinSequence-membered set holds
( b3 = P ^ Q iff for a being object holds
( a in b3 iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) );

registration
let E be empty set ;
let P be FinSequence-membered set ;
cluster E ^ P -> empty FinSequence-membered ;
coherence
E ^ P is empty
proof end;
cluster P ^ E -> empty FinSequence-membered ;
coherence
P ^ E is empty
proof end;
end;

registration
let S, T be non empty FinSequence-membered set ;
cluster S ^ T -> non empty FinSequence-membered ;
coherence
not S ^ T is empty
proof end;
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 )
proof end;

theorem Th2: :: POLNOT_1:2
for P, Q, R being FinSequence-membered set holds (P ^ Q) ^ R = P ^ (Q ^ R)
proof end;

registration
cluster {{}} -> non empty FinSequence-membered ;
coherence
( not {{}} is empty & {{}} is FinSequence-membered )
by TARSKI:def 1;
end;

theorem Th3: :: POLNOT_1:3
for P being FinSequence-membered set holds
( P ^ {{}} = P & {{}} ^ P = P )
proof end;

definition
let P be FinSequence-membered set ;
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
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b1 . n & b1 . (n + 1) = Q ^ P ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b1 . n & b1 . (n + 1) = Q ^ P ) ) & dom b2 = NAT & b2 . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b2 . n & b2 . (n + 1) = Q ^ P ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ^^ POLNOT_1:def 3 :
for P being FinSequence-membered set
for b2 being Function holds
( b2 = P ^^ iff ( dom b2 = NAT & b2 . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b2 . n & b2 . (n + 1) = Q ^ P ) ) ) );

definition
let P be FinSequence-membered set ;
let n be Nat;
func P ^^ n -> FinSequence-membered set equals :: POLNOT_1:def 4
(P ^^) . n;
coherence
(P ^^) . n is FinSequence-membered set
proof end;
end;

:: deftheorem defines ^^ POLNOT_1:def 4 :
for P being FinSequence-membered set
for n being Nat holds P ^^ n = (P ^^) . n;

theorem Th4: :: POLNOT_1:4
for P being FinSequence-membered set holds {} in P ^^ 0
proof end;

registration
let P be FinSequence-membered set ;
let n be zero Nat;
cluster P ^^ n -> non empty FinSequence-membered ;
coherence
not P ^^ n is empty
by Th4;
end;

registration
let E be empty set ;
let n be non zero Nat;
cluster E ^^ n -> empty FinSequence-membered ;
coherence
E ^^ n is empty
proof end;
end;

definition
let P be FinSequence-membered set ;
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 } is non empty FinSequence-membered set
proof end;
end;

:: deftheorem defines * POLNOT_1:def 5 :
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 )
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 ) )
proof end;

theorem Th8: :: POLNOT_1:7
for P being FinSequence-membered set holds P ^^ 1 = P
proof end;

theorem Th9: :: POLNOT_1:8
for P being FinSequence-membered set
for n being Nat holds P ^^ n c= P * by Th6;

theorem Th10: :: POLNOT_1:9
for P being FinSequence-membered set holds
( {} in P * & P c= P * )
proof end;

theorem Th11: :: POLNOT_1:10
for P being FinSequence-membered set
for m, n being Nat holds P ^^ (m + n) = (P ^^ m) ^ (P ^^ n)
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)
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 *
proof end;

theorem Th14: :: POLNOT_1:13
for P, Q, R being FinSequence-membered set st P c= R * & Q c= R * holds
P ^ Q c= R *
proof end;

theorem Th15: :: POLNOT_1:14
for P, Q being FinSequence-membered set
for n being Nat st Q c= P * holds
Q ^^ n c= P *
proof end;

theorem :: POLNOT_1:15
for P, Q being FinSequence-membered set st Q c= P * holds
Q * c= P *
proof end;

theorem Th17: :: POLNOT_1:16
for P1, P2, Q1, Q2 being FinSequence-membered set st P1 c= P2 & Q1 c= Q2 holds
P1 ^ Q1 c= P2 ^ Q2
proof end;

theorem TH18: :: POLNOT_1:17
for P, Q being FinSequence-membered set st P c= Q holds
for n being Nat holds P ^^ n c= Q ^^ n
proof end;

registration
let S be non empty FinSequence-membered set ;
let n be Nat;
cluster S ^^ n -> non empty FinSequence-membered ;
coherence
( not S ^^ n is empty & S ^^ n is FinSequence-membered )
proof end;
end;

definition
let P be FinSequence-membered set ;
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
ex b1 being Subset of (P *) st
for a being object holds
( a in b1 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 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (P *) st ( for a being object holds
( a in b1 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 b2 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
b1 = b2
proof end;
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, b4 being Subset of (P *) holds
( b4 = Polish-expression-layer (P,A,U) iff for a being object holds
( a in b4 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 ) ) ) );

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

definition
let P be FinSequence-membered set ;
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
ex b1 being Subset of (P *) st
for a being object holds
( a in b1 iff ( a in P & A . a = 0 ) )
proof end;
uniqueness
for b1, b2 being Subset of (P *) st ( for a being object holds
( a in b1 iff ( a in P & A . a = 0 ) ) ) & ( for a being object holds
( a in b2 iff ( a in P & A . a = 0 ) ) ) holds
b1 = b2
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 ) } is Subset of P
proof end;
end;

:: deftheorem Def9 defines Polish-atoms POLNOT_1:def 7 :
for P being FinSequence-membered set
for A being Function of P,NAT
for b3 being Subset of (P *) holds
( b3 = Polish-atoms (P,A) iff for a being object holds
( a in b3 iff ( a in P & A . a = 0 ) ) );

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

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

definition
let P be FinSequence-membered set ;
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
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b1 . n & b1 . (n + 1) = Polish-expression-layer (P,A,U) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b1 . n & b1 . (n + 1) = Polish-expression-layer (P,A,U) ) ) & dom b2 = NAT & b2 . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b2 . n & b2 . (n + 1) = Polish-expression-layer (P,A,U) ) ) holds
b1 = b2
proof end;
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 b3 being Function holds
( b3 = Polish-expression-hierarchy (P,A) iff ( dom b3 = NAT & b3 . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b3 . n & b3 . (n + 1) = Polish-expression-layer (P,A,U) ) ) ) );

definition
let P be FinSequence-membered set ;
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 is Subset of (P *)
proof end;
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;

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;

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

definition
let P be FinSequence-membered set ;
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 } is Subset of (P *)
proof end;
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 } ;

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

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 ;
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
ex b1 being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) st
for q being FinSequence st q in dom b1 holds
b1 . q = t ^ q
proof end;
uniqueness
for b1, b2 being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) st ( for q being FinSequence st q in dom b1 holds
b1 . q = t ^ q ) & ( for q being FinSequence st q in dom b2 holds
b2 . q = t ^ q ) holds
b1 = b2
proof end;
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 b5 being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) holds
( b5 = Polish-operation (P,A,n,t) iff for q being FinSequence st q in dom b5 holds
b5 . q = t ^ q );

definition
let X, Y be set ;
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
( 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;
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 );

registration
let X be set ;
cluster Relation-like NAT -defined bool X -valued Function-like V38() FinSequence-like FinSubsequence-like V107() for FinSequence of bool X;
existence
not for b1 being FinSequence of bool X holds b1 is V107()
proof end;
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 )
proof end;

definition
let X be set ;
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
ex b1 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 . (b1 . a) ) or ( ( for n being Nat holds not a in B . n ) & b1 . a = 0 ) )
proof end;
uniqueness
for b1, b2 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 . (b1 . a) ) or ( ( for n being Nat holds not a in B . n ) & b1 . a = 0 ) ) ) & ( for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (b2 . a) ) or ( ( for n being Nat holds not a in B . n ) & b2 . a = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines arity-from-list POLNOT_1:def 14 :
for X being set
for B being V107() FinSequence of bool X
for b3 being Function of X,NAT holds
( b3 = 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 . (b3 . a) ) or ( ( for n being Nat holds not a in B . n ) & b3 . a = 0 ) ) );

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

definition
let P be FinSequence-membered set ;
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;
end;

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

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

scheme :: POLNOT_1:sch 1
AInd{ F1() -> FinSequence-membered set , F2() -> Function of F1(),NAT, P1[ object ] } :
for a being object st a in Polish-expression-set (F1(),F2()) holds
P1[a]
provided
A1: for p, q being FinSequence
for n being Nat st p in F1() & n = F2() . p & q in (Polish-expression-set (F1(),F2())) ^^ n holds
P1[p ^ q]
proof end;

definition
let P be FinSequence-membered set ;
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 = {} ;
end;

:: 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 = {} );

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

theorem TH2: :: POLNOT_1:41
for P, Q being FinSequence-membered set st P c= Q & Q is antichain-like holds
P is antichain-like ;

registration
cluster trivial FinSequence-membered -> FinSequence-membered antichain-like for set ;
coherence
for b1 being FinSequence-membered set st b1 is trivial holds
b1 is antichain-like
proof end;
end;

theorem :: POLNOT_1:42
for P being FinSequence-membered set
for a being object st P = {a} holds
P is antichain-like ;

registration
cluster functional non empty FinSequence-membered antichain-like for set ;
existence
ex b1 being non empty FinSequence-membered set st b1 is antichain-like
proof end;
cluster empty FinSequence-membered -> FinSequence-membered antichain-like for set ;
coherence
for b1 being FinSequence-membered set st b1 is empty holds
b1 is antichain-like
;
end;

definition
mode antichain is FinSequence-membered antichain-like set ;
end;

registration
let B be antichain;
cluster -> FinSequence-membered antichain-like for Element of bool B;
coherence
for b1 being Subset of B holds
( b1 is antichain-like & b1 is FinSequence-membered )
by TH2;
end;

definition
mode Polish-language is non empty antichain;
end;

definition
let D be non empty set ;
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
( 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;
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 );

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

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

registration
let B, C be antichain;
cluster B ^ C -> FinSequence-membered antichain-like ;
coherence
B ^ C is antichain-like
by Th5;
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
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
proof end;

theorem TH8: :: POLNOT_1:46
for B being antichain st {} in B holds
B = {{}}
proof end;

registration
let B be antichain;
let n be Nat;
cluster B ^^ n -> FinSequence-membered antichain-like ;
coherence
B ^^ n is antichain-like
proof end;
end;

registration
let T be Polish-language;
cluster functional non empty FinSequence-membered antichain-like for Element of bool (T *);
existence
ex b1 being Subset of (T *) st
( not b1 is empty & b1 is antichain-like )
proof end;
let n be Nat;
cluster T ^^ n -> non empty FinSequence-membered ;
coherence
not T ^^ n is empty
;
end;

definition
let T be Polish-language;
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 b1 being Function of T,NAT ex a being object st
( a in T & b1 . a = 0 )
proof end;
end;

:: deftheorem Def5 defines Polish-arity-function POLNOT_1:def 18 :
for T being Polish-language
for b2 being Function of T,NAT holds
( b2 is Polish-arity-function of T iff ex a being object st
( a in T & b2 . a = 0 ) );

registration
let T be Polish-language;
cluster non empty antichain-like -> FinSequence-membered for Element of bool (T *);
coherence
for b1 being Polish-language of T holds
( not b1 is empty & b1 is antichain-like & b1 is FinSequence-membered )
;
end;

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;

definition
let T be Polish-language;
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 b1 being Subset of (T *) holds
( b1 = Polish-expression-layer (T,A,U) iff for a being object holds
( a in b1 iff ex t being Element of T ex u being Element of T * st
( a = t ^ u & u in U ^^ (A . t) ) ) )
proof end;
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 b4 being Subset of (T *) holds
( b4 = Polish-expression-layer (T,A,U) iff for a being object holds
( a in b4 iff ex t being Element of T ex u being Element of T * st
( a = t ^ u & u in U ^^ (A . t) ) ) );

definition
let B be antichain;
let p be FinSequence;
attr p is B -headed means :: POLNOT_1:def 20
ex q, r being FinSequence st
( q in B & p = q ^ r );
end;

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

definition
let B be antichain;
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 ;
end;

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

theorem Th11a: :: POLNOT_1:47
for B, C being antichain
for p being FinSequence st p is B -headed & B c= C holds
p is C -headed ;

theorem :: POLNOT_1:48
for B, C being antichain
for P being FinSequence-membered set st P is B -headed & B c= C holds
P is C -headed by Th11a;

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

proof end;

registration
let B be antichain;
let P be FinSequence-membered set ;
cluster B ^ P -> FinSequence-membered B -headed ;
coherence
B ^ P is B -headed
by Th13;
end;

theorem :: POLNOT_1:49
for B, C being antichain
for p being FinSequence st p is B ^ C -headed holds
p is B -headed
proof end;

theorem Th15: :: POLNOT_1:50
for B being antichain holds B is B -headed
proof end;

registration
let B be antichain;
cluster functional FinSequence-membered B -headed for set ;
existence
ex b1 being FinSequence-membered set st b1 is B -headed
proof end;
end;

registration
let B be antichain;
let P be FinSequence-membered B -headed set ;
cluster -> B -headed for Element of bool P;
coherence
for b1 being Subset of P holds b1 is B -headed
by Def8;
end;

registration
let S be Polish-language;
cluster functional non empty FinSequence-membered S -headed for set ;
existence
ex b1 being FinSequence-membered set st
( not b1 is empty & b1 is S -headed )
proof end;
end;

theorem Th16: :: POLNOT_1:51
for S being Polish-language
for m, n being Nat holds S ^^ (m + n) is S ^^ m -headed
proof end;

definition
let S be Polish-language;
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
for b1 being FinSequence holds verum
;
existence
( ( p is S -headed implies ex b1 being FinSequence st
( b1 in S & ex r being FinSequence st p = b1 ^ r ) ) & ( not p is S -headed implies ex b1 being FinSequence st b1 = {} ) )
;
uniqueness
for b1, b2 being FinSequence holds
( ( p is S -headed & b1 in S & ex r being FinSequence st p = b1 ^ r & b2 in S & ex r being FinSequence st p = b2 ^ r implies b1 = b2 ) & ( not p is S -headed & b1 = {} & b2 = {} implies b1 = b2 ) )
by TH4;
end;

:: deftheorem Def9a defines -head POLNOT_1:def 22 :
for S being Polish-language
for p, b3 being FinSequence holds
( ( p is S -headed implies ( b3 = S -head p iff ( b3 in S & ex r being FinSequence st p = b3 ^ r ) ) ) & ( not p is S -headed implies ( b3 = S -head p iff b3 = {} ) ) );

definition
let S be Polish-language;
let p be FinSequence;
func S -tail p -> FinSequence means :Def10: :: POLNOT_1:def 23
p = (S -head p) ^ it;
existence
ex b1 being FinSequence st p = (S -head p) ^ b1
proof end;
uniqueness
for b1, b2 being FinSequence st p = (S -head p) ^ b1 & p = (S -head p) ^ b2 holds
b1 = b2
by FINSEQ_1:33;
end;

:: deftheorem Def10 defines -tail POLNOT_1:def 23 :
for S being Polish-language
for p, b3 being FinSequence holds
( b3 = S -tail p iff p = (S -head p) ^ b3 );

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 )
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 = {} )
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 )
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 )
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 )
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 )
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 )
proof end;

registration
let T be Polish-language;
let A be Polish-arity-function of T;
cluster Polish-atoms (T,A) -> non empty antichain-like ;
coherence
( not Polish-atoms (T,A) is empty & Polish-atoms (T,A) is antichain-like )
proof end;
let U be Polish-language of T;
cluster Polish-expression-layer (T,A,U) -> non empty antichain-like ;
coherence
( not Polish-expression-layer (T,A,U) is empty & Polish-expression-layer (T,A,U) is antichain-like )
proof end;
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;

definition
let T be Polish-language;
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 } is Subset of T
proof end;
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 } ;

registration
let T be Polish-language;
let A be Polish-arity-function of T;
let n be Nat;
cluster Polish-expression-hierarchy (T,A,n) -> non empty antichain-like ;
coherence
( Polish-expression-hierarchy (T,A,n) is antichain-like & not Polish-expression-hierarchy (T,A,n) is empty )
proof end;
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;

definition
let T be Polish-language;
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) is Polish-language of T
proof end;
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);

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;

definition
let T be Polish-language;
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) is Function of ((Polish-WFF-set (T,A)) ^^ (A . t)),(Polish-WFF-set (T,A))
proof end;
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);

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 ;
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) is UnOp of (Polish-WFF-set (T,A))
proof end;
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);

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 ;
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
ex b1 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
b1 . (u,v) = (Polish-operation (T,A,t)) . (u ^ v)
proof end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ) holds
b1 = b2
proof end;
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 b4 being BinOp of (Polish-WFF-set (T,A)) holds
( b4 = 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
b4 . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) );

definition
let X, Y be set ;
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 );
end;

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

registration
let X be non empty set ;
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 b1 being FinSequence of bool X st
( not b1 is exhaustive & b1 is V107() )
proof end;
end;

theorem TH37: :: POLNOT_1:59
for X, Y being set
for F being PartFunc of X,(bool Y) holds
( not F is exhaustive iff ex a being object st
( a in Y & ( for b being object st b in dom F holds
not a in F . b ) ) ) ;

definition
let T be Polish-language;
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 is Polish-arity-function of T
proof end;
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;

registration
cluster functional FinSequence-membered with_non-empty_elements antichain-like for set ;
existence
ex b1 being FinSequence-membered antichain-like set st b1 is with_non-empty_elements
proof end;
cluster functional non empty non trivial FinSequence-membered antichain-like for set ;
existence
not for b1 being Polish-language holds b1 is trivial
proof end;
end;

registration
cluster non trivial FinSequence-membered antichain-like -> FinSequence-membered with_non-empty_elements antichain-like for set ;
coherence
for b1 being FinSequence-membered antichain-like set st not b1 is trivial holds
b1 is with_non-empty_elements
by TH8, SETFAM_1:def 8;
end;

definition
let S be Polish-language;
let n, m be Nat;
let p be Element of S ^^ ((n + 1) + m);
func decomp (S,n,m,p) -> Element of S equals :: POLNOT_1:def 31
S -head ((S ^^ n) -tail p);
coherence
S -head ((S ^^ n) -tail p) is Element of S
proof end;
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);

definition
let S be Polish-language;
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
ex b1 being FinSequence of S st
( dom b1 = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b1 . m = S -head ((S ^^ k) -tail p) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of S st dom b1 = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b1 . m = S -head ((S ^^ k) -tail p) ) ) & dom b2 = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b2 . m = S -head ((S ^^ k) -tail p) ) ) holds
b1 = b2
proof end;
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 b4 being FinSequence of S holds
( b4 = decomp (S,n,p) iff ( dom b4 = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b4 . m = S -head ((S ^^ k) -tail p) ) ) ) );

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

theorem Th51: :: POLNOT_1:61
for S being Polish-language
for q being Element of S ^^ 0 holds decomp (S,0,q) = {}
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
proof end;

theorem TH55: :: POLNOT_1:63
for S being Polish-language
for q being Element of S ^^ 1 holds decomp (S,1,q) = <*q*>
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*>
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
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
proof end;

definition
let T be Polish-language;
let A be Polish-arity-function of T;
let F be Polish-WFF of T,A;
func Polish-WFF-head F -> Element of T equals :: POLNOT_1:def 33
T -head F;
coherence
T -head F is Element of T
proof end;
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;

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);
func Polish-WFF-head F -> Element of T equals :: POLNOT_1:def 34
T -head F;
coherence
T -head F is Element of T
proof end;
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;

definition
let T be Polish-language;
let A be Polish-arity-function of T;
let F be Polish-WFF of T,A;
func Polish-arity F -> Nat equals :: POLNOT_1:def 35
A . (Polish-WFF-head F);
coherence
A . (Polish-WFF-head F) is Nat
;
end;

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

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);
func Polish-arity F -> Nat equals :: POLNOT_1:def 36
A . (Polish-WFF-head F);
coherence
A . (Polish-WFF-head F) is Nat
;
end;

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

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

definition
let T be Polish-language;
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 is Element of (Polish-WFF-set (T,A)) ^^ (Polish-arity F)
by Th62;
end;

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

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
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));
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 is Element of (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F)
by Th63;
end;

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

definition
let T be Polish-language;
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)) is FinSequence of Polish-WFF-set (T,A)
;
end;

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

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));
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)) is FinSequence of Polish-expression-hierarchy (T,A,n)
;
end;

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

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

definition
let T be Polish-language;
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 } is Subset of [:T,(D *):]
proof end;
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 } ;

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;

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

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

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

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

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

definition
let S be Polish-language;
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
ex b1 being Element of S ^^ (len p) st decomp (S,(len p),b1) = p
proof end;
uniqueness
for b1, b2 being Element of S ^^ (len p) st decomp (S,(len p),b1) = p & decomp (S,(len p),b2) = p holds
b1 = b2
proof end;
end;

:: deftheorem Def102 defines FlattenSeq POLNOT_1:def 44 :
for S being Polish-language
for p being FinSequence of S
for b3 being Element of S ^^ (len p) holds
( b3 = FlattenSeq p iff decomp (S,(len p),b3) = p );

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;

definition
let L be non trivial Polish-language;
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
ex b1 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 b1 . (t,p) = s . t ) & ( not t in dom s implies b1 . (t,p) = t ^ (FlattenSeq p) ) )
proof end;
uniqueness
for b1, b2 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 b1 . (t,p) = s . t ) & ( not t in dom s implies b1 . (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 b2 . (t,p) = s . t ) & ( not t in dom s implies b2 . (t,p) = t ^ (FlattenSeq p) ) ) ) holds
b1 = b2
proof end;
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 b4 being Polish-recursion-function of E,(Polish-WFF-set (L,E)) holds
( b4 = 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 b4 . (t,p) = s . t ) & ( not t in dom s implies b4 . (t,p) = t ^ (FlattenSeq p) ) ) );

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;
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 b1 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 & b1 = H . F )
proof end;
uniqueness
for b1, b2 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 & b1 = H . F ) & ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st
( H is Subst s -recursive & b2 = H . F ) holds
b1 = b2
by Th72;
end;

:: 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, b5 being Polish-WFF of L,E holds
( b5 = 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 & b5 = H . F ) );

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