:: 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 b₁ being FinSequence-membered set st
for a being object holds
( a in b₁ iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence-membered set st ( for a being object holds
( a in b₁ iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) ) & ( for a being object holds
( a in b₂ iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ^ POLNOT_1:def 2 :
for P, Q, b₃ being FinSequence-membered set holds
( b₃ = P ^ Q iff for a being object holds
( a in b₃ 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 b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b₁ . n & b₁ . (n + 1) = Q ^ P ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & b₁ . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b₁ . n & b₁ . (n + 1) = Q ^ P ) ) & dom b₂ = NAT & b₂ . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b₂ . n & b₂ . (n + 1) = Q ^ P ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines ^^ POLNOT_1:def 3 :
for P being FinSequence-membered set
for b₂ being Function holds
( b₂ = P ^^ iff ( dom b₂ = NAT & b₂ . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b₂ . n & b₂ . (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 b₁ being Subset of (P *) st
for a being object holds
( a in b₁ 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 b₁, b₂ being Subset of (P *) st ( for a being object holds
( a in b₁ 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₂ 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₁ = b₂

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, b₄ being Subset of (P *) holds
( b₄ = Polish-expression-layer (P,A,U) iff for a being object holds
( a in b₄ 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 b₁ being Subset of (P *) st
for a being object holds
( a in b₁ iff ( a in P & A . a = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (P *) st ( for a being object holds
( a in b₁ iff ( a in P & A . a = 0 ) ) ) & ( for a being object holds
( a in b₂ iff ( a in P & A . a = 0 ) ) ) holds
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 ) } 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 b₃ being Subset of (P *) holds
( b₃ = Polish-atoms (P,A) iff for a being object holds
( a in b₃ 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 b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b₁ . n & b₁ . (n + 1) = Polish-expression-layer (P,A,U) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & b₁ . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b₁ . n & b₁ . (n + 1) = Polish-expression-layer (P,A,U) ) ) & dom b₂ = NAT & b₂ . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b₂ . n & b₂ . (n + 1) = Polish-expression-layer (P,A,U) ) ) holds
b₁ = b₂

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 b₃ being Function holds
( b₃ = Polish-expression-hierarchy (P,A) iff ( dom b₃ = NAT & b₃ . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = b₃ . n & b₃ . (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 b₁ being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) st
for q being FinSequence st q in dom b₁ holds
b₁ . q = t ^ q

proof end;

uniqueness
for b₁, b₂ being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) st ( for q being FinSequence st q in dom b₁ holds
b₁ . q = t ^ q ) & ( for q being FinSequence st q in dom b₂ holds
b₂ . q = t ^ q ) holds
b₁ = b₂

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 b₅ being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) holds
( b₅ = Polish-operation (P,A,n,t) iff for q being FinSequence st q in dom b₅ holds
b₅ . 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 b₁ being FinSequence of bool X holds b₁ 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 b₁ 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₁ . a) ) or ( ( for n being Nat holds not a in B . n ) & b₁ . a = 0 ) )

proof end;

uniqueness
for b₁, b₂ 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₁ . a) ) or ( ( for n being Nat holds not a in B . n ) & b₁ . 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₂ . a) ) or ( ( for n being Nat holds not a in B . n ) & b₂ . a = 0 ) ) ) holds
b₁ = b₂

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 b₃ being Function of X,NAT holds
( b₃ = 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₃ . a) ) or ( ( for n being Nat holds not a in B . n ) & b₃ . 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{ F₁() -> FinSequence-membered set , F₂() -> Function of F₁(),NAT, P₁[ object ] } :

for a being object st a in Polish-expression-set (F₁(),F₂()) holds
P₁[a]

provided

A1: for p, q being FinSequence
for n being Nat st p in F₁() & n = F₂() . p & q in (Polish-expression-set (F₁(),F₂())) ^^ n holds
P₁[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 b₁ being FinSequence-membered set st b₁ is trivial holds
b₁ 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 b₁ being non empty FinSequence-membered set st b₁ is antichain-like

proof end;

cluster empty FinSequence-membered -> FinSequence-membered antichain-like for set ;

coherence
for b₁ being FinSequence-membered set st b₁ is empty holds
b₁ 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 b₁ being Subset of B holds
( b₁ is antichain-like & b₁ 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 b₁ being Subset of (T *) st
( not b₁ is empty & b₁ 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 b₁ being Function of T,NAT ex a being object st
( a in T & b₁ . a = 0 )

proof end;

end;

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

registration

let T be Polish-language;

cluster non empty antichain-like -> FinSequence-membered for Element of bool (T *);

coherence
for b₁ being Polish-language of T holds
( not b₁ is empty & b₁ is antichain-like & b₁ 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 b₁ being Subset of (T *) holds
( b₁ = Polish-expression-layer (T,A,U) iff for a being object holds
( a in b₁ 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 b₄ being Subset of (T *) holds
( b₄ = Polish-expression-layer (T,A,U) iff for a being object holds
( a in b₄ 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 b₁ being FinSequence-membered set st b₁ 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 b₁ being Subset of P holds b₁ is B -headed by Def8;

end;

registration

let S be Polish-language;

cluster functional non empty FinSequence-membered S -headed for set ;

existence
ex b₁ being FinSequence-membered set st
( not b₁ is empty & b₁ 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 b₁ being FinSequence holds verum ;
existence
( ( p is S -headed implies ex b₁ being FinSequence st
( b₁ in S & ex r being FinSequence st p = b₁ ^ r ) ) & ( not p is S -headed implies ex b₁ being FinSequence st b₁ = {} ) ) ;
uniqueness
for b₁, b₂ being FinSequence holds
( ( p is S -headed & b₁ in S & ex r being FinSequence st p = b₁ ^ r & b₂ in S & ex r being FinSequence st p = b₂ ^ r implies b₁ = b₂ ) & ( not p is S -headed & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) by TH4;

end;

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

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 b₁ being FinSequence st p = (S -head p) ^ b₁

proof end;

uniqueness
for b₁, b₂ being FinSequence st p = (S -head p) ^ b₁ & p = (S -head p) ^ b₂ holds
b₁ = b₂ by FINSEQ_1:33;

end;

:: deftheorem Def10 defines -tail POLNOT_1:def 23 :
for S being Polish-language
for p, b₃ being FinSequence holds
( b₃ = S -tail p iff p = (S -head p) ^ 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 )

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 b₁ 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₁ . (u,v) = (Polish-operation (T,A,t)) . (u ^ v)

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₂ . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ) holds
b₁ = b₂

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 b₄ being BinOp of (Polish-WFF-set (T,A)) holds
( b₄ = 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₄ . (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 b₁ being FinSequence of bool X st
( not b₁ is exhaustive & b₁ 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 b₁ being FinSequence-membered antichain-like set st b₁ is with_non-empty_elements

proof end;

cluster functional non empty non trivial FinSequence-membered antichain-like for set ;

existence
not for b₁ being Polish-language holds b₁ 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 b₁ being FinSequence-membered antichain-like set st not b₁ is trivial holds
b₁ 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 b₁ being FinSequence of S st
( dom b₁ = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b₁ . m = S -head ((S ^^ k) -tail p) ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of S st dom b₁ = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b₁ . m = S -head ((S ^^ k) -tail p) ) ) & dom b₂ = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b₂ . m = S -head ((S ^^ k) -tail p) ) ) holds
b₁ = b₂

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 b₄ being FinSequence of S holds
( b₄ = decomp (S,n,p) iff ( dom b₄ = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b₄ . 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 b₁ being Element of S ^^ (len p) st decomp (S,(len p),b₁) = p

proof end;

uniqueness
for b₁, b₂ being Element of S ^^ (len p) st decomp (S,(len p),b₁) = p & decomp (S,(len p),b₂) = p holds
b₁ = b₂

proof end;

end;

:: deftheorem Def102 defines FlattenSeq POLNOT_1:def 44 :
for S being Polish-language
for p being FinSequence of S
for b₃ being Element of S ^^ (len p) holds
( b₃ = FlattenSeq p iff decomp (S,(len p),b₃) = 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 b₁ 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₁ . (t,p) = s . t ) & ( not t in dom s implies b₁ . (t,p) = t ^ (FlattenSeq p) ) )

proof end;

uniqueness
for b₁, b₂ 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₁ . (t,p) = s . t ) & ( not t in dom s implies b₁ . (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₂ . (t,p) = s . t ) & ( not t in dom s implies b₂ . (t,p) = t ^ (FlattenSeq p) ) ) ) holds
b₁ = b₂

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 b₄ being Polish-recursion-function of E,(Polish-WFF-set (L,E)) holds
( b₄ = 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₄ . (t,p) = s . t ) & ( not t in dom s implies b₄ . (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 b₁ 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₁ = H . F )

proof end;

uniqueness
for b₁, b₂ 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₁ = H . F ) & ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st
( H is Subst s -recursive & b₂ = H . F ) holds
b₁ = b₂ 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, b₅ being Polish-WFF of L,E holds
( b₅ = 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₅ = 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;