:: Extensions of Languages in {P}olish Notation
:: by Taneli Huuskonen
::
:: Received May 23, 2025
:: Copyright (c) 2025 Association of Mizar Users

Lm22: for x being trivial set
for y being Subset of x st not y is empty holds
x = y

proof end;

definition

let F be Function;

attr F is Polish-arity-like means :Def1: :: POLNOT_2:def 1
ex T being Polish-language st F is Polish-arity-function of T;

end;

:: deftheorem Def1 defines Polish-arity-like POLNOT_2:def 1 :
for F being Function holds
( F is Polish-arity-like iff ex T being Polish-language st F is Polish-arity-function of T );

registration

let T be Polish-language;

cluster -> Polish-arity-like for Polish-arity-function of T;

coherence
for b₁ being Polish-arity-function of T holds b₁ is Polish-arity-like ;

end;

definition

let F be Function;

redefine attr F is Polish-arity-like means :Def2: :: POLNOT_2:def 2
( dom F is Polish-language & F is natural-valued & F is with_zero );

compatibility
( F is Polish-arity-like iff ( dom F is Polish-language & F is natural-valued & F is with_zero ) )

proof end;

end;

:: deftheorem Def2 defines Polish-arity-like POLNOT_2:def 2 :
for F being Function holds
( F is Polish-arity-like iff ( dom F is Polish-language & F is natural-valued & F is with_zero ) );

registration

cluster Relation-like Function-like Polish-arity-like -> with_zero natural-valued for set ;

coherence
for b₁ being Function st b₁ is Polish-arity-like holds
( b₁ is natural-valued & b₁ is with_zero ) ;

end;

registration

cluster Relation-like Function-like Polish-arity-like for set ;

existence
ex b₁ being Function st b₁ is Polish-arity-like

proof end;

end;

definition

mode Polish-arity-function is Polish-arity-like Function;

end;

definition

let B, C be Polish-arity-function;

attr C is B -extending means :Def3: :: POLNOT_2:def 3
B c= C;

end;

:: deftheorem Def3 defines -extending POLNOT_2:def 3 :
for B, C being Polish-arity-function holds
( C is B -extending iff B c= C );

definition

let B be Polish-arity-function;
:: original: dom
redefine func dom B -> Polish-language;
coherence
dom B is Polish-language

proof end;

end;

Lemma1: for B being Polish-arity-function holds
( B is empty-yielding iff for a being object st a in dom B holds
B . a = 0 )

proof end;

theorem Th1: :: POLNOT_2:1

for T being Polish-language
for B being Polish-arity-function holds
( B is Polish-arity-function of T iff T = dom B )

proof end;

definition

let B be Polish-arity-function;

func Polish-WFF-set B -> Polish-language of (dom B) means :Def4: :: POLNOT_2:def 4
ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & it = Polish-WFF-set (T,A) );

existence
ex b₁ being Polish-language of (dom B) ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & b₁ = Polish-WFF-set (T,A) )

proof end;

uniqueness
for b₁, b₂ being Polish-language of (dom B) st ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & b₁ = Polish-WFF-set (T,A) ) & ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & b₂ = Polish-WFF-set (T,A) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Polish-WFF-set POLNOT_2:def 4 :
for B being Polish-arity-function
for b₂ being Polish-language of (dom B) holds
( b₂ = Polish-WFF-set B iff ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & b₂ = Polish-WFF-set (T,A) ) );

definition

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

:: original: empty-yielding
redefine attr A is empty-yielding means :: POLNOT_2:def 5
for a being object st a in T holds
A . a = 0 ;

compatibility
( A is empty-yielding iff for a being object st a in T holds
A . a = 0 )

proof end;

end;

:: deftheorem defines empty-yielding POLNOT_2:def 5 :
for T being Polish-language
for A being Polish-arity-function of T holds
( A is empty-yielding iff for a being object st a in T holds
A . a = 0 );

definition

let T be Polish-language;
let A be Polish-arity-function of T;
let P be non empty FinSequence-membered set ;

:: original: -closed
redefine attr P is A -closed means :Def6: :: POLNOT_2:def 6
for p being FinSequence
for n being Nat
for q being FinSequence st p in T & n = A . p & q in P ^^ n holds
p ^ q in P;

compatibility
( P is A -closed iff for p being FinSequence
for n being Nat
for q being FinSequence st p in T & n = A . p & q in P ^^ n holds
p ^ q in P )

proof end;

end;

:: deftheorem Def6 defines -closed POLNOT_2:def 6 :
for T being Polish-language
for A being Polish-arity-function of T
for P being non empty FinSequence-membered set holds
( P is A -closed iff for p being FinSequence
for n being Nat
for q being FinSequence st p in T & n = A . p & q in P ^^ n holds
p ^ q in P );

registration

let T be Polish-language;

cluster Relation-like with_zero empty-yielding T -defined NAT -valued Function-like quasi_total complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued Polish-arity-like for Polish-arity-function of T;

existence
not for b₁ being Polish-arity-function of T holds b₁ is empty-yielding

proof end;

end;

definition

let T be Polish-language;
let V be Polish-language of T;

attr V is full means :Def8: :: POLNOT_2:def 7
ex A being Polish-arity-function of T st V = Polish-WFF-set (T,A);

end;

:: deftheorem Def8 defines full POLNOT_2:def 7 :
for T being Polish-language
for V being Polish-language of T holds
( V is full iff ex A being Polish-arity-function of T st V = Polish-WFF-set (T,A) );

registration

let T be Polish-language;

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

existence
ex b₁ being Polish-language of T st b₁ is full

proof end;

end;

definition

let T be Polish-language;
let A be Polish-arity-function of T;
:: original: Polish-WFF-set
redefine func Polish-WFF-set (T,A) -> full Polish-language of T;
coherence
Polish-WFF-set (T,A) is full Polish-language of T by Def8;

end;

Lm2: for K being non trivial Polish-language
for m, n being Nat
for a being object st a in K ^^ m & a in K ^^ n holds
m <= n

proof end;

Lm3: for T being Polish-language
for m, n being Nat
for a being object st a in T ^^ m & a in T ^^ n & not T is trivial holds
m = n

proof end;

Lm4: for T being Polish-language
for A being Polish-arity-function of T
for t being Element of T
for u being FinSequence holds
( t ^ u in Polish-WFF-set (T,A) iff u in (Polish-WFF-set (T,A)) ^^ (A . t) )

proof end;

Lm5: for T being Polish-language
for A being Polish-arity-function of T
for a being object st T is trivial & a in T holds
A . a = 0

proof end;

definition

let T, U be Polish-language;

attr U is T -extending means :Def9: :: POLNOT_2:def 8
T c= U;

end;

:: deftheorem Def9 defines -extending POLNOT_2:def 8 :
for T, U being Polish-language holds
( U is T -extending iff T c= U );

registration

let T be Polish-language;

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

existence
ex b₁ being Polish-language st b₁ is T -extending

proof end;

end;

registration

let K be non trivial Polish-language;

cluster non empty FinSequence-membered antichain-like K -extending -> non trivial for set ;

coherence
for b₁ being Polish-language st b₁ is K -extending holds
not b₁ is trivial ;

end;

definition

let B be Polish-arity-function;
let S be Polish-language;

attr S is B -compatible means :: POLNOT_2:def 9
for s being FinSequence st s in S & s is dom B -headed holds
ex n being Nat st
( n = B . ((dom B) -head s) & (dom B) -tail s in S ^^ n );

end;

:: deftheorem defines -compatible POLNOT_2:def 9 :
for B being Polish-arity-function
for S being Polish-language holds
( S is B -compatible iff for s being FinSequence st s in S & s is dom B -headed holds
ex n being Nat st
( n = B . ((dom B) -head s) & (dom B) -tail s in S ^^ n ) );

definition

let T be Polish-language;
let A be Polish-arity-function of T;
let S be Polish-language;

:: original: -compatible
redefine attr S is A -compatible means :: POLNOT_2:def 10
for s being FinSequence st s in S & s is T -headed holds
T -tail s in S ^^ (A . (T -head s));

compatibility
( S is A -compatible iff for s being FinSequence st s in S & s is T -headed holds
T -tail s in S ^^ (A . (T -head s)) )

proof end;

end;

:: deftheorem defines -compatible POLNOT_2:def 10 :
for T being Polish-language
for A being Polish-arity-function of T
for S being Polish-language holds
( S is A -compatible iff for s being FinSequence st s in S & s is T -headed holds
T -tail s in S ^^ (A . (T -head s)) );

registration

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

cluster Polish-WFF-set (T,A) -> (A) ;

coherence
Polish-WFF-set (T,A) is A -compatible

proof end;

end;

registration

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

cluster functional non empty FinSequence-membered -closed antichain-like (A) for set ;

existence
ex b₁ being Polish-language st
( b₁ is -closed & b₁ is (A) )

proof end;

end;

registration

let B be Polish-arity-function;

cluster Relation-like non non-empty NAT -valued Function-like complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued Polish-arity-like B -extending for set ;

existence
ex b₁ being Polish-arity-function st b₁ is B -extending

proof end;

cluster functional non empty FinSequence-membered B -closed antichain-like B -compatible for set ;

existence
ex b₁ being Polish-language st
( b₁ is B -closed & b₁ is B -compatible )

proof end;

end;

definition

let B be Polish-arity-function;
mode Polish-ext-set of B is B -closed B -compatible Polish-language;
mode Extension of B is B -extending Polish-arity-function;

end;

registration

let B be Polish-arity-function;
let C be Extension of B;

cluster Relation-like Function-like Polish-arity-like C -extending -> B -extending for set ;

coherence
for b₁ being Polish-arity-function st b₁ is C -extending holds
b₁ is B -extending

proof end;

end;

registration

let B be Polish-arity-function;
let C be Extension of B;

cluster non empty FinSequence-membered C -closed antichain-like -> B -closed for set ;

coherence
for b₁ being Polish-language st b₁ is C -closed holds
b₁ is B -closed

proof end;

cluster non empty FinSequence-membered antichain-like C -compatible -> B -compatible for set ;

coherence
for b₁ being Polish-language st b₁ is C -compatible holds
b₁ is B -compatible

proof end;

end;

theorem :: POLNOT_2:2

for B being Polish-arity-function
for Z being b₁ -closed Polish-language
for p, q being FinSequence st p in dom B & B . p = 1 & q in Z holds
p ^ q in Z

proof end;

theorem :: POLNOT_2:3

for B being Polish-arity-function
for Z being b₁ -closed Polish-language
for p, q, r being FinSequence st p in dom B & B . p = 2 & q in Z & r in Z holds
p ^ (q ^ r) in Z

proof end;

definition

let B be Polish-arity-function;
let Z be B -closed Polish-language;
let p be FinSequence;
assume A1: ( p in dom B & B . p = 1 ) ;

func Polish-unOp (B,Z,p) -> UnOp of Z means :Def15: :: POLNOT_2:def 11
for q being FinSequence st q in Z holds
it . q = p ^ q;

existence
ex b₁ being UnOp of Z st
for q being FinSequence st q in Z holds
b₁ . q = p ^ q

proof end;

uniqueness
for b₁, b₂ being UnOp of Z st ( for q being FinSequence st q in Z holds
b₁ . q = p ^ q ) & ( for q being FinSequence st q in Z holds
b₂ . q = p ^ q ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Polish-unOp POLNOT_2:def 11 :
for B being Polish-arity-function
for Z being b₁ -closed Polish-language
for p being FinSequence st p in dom B & B . p = 1 holds
for b₄ being UnOp of Z holds
( b₄ = Polish-unOp (B,Z,p) iff for q being FinSequence st q in Z holds
b₄ . q = p ^ q );

definition

let B be Polish-arity-function;
let Z be B -closed Polish-language;
let p be FinSequence;
assume A1: ( p in dom B & B . p = 2 ) ;

func Polish-binOp (B,Z,p) -> BinOp of Z means :Def16: :: POLNOT_2:def 12
for q, r being FinSequence st q in Z & r in Z holds
it . (q,r) = p ^ (q ^ r);

existence
ex b₁ being BinOp of Z st
for q, r being FinSequence st q in Z & r in Z holds
b₁ . (q,r) = p ^ (q ^ r)

proof end;

uniqueness
for b₁, b₂ being BinOp of Z st ( for q, r being FinSequence st q in Z & r in Z holds
b₁ . (q,r) = p ^ (q ^ r) ) & ( for q, r being FinSequence st q in Z & r in Z holds
b₂ . (q,r) = p ^ (q ^ r) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines Polish-binOp POLNOT_2:def 12 :
for B being Polish-arity-function
for Z being b₁ -closed Polish-language
for p being FinSequence st p in dom B & B . p = 2 holds
for b₄ being BinOp of Z holds
( b₄ = Polish-binOp (B,Z,p) iff for q, r being FinSequence st q in Z & r in Z holds
b₄ . (q,r) = p ^ (q ^ r) );

definition

let B be Polish-arity-function;
let J be Polish-ext-set of B;

func Polish-ext-complement (B,J) -> Subset of J equals :: POLNOT_2:def 13
{ p where p is Element of J : not p is dom B -headed } ;

coherence
{ p where p is Element of J : not p is dom B -headed } is Subset of J

proof end;

end;

:: deftheorem defines Polish-ext-complement POLNOT_2:def 13 :
for B being Polish-arity-function
for J being Polish-ext-set of B holds Polish-ext-complement (B,J) = { p where p is Element of J : not p is dom B -headed } ;

definition

let B be Polish-arity-function;
let J be Polish-ext-set of B;

func Polish-ext-domain (B,J) -> dom B -extending Polish-language equals :: POLNOT_2:def 14
(dom B) \/ (Polish-ext-complement (B,J));

coherence
(dom B) \/ (Polish-ext-complement (B,J)) is dom B -extending Polish-language

proof end;

end;

:: deftheorem defines Polish-ext-domain POLNOT_2:def 14 :
for B being Polish-arity-function
for J being Polish-ext-set of B holds Polish-ext-domain (B,J) = (dom B) \/ (Polish-ext-complement (B,J));

Lm21: for B being Polish-arity-function
for J being Polish-ext-set of B
for a being object st a in Polish-ext-complement (B,J) holds
( a in J & a in Polish-ext-domain (B,J) & not a in dom B )

proof end;

theorem Th8: :: POLNOT_2:4

for B being Polish-arity-function
for J being Polish-ext-set of B holds Polish-WFF-set B c= J

proof end;

Lm23: for B being Polish-arity-function
for J being Polish-ext-set of B st ( {} in J or {} in dom B ) holds
( J = {{}} & Polish-WFF-set B = {{}} & dom B = {{}} & Polish-ext-complement (B,J) = {} )

proof end;

definition

let P be non empty FinSequence-membered set ;
let n be Nat;

func P |` n -> Subset of P equals :: POLNOT_2:def 15
{ p where p is Element of P : len p <= n } ;

coherence
{ p where p is Element of P : len p <= n } is Subset of P

proof end;

end;

:: deftheorem defines |` POLNOT_2:def 15 :
for P being non empty FinSequence-membered set
for n being Nat holds P |` n = { p where p is Element of P : len p <= n } ;

Lm19: for P being non empty FinSequence-membered set
for p being FinSequence
for n being Nat holds
( p in P |` n iff ( p in P & len p <= n ) )

proof end;

Lm20: for P being non empty FinSequence-membered set
for m, n being Nat holds (P ^^ n) |` m c= (P |` m) ^^ n

proof end;

Lm9: for T being Polish-language
for A being Polish-arity-function of T st A is empty-yielding holds
Polish-WFF-set (T,A) = T

proof end;

theorem :: POLNOT_2:5

for T being Polish-language holds T is full Polish-language of T

proof end;

definition

let T be Polish-language;
let V be full Polish-language of T;

func Polish-arity V -> Polish-arity-function of T means :Def10: :: POLNOT_2:def 16
V = Polish-WFF-set (T,it);

existence
ex b₁ being Polish-arity-function of T st V = Polish-WFF-set (T,b₁) by Def8;
uniqueness
for b₁, b₂ being Polish-arity-function of T st V = Polish-WFF-set (T,b₁) & V = Polish-WFF-set (T,b₂) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Polish-arity POLNOT_2:def 16 :
for T being Polish-language
for V being full Polish-language of T
for b₃ being Polish-arity-function of T holds
( b₃ = Polish-arity V iff V = Polish-WFF-set (T,b₃) );

registration

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

reduce Polish-arity (Polish-WFF-set (T,A)) to A;

reducibility
Polish-arity (Polish-WFF-set (T,A)) = A by Def10;

end;

registration

let T be Polish-language;
let V be full Polish-language of T;

reduce Polish-WFF-set (T,(Polish-arity V)) to V;

reducibility
Polish-WFF-set (T,(Polish-arity V)) = V by Def10;

end;

definition

let B be Polish-arity-function;
let J be Polish-ext-set of B;

func Polish-ext-arity (B,J) -> Polish-arity-function of Polish-ext-domain (B,J) means :Def23: :: POLNOT_2:def 17
J = Polish-WFF-set ((Polish-ext-domain (B,J)),it);

existence
ex b₁ being Polish-arity-function of Polish-ext-domain (B,J) st J = Polish-WFF-set ((Polish-ext-domain (B,J)),b₁)

proof end;

uniqueness
for b₁, b₂ being Polish-arity-function of Polish-ext-domain (B,J) st J = Polish-WFF-set ((Polish-ext-domain (B,J)),b₁) & J = Polish-WFF-set ((Polish-ext-domain (B,J)),b₂) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines Polish-ext-arity POLNOT_2:def 17 :
for B being Polish-arity-function
for J being Polish-ext-set of B
for b₃ being Polish-arity-function of Polish-ext-domain (B,J) holds
( b₃ = Polish-ext-arity (B,J) iff J = Polish-WFF-set ((Polish-ext-domain (B,J)),b₃) );

definition

let T be Polish-language;
mode Formula of T is Element of T;

end;

definition

let B be Polish-arity-function;
let J be Polish-ext-set of B;
let F be Formula of J;

func Polish-ext-head F -> Element of Polish-ext-domain (B,J) equals :: POLNOT_2:def 18
(Polish-ext-domain (B,J)) -head F;

coherence
(Polish-ext-domain (B,J)) -head F is Element of Polish-ext-domain (B,J)

proof end;

end;

:: deftheorem defines Polish-ext-head POLNOT_2:def 18 :
for B being Polish-arity-function
for J being Polish-ext-set of B
for F being Formula of J holds Polish-ext-head F = (Polish-ext-domain (B,J)) -head F;

theorem Th10: :: POLNOT_2:6

for S, T being Polish-language
for p being FinSequence st S -head p in T holds
( p is T -headed & S -head p = T -head p )

proof end;

theorem :: POLNOT_2:7

for B being Polish-arity-function
for J being Polish-ext-set of B
for F being Formula of J st Polish-ext-head F in dom B holds
Polish-ext-head F = (dom B) -head F by Th10;

theorem Th12: :: POLNOT_2:8

for B being Polish-arity-function
for J being Polish-ext-set of B
for F being Formula of J st F is dom B -headed holds
Polish-ext-head F = (dom B) -head F

proof end;

theorem :: POLNOT_2:9

for B being Polish-arity-function
for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for F being Formula of M st C . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (C,M,e)) . G

proof end;

theorem :: POLNOT_2:10

for B being Polish-arity-function
for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for G being Formula of M st C . e = 1 holds
Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e

proof end;

theorem :: POLNOT_2:11

for B being Polish-arity-function
for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for F being Formula of M st C . e = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)

proof end;

theorem :: POLNOT_2:12

for B being Polish-arity-function
for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for G, H being Formula of M st C . e = 2 holds
Polish-ext-head ((Polish-binOp (C,M,e)) . (G,H)) = e

proof end;

theorem Th22: :: POLNOT_2:13

for T being Polish-language
for U being b₁ -extending Polish-language
for V being full Polish-language of T
for W being full Polish-language of U holds
( Polish-arity V c= Polish-arity W iff V c= W )

proof end;

theorem :: POLNOT_2:14

for T being Polish-language
for U being b₁ -extending Polish-language
for V being full Polish-language of T
for W being full Polish-language of U holds
( V c= W iff W is -closed )

proof end;

definition

let T be Polish-language;
let U be T -extending Polish-language;
let V be full Polish-language of T;
let W be full Polish-language of U;

:: original: -extending
redefine attr W is V -extending means :: POLNOT_2:def 19
Polish-arity V c= Polish-arity W;

compatibility
( W is V -extending iff Polish-arity V c= Polish-arity W ) by Th22;

end;

:: deftheorem defines -extending POLNOT_2:def 19 :
for T being Polish-language
for U being b₁ -extending Polish-language
for V being full Polish-language of T
for W being full Polish-language of U holds
( W is V -extending iff Polish-arity V c= Polish-arity W );

registration

let T be Polish-language;
let U be T -extending Polish-language;
let V be full Polish-language of T;

cluster functional non empty FinSequence-membered antichain-like full (V) for Element of bool (U *);

existence
not for b₁ being full Polish-language of U holds b₁ is (V)

proof end;

end;

definition

let T be Polish-language;
let V be full Polish-language of T;
mode Extension of V is Polish-ext-set of Polish-arity V;

end;

registration

let T be Polish-language;
let V be full Polish-language of T;

cluster non empty FinSequence-membered Polish-arity V -closed antichain-like Polish-arity V -compatible -> for set ;

coherence
for b₁ being Extension of V holds
( b₁ is -closed & b₁ is ( Polish-arity V) ) ;

end;

theorem :: POLNOT_2:15

for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V holds V c= Q

proof end;

definition

let T be Polish-language;
let V be full Polish-language of T;
let Q be Extension of V;

func Polish-ext-complement Q -> Subset of Q equals :: POLNOT_2:def 20
Polish-ext-complement ((Polish-arity V),Q);

coherence
Polish-ext-complement ((Polish-arity V),Q) is Subset of Q ;

end;

:: deftheorem defines Polish-ext-complement POLNOT_2:def 20 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V holds Polish-ext-complement Q = Polish-ext-complement ((Polish-arity V),Q);

definition

let T be Polish-language;
let V be full Polish-language of T;
let Q be Extension of V;

func Polish-ext-domain Q -> T -extending Polish-language equals :: POLNOT_2:def 21
Polish-ext-domain ((Polish-arity V),Q);

coherence
Polish-ext-domain ((Polish-arity V),Q) is T -extending Polish-language

proof end;

end;

:: deftheorem defines Polish-ext-domain POLNOT_2:def 21 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V holds Polish-ext-domain Q = Polish-ext-domain ((Polish-arity V),Q);

definition

let T be Polish-language;
let V be full Polish-language of T;
let Q be Extension of V;

func Polish-ext-arity Q -> Polish-arity-function of Polish-ext-domain Q equals :: POLNOT_2:def 22
Polish-ext-arity ((Polish-arity V),Q);

coherence
Polish-ext-arity ((Polish-arity V),Q) is Polish-arity-function of Polish-ext-domain Q ;

end;

:: deftheorem defines Polish-ext-arity POLNOT_2:def 22 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V holds Polish-ext-arity Q = Polish-ext-arity ((Polish-arity V),Q);

definition

let T be Polish-language;
let V be full Polish-language of T;
let Q be Extension of V;
let F be Formula of Q;

func Polish-ext-head F -> Element of Polish-ext-domain Q equals :: POLNOT_2:def 23
(Polish-ext-domain Q) -head F;

coherence
(Polish-ext-domain Q) -head F is Element of Polish-ext-domain Q

proof end;

end;

:: deftheorem defines Polish-ext-head POLNOT_2:def 23 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V
for F being Formula of Q holds Polish-ext-head F = (Polish-ext-domain Q) -head F;

theorem :: POLNOT_2:16

for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V
for F being Formula of Q st Polish-ext-head F in T holds
Polish-ext-head F = T -head F by Th10;

theorem Th32: :: POLNOT_2:17

for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V
for F being Formula of Q st F is T -headed holds
Polish-ext-head F = T -head F

proof end;

definition

let T be Polish-language;
let V be full Polish-language of T;
let Q be Extension of V;
let t be Element of T;
assume A1: (Polish-arity V) . t = 1 ;

func Polish-unOp (T,Q,t) -> UnOp of Q means :Def15r: :: POLNOT_2:def 24
for p being FinSequence st p in Q holds
it . p = t ^ p;

existence
ex b₁ being UnOp of Q st
for p being FinSequence st p in Q holds
b₁ . p = t ^ p

proof end;

uniqueness
for b₁, b₂ being UnOp of Q st ( for p being FinSequence st p in Q holds
b₁ . p = t ^ p ) & ( for p being FinSequence st p in Q holds
b₂ . p = t ^ p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15r defines Polish-unOp POLNOT_2:def 24 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V
for t being Element of T st (Polish-arity V) . t = 1 holds
for b₅ being UnOp of Q holds
( b₅ = Polish-unOp (T,Q,t) iff for p being FinSequence st p in Q holds
b₅ . p = t ^ p );

definition

let T be Polish-language;
let V be full Polish-language of T;
let Q be Extension of V;
let t be Element of T;
assume A1: (Polish-arity V) . t = 2 ;

func Polish-binOp (T,Q,t) -> BinOp of Q means :Def16r: :: POLNOT_2:def 25
for p, q being FinSequence st p in Q & q in Q holds
it . (p,q) = t ^ (p ^ q);

existence
ex b₁ being BinOp of Q st
for p, q being FinSequence st p in Q & q in Q holds
b₁ . (p,q) = t ^ (p ^ q)

proof end;

uniqueness
for b₁, b₂ being BinOp of Q st ( for p, q being FinSequence st p in Q & q in Q holds
b₁ . (p,q) = t ^ (p ^ q) ) & ( for p, q being FinSequence st p in Q & q in Q holds
b₂ . (p,q) = t ^ (p ^ q) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16r defines Polish-binOp POLNOT_2:def 25 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V
for t being Element of T st (Polish-arity V) . t = 2 holds
for b₅ being BinOp of Q holds
( b₅ = Polish-binOp (T,Q,t) iff for p, q being FinSequence st p in Q & q in Q holds
b₅ . (p,q) = t ^ (p ^ q) );

theorem :: POLNOT_2:18

for K being non trivial Polish-language
for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for F being Formula of M st E . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G

proof end;

theorem :: POLNOT_2:19

for K being non trivial Polish-language
for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for G being Formula of M st E . e = 1 holds
Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e

proof end;

theorem :: POLNOT_2:20

for K being non trivial Polish-language
for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for F being Formula of M st E . e = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H)

proof end;

theorem :: POLNOT_2:21

for K being non trivial Polish-language
for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for G, H being Formula of M st E . e = 2 holds
Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e

proof end;