:: Polish Notation
:: by Taneli Huuskonen
::
:: Received April 30, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, TARSKI, ARYTM_3,
CARD_1, ORDINAL4, FUNCT_1, RELAT_1, NAT_1, POLNOT_1, PRE_POLY, ZFMISC_1,
PROB_2, PARTFUN1, QC_LANG1, XCMPLX_0, SETFAM_1, BINOP_1, CQC_LANG;
notations TARSKI, XBOOLE_0, SUBSET_1, NAT_1, SETFAM_1, NUMBERS, FINSEQ_1,
XXREAL_0, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, ORDINAL1, ZFMISC_1,
PROB_2, BINOP_1, FUNCT_2;
constructors PRE_POLY, RELSET_1, PROB_2, SETFAM_1;
registrations ORDINAL1, XREAL_0, FINSEQ_1, SUBSET_1, RELAT_1, XBOOLE_0,
FUNCT_1, NAT_1, CARD_1, SETFAM_1, RELSET_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
begin :: Preliminaries
reserve k,m,n for Nat,
a, b, c, c1, c2 for object,
x, y, z, X, Y, Z for set,
D for non empty set;
reserve p, q, r, s, t, u, v for FinSequence;
reserve P, Q, R, P1, P2, Q1, Q2, R1, R2 for FinSequence-membered set;
reserve S, T for non empty FinSequence-membered set;
::
:: 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 is FinSequence of D, q is FinSequence of D
: p in P & q in Q};
end;
definition
let P, Q;
func P^Q -> FinSequence-membered set means
:: POLNOT_1:def 2
for a holds a in it iff ex p, q st a = p^q & p in P & q in Q;
end;
registration
let E be empty set;
let P;
cluster E^P -> empty;
cluster P^E -> empty;
end;
registration
let S, T;
cluster S^T -> non empty;
end;
theorem :: POLNOT_1:1
for p,q,r,s st p^q = r^s ex t st p^t = r or p = r^t;
theorem :: POLNOT_1:2
for P, Q, R holds (P^Q)^R = P^(Q^R);
registration
cluster {{}} -> non empty FinSequence-membered;
end;
theorem :: POLNOT_1:3
for P holds P^{{}} = P & {{}}^P = P;
definition
let P;
func P^^ -> Function means
:: POLNOT_1:def 3
dom it = NAT & it.0 = {{}} & for n holds ex Q st Q = it.n & it.(n+1) = Q^P;
end;
definition
let P, n;
func P^^n -> FinSequence-membered set equals
:: POLNOT_1:def 4
P^^.n;
end;
theorem :: POLNOT_1:4
for P holds {} in P^^0;
registration
let P;
let n be zero Nat;
cluster P^^n -> non empty;
end;
registration
let E be empty set;
let n be non zero Nat;
cluster E^^n -> empty;
end;
definition
let P;
func P* -> non empty FinSequence-membered set equals
:: POLNOT_1:def 5
union the set of all P^^n where n is Nat;
end;
theorem :: POLNOT_1:5
for P, a holds a in P* iff ex n st a in P^^n;
theorem :: POLNOT_1:6
for P holds P^^0 = {{}} & for n holds P^^(n+1) = (P^^n)^P;
theorem :: POLNOT_1:7
for P holds P^^1 = P;
theorem :: POLNOT_1:8
for P, n holds P^^n c= P*;
theorem :: POLNOT_1:9
for P holds {} in P* & P c= P*;
theorem :: POLNOT_1:10
for P, m, n holds P^^(m+n) = (P^^m)^(P^^n);
theorem :: POLNOT_1:11
for P, p, q, m, n st p in P^^m & q in P^^n holds p^q in P^^(m+n);
theorem :: POLNOT_1:12
for P, p, q st p in P* & q in P* holds p^q in P*;
theorem :: POLNOT_1:13
for P, Q, R st P c= R* & Q c= R* holds P^Q c= R*;
theorem :: POLNOT_1:14
for P, Q, n st Q c= P* holds Q^^n c= P*;
theorem :: POLNOT_1:15
for P, Q st Q c= P* holds Q* c= P*;
theorem :: POLNOT_1:16
for P1, P2, Q1, Q2 st P1 c= P2 & Q1 c= Q2 holds P1^Q1 c= P2^Q2;
theorem :: POLNOT_1:17
for P, Q st P c= Q for n holds P^^n c= Q^^n;
registration
let S, n;
cluster S^^n -> non empty FinSequence-membered;
end;
begin :: The Language
reserve A for Function of P, NAT;
reserve U, V, W for Subset of P*;
definition
let P, A, U;
func Polish-expression-layer(P, A, U) -> Subset of P* means
:: POLNOT_1:def 6
for a holds a in it
iff a in P* & ex p, q, n st a = p^q & p in P & n = A.p & q in U^^n;
end;
theorem :: POLNOT_1:18
for P, A, U, n, p, q st p in P & n = A.p & q in U^^n holds
p^q in Polish-expression-layer(P, A, U);
definition
let P, A;
func Polish-atoms(P, A) -> Subset of P* means
:: POLNOT_1:def 7
for a holds a in it iff a in P & A.a = 0;
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};
end;
theorem :: POLNOT_1:19
for P, A, U holds Polish-atoms(P, A) c= Polish-expression-layer(P, A, U);
theorem :: POLNOT_1:20
for P, A, U, V st U c= V holds
Polish-expression-layer(P, A, U) c= Polish-expression-layer(P, A, V);
theorem :: POLNOT_1:21
for P, A, U, u st u in Polish-expression-layer(P, A, U)
ex p, q st p in P & u = p^q;
definition
let P, A;
func Polish-expression-hierarchy(P, A) -> Function means
:: POLNOT_1:def 9
dom it = NAT & it.0 = Polish-atoms(P, A)
& for n holds ex U st U = it.n &
it.(n+1) = Polish-expression-layer(P, A, U);
end;
definition
let P, A, n;
func Polish-expression-hierarchy(P, A, n) -> Subset of P* equals
:: POLNOT_1:def 10
Polish-expression-hierarchy(P, A).n;
end;
theorem :: POLNOT_1:22
for P, A holds Polish-expression-hierarchy(P, A, 0) = Polish-atoms(P, A);
theorem :: POLNOT_1:23
for P, A, n holds Polish-expression-hierarchy(P, A, n+1)
= Polish-expression-layer(P, A, Polish-expression-hierarchy(P, A, n));
theorem :: POLNOT_1:24
for P, A, n holds
Polish-expression-hierarchy(P, A, n)
c= Polish-expression-hierarchy(P, A, n+1);
theorem :: POLNOT_1:25
for P, A, n, m holds
Polish-expression-hierarchy(P, A, n)
c= Polish-expression-hierarchy(P, A, n+m);
definition
let P, A;
func Polish-expression-set(P, A) -> Subset of P* equals
:: POLNOT_1:def 11
union the set of all Polish-expression-hierarchy(P, A, n) where n is Nat;
end;
theorem :: POLNOT_1:26
for P, A, n holds Polish-expression-hierarchy(P, A, n)
c= Polish-expression-set(P, A);
theorem :: POLNOT_1:27
for P, A, n, q st q in (Polish-expression-set(P, A))^^n
ex m st q in (Polish-expression-hierarchy(P, A, m))^^n;
theorem :: POLNOT_1:28
for P, A, a st a in Polish-expression-set(P, A)
ex n st a in Polish-expression-hierarchy(P, A, n+1);
definition
let P, A;
mode Polish-expression of P, A is Element of Polish-expression-set(P, A);
end;
definition
let P, A, n, t;
assume t in P;
func Polish-operation (P, A, n, t)
-> Function of (Polish-expression-set(P, A))^^n, P* means
:: POLNOT_1:def 12
for q st q in dom it holds it.q = t^q;
end;
definition
let X, Y;
let F be PartFunc of X, bool Y;
redefine attr F is disjoint_valued means
:: POLNOT_1:def 13
for a, b st a in dom F & b in dom F & a <> b holds F.a misses F.b;
end;
registration
let X be set;
cluster disjoint_valued for FinSequence of bool X;
end;
theorem :: POLNOT_1:29
for X being set for B being disjoint_valued FinSequence of bool X
for a, b, c st a in B.b & a in B.c holds b = c & b in dom B;
definition
let X;
let B be disjoint_valued FinSequence of bool X;
func arity-from-list B -> Function of X, NAT means
:: POLNOT_1:def 14
for a st a in X holds
((ex n st a in B.n) & a in B.(it.a))
or ((not ex n st a in B.n) & it.a = 0);
end;
theorem :: POLNOT_1:30
for X for B being disjoint_valued FinSequence of bool X for a st a in X
holds (arity-from-list B).a <> 0 iff ex n st a in B.n;
theorem :: POLNOT_1:31
for X for B being disjoint_valued FinSequence of bool X for a, n
st a in B.n holds (arity-from-list B).a = n;
theorem :: POLNOT_1:32
for P, A, r st r in Polish-expression-set(P, A)
ex n, p, q
st p in P & n = A.p & q in Polish-expression-set(P, A)^^n & r = p^q;
definition
let P, A, Q;
attr Q is A-closed means
:: POLNOT_1:def 15
for p, n, q st p in P & n = A.p & q in Q^^n holds p^q in Q;
end;
theorem :: POLNOT_1:33
for P, A holds Polish-expression-set(P, A) is A-closed;
theorem :: POLNOT_1:34
for P, A, Q st Q is A-closed holds Polish-atoms(P, A) c= Q;
theorem :: POLNOT_1:35
for P, A, Q, n st Q is A-closed holds
Polish-expression-hierarchy(P, A, n) c= Q;
theorem :: POLNOT_1:36
for P, A holds Polish-atoms(P, A) c= Polish-expression-set(P, A);
theorem :: POLNOT_1:37
for P, A, Q st Q is A-closed holds Polish-expression-set(P, A) c= Q;
theorem :: POLNOT_1:38
for P, A, r st r in Polish-expression-set(P, A)
ex n, t, q st t in P & n = A.t & r = Polish-operation(P, A, n, t).q;
theorem :: POLNOT_1:39
for P, A, n, p, q 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);
scheme :: POLNOT_1:sch 1
AInd {
P() -> FinSequence-membered set,
A() -> Function of P(), NAT,
X[object] } :
for a st a in Polish-expression-set(P(), A()) holds X[ a ]
provided
for p, q, n
st p in P() & n = A().p & q in Polish-expression-set(P(), A())^^n
holds X[p^q];
begin
::
:: Polish Notation, Part II: Parsing
::
reserve k,l,m,n,i,j for Nat,
a, b, c, c1, c2 for object,
x, y, z, X, Y, Z for set,
D, D1, D2 for non empty set;
reserve p, q, r, s, t, u, v for FinSequence;
reserve P, Q, R for FinSequence-membered set;
definition
let P;
attr P is antichain-like means
:: POLNOT_1:def 16
for p,q st p in P & p^q in P holds q = {};
end;
theorem :: POLNOT_1:40
for P holds P is antichain-like
iff for p,q st p in P & p^q in P holds p = p^q;
theorem :: POLNOT_1:41
for P, Q st P c= Q & Q is antichain-like holds P is antichain-like;
registration
cluster trivial -> antichain-like for FinSequence-membered set;
end;
theorem :: POLNOT_1:42
for P, a st P = {a} holds P is antichain-like;
registration
cluster antichain-like for non empty FinSequence-membered set;
cluster empty -> antichain-like for FinSequence-membered set;
end;
definition
mode antichain is antichain-like FinSequence-membered set;
end;
reserve B, C for antichain;
registration
let B;
cluster -> antichain-like FinSequence-membered for Subset of B;
end;
definition
mode Polish-language is non empty antichain;
end;
reserve S, T for Polish-language;
definition
let D be non empty set;
let G be Subset of D*;
redefine attr G is antichain-like means
:: POLNOT_1:def 17
for g being FinSequence of D,h being FinSequence of D
st g in G & g^h in G holds h = <*>D;
end;
theorem :: POLNOT_1:43
for B for p, q, r, s st p^q = r^s & p in B & r in B
holds p = r & q = s;
registration
let B, C;
cluster B^C -> antichain-like;
end;
theorem :: POLNOT_1:44
for P st for p, q st p in P & q in P holds dom p = dom q
holds P is antichain-like;
theorem :: POLNOT_1:45
for P, a st for p st p in P holds dom p = a holds P is antichain-like;
theorem :: POLNOT_1:46
for B holds {} in B implies B = {{}};
registration
let B, n;
cluster B^^n -> antichain-like;
end;
registration
let T;
cluster non empty antichain-like for Subset of (T*);
let n;
cluster T^^n -> non empty;
end;
definition
let T;
mode Polish-language of T is non empty antichain-like Subset of (T*);
mode Polish-arity-function of T -> Function of T, NAT means
:: POLNOT_1:def 18
ex a st a in T & it.a = 0;
end;
registration
let T;
cluster -> non empty antichain-like FinSequence-membered
for Polish-language of T;
end;
reserve A for Polish-arity-function of T;
reserve U, V, W for Polish-language of T;
definition
let T, A;
let t be Element of T;
redefine func A.t -> Nat;
end;
definition
let T, A, U;
redefine func Polish-expression-layer(T, A, U) means
:: POLNOT_1:def 19
for a holds a in it iff ex t being Element of T, u being Element of T*
st a = t^u & u in U^^(A.t);
end;
definition
let B, p;
attr p is B-headed means
:: POLNOT_1:def 20
ex q, r st q in B & p = q^r;
end;
definition
let B, P;
attr P is B-headed means
:: POLNOT_1:def 21
for p st p in P holds p is B-headed;
end;
theorem :: POLNOT_1:47
for B, C, p st p is B-headed & B c= C holds p is C-headed;
theorem :: POLNOT_1:48
for B, C, P st P is B-headed & B c= C holds P is C-headed;
registration
let B, P;
cluster B^P -> B-headed;
end;
theorem :: POLNOT_1:49
for B, C, p st p is (B^C)-headed holds p is B-headed;
theorem :: POLNOT_1:50
for B holds B is B-headed;
registration
let B;
cluster B-headed for FinSequence-membered set;
end;
registration
let B;
let P be B-headed FinSequence-membered set;
cluster -> B-headed for Subset of P;
end;
registration
let S;
cluster non empty S-headed for FinSequence-membered set;
end;
theorem :: POLNOT_1:51
for S, m, n holds S^^(m+n) is (S^^m)-headed;
definition
let S, p;
func S-head p -> FinSequence means
:: POLNOT_1:def 22
it in S & ex r st p = it^r if p is S-headed otherwise it = {};
end;
definition
let S, p;
func S-tail p -> FinSequence means
:: POLNOT_1:def 23
p = (S-head p)^it;
end;
theorem :: POLNOT_1:52
for S, s, t st s in S holds S-head (s^t) = s & S-tail (s^t) = t;
theorem :: POLNOT_1:53
for S, s st s in S holds S-head s = s & S-tail s = {};
theorem :: POLNOT_1:54
for S, T, u st u in S^T holds S-head u in S & S-tail u in T;
theorem :: POLNOT_1:55
for S, T, u st S c= T & u is S-headed holds
S-head u = T-head u & S-tail u = T-tail u;
theorem :: POLNOT_1:56
for S, s, t 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;
theorem :: POLNOT_1:57
for S, m, n, s st m+1 <= n & s in S^^n
holds s is (S^^m)-headed & (S^^m)-tail s is S-headed;
theorem :: POLNOT_1:58
for S, s holds s is (S^^0)-headed & (S^^0)-head s = {} & (S^^0)-tail s = s;
registration
let T, A;
cluster Polish-atoms(T, A) -> non empty antichain-like;
let U;
cluster Polish-expression-layer(T, A, U) -> non empty antichain-like;
end;
definition
let T, A, U;
redefine func Polish-expression-layer(T, A, U) -> Polish-language of T;
end;
definition
let T, A;
func Polish-operations(T, A) -> Subset of T equals
:: POLNOT_1:def 24
{t where t is Element of T : A.t <> 0};
end;
registration
let T, A, n;
cluster Polish-expression-hierarchy(T, A, n) -> antichain-like non empty;
end;
definition
let T, A, n;
redefine func Polish-expression-hierarchy(T, A, n) -> Polish-language of T;
end;
definition
let T, A;
func Polish-WFF-set(T, A) -> Polish-language of T equals
:: POLNOT_1:def 25
Polish-expression-set(T, A);
end;
definition
let T, A;
mode Polish-WFF of T, A is Element of Polish-WFF-set(T, A);
end;
definition
let T, A;
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);
end;
definition
let T, A;
let t be Element of T;
assume A.t = 1;
func Polish-unOp (T, A, t) -> UnOp of Polish-WFF-set(T, A) equals
:: POLNOT_1:def 27
Polish-operation(T, A, t);
end;
definition
let T, A;
let t be Element of T;
assume A.t = 2;
func Polish-binOp (T, A, t) -> BinOp of Polish-WFF-set(T, A) means
:: POLNOT_1:def 28
for u, v 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);
end;
reserve F, G for Polish-WFF of T, A;
definition
let X, Y;
let F be PartFunc of X, bool Y;
attr F is exhaustive means
:: POLNOT_1:def 29
for a st a in Y ex b st b in dom F & a in F.b;
end;
registration
let X be non empty set;
cluster non exhaustive disjoint_valued for FinSequence of bool X;
end;
theorem :: POLNOT_1:59
for X, Y for F being PartFunc of X, bool Y holds
F is non exhaustive iff
ex a st a in Y & for b st b in dom F holds not a in F.b;
definition
let T;
let B be non exhaustive disjoint_valued FinSequence of bool T;
func Polish-arity-from-list B -> Polish-arity-function of T equals
:: POLNOT_1:def 30
arity-from-list B;
end;
registration
cluster with_non-empty_elements
for antichain-like FinSequence-membered set;
cluster non trivial for Polish-language;
end;
registration
cluster non trivial -> with_non-empty_elements
for antichain-like FinSequence-membered set;
end;
definition
let S, n, m;
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);
end;
definition
let S, n;
let p be Element of S^^n;
func decomp( S, n, p ) -> FinSequence of S means
:: POLNOT_1:def 32
dom it = Seg n
& for m st m in Seg n ex k st m = k+1 & it.m = S-head((S^^k)-tail p);
end;
theorem :: POLNOT_1:60
for S, T, n for s being Element of S^^n, t being Element of T^^n
st S c= T & s = t holds decomp( S, n, s ) = decomp( T, n, t );
theorem :: POLNOT_1:61
for S for q being Element of S^^0 holds decomp(S, 0, q) = {};
theorem :: POLNOT_1:62
for S, n for q being Element of S^^n holds len decomp(S, n, q) = n;
theorem :: POLNOT_1:63
for S for q being Element of S^^1 holds decomp(S, 1, q) = <*q*>;
theorem :: POLNOT_1:64
for S 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*>;
theorem :: POLNOT_1:65
for T, A holds Polish-WFF-set(T, A) is T-headed;
theorem :: POLNOT_1:66
for T, A, n holds Polish-expression-hierarchy(T, A, n) is T-headed;
definition
let T, A, F;
func Polish-WFF-head F -> Element of T equals
:: POLNOT_1:def 33
T-head F;
end;
definition
let T, A, n;
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;
end;
definition
let T, A, F;
func Polish-arity F -> Nat equals
:: POLNOT_1:def 35
A.(Polish-WFF-head F);
end;
definition
let T, A, n;
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);
end;
theorem :: POLNOT_1:67
for T, A, F holds T-tail F in (Polish-WFF-set(T, A))^^Polish-arity F;
theorem :: POLNOT_1:68
for T, A, n 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;
definition
let T, A, F;
func (T, A)-tail F -> Element of Polish-WFF-set(T, A)^^Polish-arity F equals
:: POLNOT_1:def 37
T-tail F;
end;
theorem :: POLNOT_1:69
for T, A, F st T-head F in Polish-atoms(T, A) holds F = T-head F;
definition
let T, A, n;
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;
end;
definition
let T, A, F;
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 );
end;
definition
let T, A, n;
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 );
end;
theorem :: POLNOT_1:70
for T, A for t being Element of T for u st u in Polish-WFF-set(T, A)^^(A.t)
holds T-tail (Polish-operation(T, A, t).u) = u;
theorem :: POLNOT_1:71
for T, A, F, n st F in Polish-expression-hierarchy(T, A, n+1) holds
rng Polish-WFF-args F c= Polish-expression-hierarchy(T, A, n);
theorem :: POLNOT_1:72
for Y, Z, D 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 st a in rng p holds f.a = g.a
holds f * p = g * p;
definition
let T, A, D;
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};
end;
definition
let T, A, D;
mode Polish-recursion-function of A, D
is Function of Polish-recursion-domain(A, D), D;
end;
reserve f for Polish-recursion-function of A, D;
reserve K, K1, K2 for Function of Polish-WFF-set(T, A), D;
definition
let T, A, D, f, K;
attr K is f-recursive means
:: POLNOT_1:def 42
for F holds K.F = f.[ T-head F, K * (Polish-WFF-args F) ];
end;
theorem :: POLNOT_1:73
for T, A, D, f, K1, K2 st K1 is f-recursive & K2 is f-recursive holds K1 = K2
;
reserve L for non trivial Polish-language;
reserve E for Polish-arity-function of L;
reserve g for Polish-recursion-function of E, D;
reserve J, J1, J2, J3 for Subset of Polish-WFF-set(L, E);
reserve H for Function of J, D;
reserve H1 for Function of J1, D;
reserve H2 for Function of J2, D;
reserve H3 for Function of J3, D;
definition
let L, E, D, g, J, H;
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;
theorem :: POLNOT_1:74
for L, E, D, g, n ex J, H st J = Polish-expression-hierarchy(L, E, n)
& H is g-recursive;
theorem :: POLNOT_1:75
for L, E, D, g ex K being Function of Polish-WFF-set(L, E), D
st K is g-recursive;
theorem :: POLNOT_1:76
for L, E for t being Element of L holds Polish-operation(L, E, t)
is one-to-one;
theorem :: POLNOT_1:77
for L, E for t, u being Element of L
st rng Polish-operation(L, E, t) meets rng Polish-operation(L, E, u)
holds t = u;
theorem :: POLNOT_1:78
for L, E for t being Element of L
for a st a in dom Polish-operation(L, E, t) ex p st
p = Polish-operation(L, E, t).a & L-head p = t;
theorem :: POLNOT_1:79
for L, E 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;
theorem :: POLNOT_1:80
for L, E for t being Element of L st E.t = 1 for F being Polish-WFF of L, E
st Polish-WFF-head F = t ex G being Polish-WFF of L, E
st F = Polish-unOp(L, E, t).G;
theorem :: POLNOT_1:81
for L, E for t being Element of L st E.t = 1 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*>;
theorem :: POLNOT_1:82
for L, E for t being Element of L st E.t = 2 for F being Polish-WFF of L, E
st Polish-WFF-head F = t ex G, H being Polish-WFF of L, E
st F = Polish-binOp(L, E, t).(G, H);
theorem :: POLNOT_1:83
for L, E for t being Element of L st E.t = 2
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*>;
theorem :: POLNOT_1:84
for L, E for F being Polish-WFF of L, E holds
F in Polish-atoms(L, E) iff Polish-arity F = 0;
theorem :: POLNOT_1:85
for L, E, D, g 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*>);
definition
let S;
let p be FinSequence of S;
func FlattenSeq p -> Element of S^^(len p) means
:: POLNOT_1:def 44
decomp( S, len p, it ) = p;
end;
definition
let L, E;
mode Substitution of L, E is
PartFunc of Polish-atoms(L, E), Polish-WFF-set(L, E);
end;
definition
let L, E;
let s be Substitution of L, E;
func Subst s -> Polish-recursion-function of E, Polish-WFF-set(L, E) means
:: POLNOT_1:def 45
for t being Element of L, 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));
end;
definition
let L, E;
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
:: 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;
end;
theorem :: POLNOT_1:86
for L, E for s being Substitution of L, E for F being Polish-WFF of L, E
st s = {} holds Subst(s, F) = F;