:: Polish Notation :: by Taneli Huuskonen :: :: Received April 30, 2015 :: Copyright (c) 2015-2021 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;