:: Definition of first order language with arbitrary alphabet. Syntax of terms, atomic formulas and their subterms
:: by Marco B. Caminati
::
:: Copyright (c) 2010-2021 Association of Mizar Users

registration
let z be zero Integer;
cluster K327(z) -> zero for Integer;
coherence
for b1 being Integer st b1 = |.z.| holds
b1 is zero
by COMPLEX1:47;
end;

registration
let S be non degenerated ZeroOneStr ;
cluster the carrier of S \ { the OneF of S} -> non empty ;
coherence
not the carrier of S \ { the OneF of S} is empty
;
end;

::########## First-order structure (theory) formalization ###########
::###################### basic definitions ##########################
::#####################################################################
::#####################################################################
definition
attr c1 is strict ;
struct Language-like -> ZeroOneStr ;
aggr Language-like(# carrier, ZeroF, OneF, adicity #) -> Language-like ;
sel adicity c1 -> Function of ( the carrier of c1 \ { the OneF of c1}),INT;
end;

definition
let S be Language-like ;
func AllSymbolsOf S -> set equals :: FOMODEL1:def 1
the carrier of S;
coherence
the carrier of S is set
;
func LettersOf S -> set equals :: FOMODEL1:def 2
the adicity of S " ;
coherence
the adicity of S " is set
;
func OpSymbolsOf S -> set equals :: FOMODEL1:def 3
the adicity of S " ();
coherence
the adicity of S " () is set
;
func RelSymbolsOf S -> set equals :: FOMODEL1:def 4
the adicity of S " ();
coherence
the adicity of S " () is set
;
func TermSymbolsOf S -> set equals :: FOMODEL1:def 5
the adicity of S " NAT;
coherence
the adicity of S " NAT is set
;
func LowerCompoundersOf S -> set equals :: FOMODEL1:def 6
the adicity of S " ();
coherence
the adicity of S " () is set
;
func TheEqSymbOf S -> set equals :: FOMODEL1:def 7
the ZeroF of S;
coherence
the ZeroF of S is set
;
func TheNorSymbOf S -> set equals :: FOMODEL1:def 8
the OneF of S;
coherence
the OneF of S is set
;
func OwnSymbolsOf S -> set equals :: FOMODEL1:def 9
the carrier of S \ { the ZeroF of S, the OneF of S};
coherence
the carrier of S \ { the ZeroF of S, the OneF of S} is set
;
end;

:: deftheorem defines AllSymbolsOf FOMODEL1:def 1 :
for S being Language-like holds AllSymbolsOf S = the carrier of S;

:: deftheorem defines LettersOf FOMODEL1:def 2 :
for S being Language-like holds LettersOf S = the adicity of S " ;

:: deftheorem defines OpSymbolsOf FOMODEL1:def 3 :
for S being Language-like holds OpSymbolsOf S = the adicity of S " ();

:: deftheorem defines RelSymbolsOf FOMODEL1:def 4 :
for S being Language-like holds RelSymbolsOf S = the adicity of S " ();

:: deftheorem defines TermSymbolsOf FOMODEL1:def 5 :
for S being Language-like holds TermSymbolsOf S = the adicity of S " NAT;

:: deftheorem defines LowerCompoundersOf FOMODEL1:def 6 :
for S being Language-like holds LowerCompoundersOf S = the adicity of S " ();

:: deftheorem defines TheEqSymbOf FOMODEL1:def 7 :
for S being Language-like holds TheEqSymbOf S = the ZeroF of S;

:: deftheorem defines TheNorSymbOf FOMODEL1:def 8 :
for S being Language-like holds TheNorSymbOf S = the OneF of S;

:: deftheorem defines OwnSymbolsOf FOMODEL1:def 9 :
for S being Language-like holds OwnSymbolsOf S = the carrier of S \ { the ZeroF of S, the OneF of S};

definition
let S be Language-like ;
mode Element of S is Element of AllSymbolsOf S;
coherence
() \ {()} is set
;
func AtomicTermsOf S -> set equals :: FOMODEL1:def 11
1 -tuples_on ();
coherence
1 -tuples_on () is set
;
attr S is operational means :: FOMODEL1:def 12
not OpSymbolsOf S is empty ;
attr S is relational means :: FOMODEL1:def 13
not () \ {()} is empty ;
end;

:: deftheorem defines AtomicFormulaSymbolsOf FOMODEL1:def 10 :
for S being Language-like holds AtomicFormulaSymbolsOf S = () \ {()};

:: deftheorem defines AtomicTermsOf FOMODEL1:def 11 :
for S being Language-like holds AtomicTermsOf S = 1 -tuples_on ();

:: deftheorem defines operational FOMODEL1:def 12 :
for S being Language-like holds
( S is operational iff not OpSymbolsOf S is empty );

:: deftheorem defines relational FOMODEL1:def 13 :
for S being Language-like holds
( S is relational iff not () \ {()} is empty );

definition
let S be Language-like ;
let s be Element of S;
attr s is literal means :Def14: :: FOMODEL1:def 14
s in LettersOf S;
attr s is low-compounding means :Def15: :: FOMODEL1:def 15
s in LowerCompoundersOf S;
attr s is operational means :Def16: :: FOMODEL1:def 16
s in OpSymbolsOf S;
attr s is relational means :Def17: :: FOMODEL1:def 17
s in RelSymbolsOf S;
attr s is termal means :Def18: :: FOMODEL1:def 18
s in TermSymbolsOf S;
attr s is own means :: FOMODEL1:def 19
s in OwnSymbolsOf S;
attr s is ofAtomicFormula means :Def20: :: FOMODEL1:def 20
s in AtomicFormulaSymbolsOf S;
end;

:: deftheorem Def14 defines literal FOMODEL1:def 14 :
for S being Language-like
for s being Element of S holds
( s is literal iff s in LettersOf S );

:: deftheorem Def15 defines low-compounding FOMODEL1:def 15 :
for S being Language-like
for s being Element of S holds
( s is low-compounding iff s in LowerCompoundersOf S );

:: deftheorem Def16 defines operational FOMODEL1:def 16 :
for S being Language-like
for s being Element of S holds
( s is operational iff s in OpSymbolsOf S );

:: deftheorem Def17 defines relational FOMODEL1:def 17 :
for S being Language-like
for s being Element of S holds
( s is relational iff s in RelSymbolsOf S );

:: deftheorem Def18 defines termal FOMODEL1:def 18 :
for S being Language-like
for s being Element of S holds
( s is termal iff s in TermSymbolsOf S );

:: deftheorem defines own FOMODEL1:def 19 :
for S being Language-like
for s being Element of S holds
( s is own iff s in OwnSymbolsOf S );

:: deftheorem Def20 defines ofAtomicFormula FOMODEL1:def 20 :
for S being Language-like
for s being Element of S holds
( s is ofAtomicFormula iff s in AtomicFormulaSymbolsOf S );

definition
let S be ZeroOneStr ;
let s be Element of the carrier of S \ { the OneF of S};
func TrivialArity s -> Integer equals :Def21: :: FOMODEL1:def 21
- 2 if s = the ZeroF of S
otherwise 0 ;
coherence
( ( s = the ZeroF of S implies - 2 is Integer ) & ( not s = the ZeroF of S implies 0 is Integer ) )
;
consistency
for b1 being Integer holds verum
;
end;

:: deftheorem Def21 defines TrivialArity FOMODEL1:def 21 :
for S being ZeroOneStr
for s being Element of the carrier of S \ { the OneF of S} holds
( ( s = the ZeroF of S implies TrivialArity s = - 2 ) & ( not s = the ZeroF of S implies TrivialArity s = 0 ) );

definition
let S be ZeroOneStr ;
let s be Element of the carrier of S \ { the OneF of S};
:: original: TrivialArity
redefine func TrivialArity s -> Element of INT ;
coherence by INT_1:def 2;
end;

definition
let S be non degenerated ZeroOneStr ;
func S TrivialArity -> Function of ( the carrier of S \ { the OneF of S}),INT means :Def22: :: FOMODEL1:def 22
for s being Element of the carrier of S \ { the OneF of S} holds it . s = TrivialArity s;
existence
ex b1 being Function of ( the carrier of S \ { the OneF of S}),INT st
for s being Element of the carrier of S \ { the OneF of S} holds b1 . s = TrivialArity s
proof end;
uniqueness
for b1, b2 being Function of ( the carrier of S \ { the OneF of S}),INT st ( for s being Element of the carrier of S \ { the OneF of S} holds b1 . s = TrivialArity s ) & ( for s being Element of the carrier of S \ { the OneF of S} holds b2 . s = TrivialArity s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines TrivialArity FOMODEL1:def 22 :
for S being non degenerated ZeroOneStr
for b2 being Function of ( the carrier of S \ { the OneF of S}),INT holds
( b2 = S TrivialArity iff for s being Element of the carrier of S \ { the OneF of S} holds b2 . s = TrivialArity s );

registration
cluster non empty non degenerated non trivial infinite for ZeroOneStr ;
existence
ex b1 being non degenerated ZeroOneStr st b1 is infinite
proof end;
end;

registration
let S be non degenerated infinite ZeroOneStr ;
cluster () " -> infinite for set ;
coherence
for b1 being set st b1 = () " holds
not b1 is finite
proof end;
end;

Lm1: for S being non degenerated ZeroOneStr holds () . the ZeroF of S = - 2
proof end;

definition
let S be Language-like ;
attr S is eligible means :Def23: :: FOMODEL1:def 23
( LettersOf S is infinite & the adicity of S . () = - 2 );
end;

:: deftheorem Def23 defines eligible FOMODEL1:def 23 :
for S being Language-like holds
( S is eligible iff ( LettersOf S is infinite & the adicity of S . () = - 2 ) );

Lm2: ex S being Language-like st
( not S is degenerated & S is eligible )

proof end;

registration
existence
not for b1 being Language-like holds b1 is degenerated
by Lm2;
end;

registration
cluster non empty non degenerated non trivial eligible for Language-like ;
existence
ex b1 being non degenerated Language-like st b1 is eligible
by Lm2;
end;

definition end;

definition
let S be non empty Language-like ;
:: original: AllSymbolsOf
redefine func AllSymbolsOf S -> non empty set ;
coherence
AllSymbolsOf S is non empty set
;
end;

registration
let S be eligible Language-like ;
cluster LettersOf S -> infinite for set ;
coherence
for b1 being set st b1 = LettersOf S holds
not b1 is finite
by Def23;
end;

definition
let S be Language;
:: original: LettersOf
redefine func LettersOf S -> non empty Subset of ();
coherence
LettersOf S is non empty Subset of ()
by XBOOLE_1:1;
end;

Lm3: for S being non degenerated Language-like holds TheEqSymbOf S in () \ {()}
proof end;

registration
let S be Language;
cluster TheEqSymbOf S -> relational for Element of S;
coherence
for b1 being Element of S st b1 = TheEqSymbOf S holds
b1 is relational
proof end;
end;

definition
let S be non degenerated Language-like ;
:: original: AtomicFormulaSymbolsOf
redefine func AtomicFormulaSymbolsOf S -> non empty Subset of ();
coherence
AtomicFormulaSymbolsOf S is non empty Subset of ()
;
end;

definition
let S be Language;
:: original: TheEqSymbOf
redefine func TheEqSymbOf S -> Element of S;
coherence
TheEqSymbOf S is Element of S
;
end;

theorem Th1: :: FOMODEL1:1
proof end;

registration
let S be Language;
cluster TermSymbolsOf S -> non empty for set ;
coherence
for b1 being set st b1 = TermSymbolsOf S holds
not b1 is empty
proof end;
coherence
for b1 being Element of S st b1 is own holds
b1 is ofAtomicFormula
proof end;
coherence
for b1 being Element of S st b1 is relational holds
b1 is low-compounding
proof end;
coherence
for b1 being Element of S st b1 is operational holds
b1 is termal
proof end;
coherence
for b1 being Element of S st b1 is literal holds
b1 is termal
proof end;
cluster termal -> own for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is termal holds
b1 is own
proof end;
coherence
for b1 being Element of S st b1 is operational holds
b1 is low-compounding
proof end;
coherence
for b1 being Element of S st b1 is low-compounding holds
b1 is ofAtomicFormula
;
cluster termal -> non relational for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is termal holds
not b1 is relational
proof end;
cluster literal -> non relational for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is literal holds
not b1 is relational
;
cluster literal -> non operational for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is literal holds
not b1 is operational
proof end;
end;

registration
let S be Language;
existence
ex b1 being Element of S st b1 is relational
proof end;
existence
ex b1 being Element of S st b1 is literal
proof end;
end;

registration
let S be Language;
coherence
for b1 being low-compounding Element of S st b1 is termal holds
b1 is operational
proof end;
end;

registration
let S be Language;
existence
ex b1 being Element of S st b1 is ofAtomicFormula
proof end;
end;

definition
let S be Language;
let s be ofAtomicFormula Element of S;
func ar s -> Element of INT equals :: FOMODEL1:def 24
the adicity of S . s;
coherence
the adicity of S . s is Element of INT
proof end;
end;

:: deftheorem defines ar FOMODEL1:def 24 :
for S being Language
for s being ofAtomicFormula Element of S holds ar s = the adicity of S . s;

registration
let S be Language;
let s be literal Element of S;
cluster ar s -> zero for number ;
coherence
for b1 being number st b1 = ar s holds
b1 is zero
proof end;
end;

definition
let S be Language;
func S -cons -> BinOp of (() *) equals :: FOMODEL1:def 25
() -concatenation ;
coherence
() -concatenation is BinOp of (() *)
;
end;

:: deftheorem defines -cons FOMODEL1:def 25 :
for S being Language holds S -cons = () -concatenation ;

definition
let S be Language;
func S -multiCat -> Function of ((() *) *),(() *) equals :: FOMODEL1:def 26
() -multiCat ;
coherence
() -multiCat is Function of ((() *) *),(() *)
;
end;

:: deftheorem defines -multiCat FOMODEL1:def 26 :
for S being Language holds S -multiCat = () -multiCat ;

definition
let S be Language;
func S -firstChar -> Function of ((() *) \ ),() equals :: FOMODEL1:def 27
() -firstChar ;
coherence
() -firstChar is Function of ((() *) \ ),()
;
end;

:: deftheorem defines -firstChar FOMODEL1:def 27 :
for S being Language holds S -firstChar = () -firstChar ;

definition
let S be Language;
let X be set ;
attr X is S -prefix means :Def28: :: FOMODEL1:def 28
X is AllSymbolsOf S -prefix ;
end;

:: deftheorem Def28 defines -prefix FOMODEL1:def 28 :
for S being Language
for X being set holds
( X is S -prefix iff X is AllSymbolsOf S -prefix );

registration
let S be Language;
coherence
for b1 being set st b1 is S -prefix holds
b1 is AllSymbolsOf S -prefix
;
coherence
for b1 being set st b1 is AllSymbolsOf S -prefix holds
b1 is S -prefix
;
end;

definition
let S be Language;
mode string of S is Element of (() *) \ ;
end;

registration
let S be Language;
cluster (() *) \ -> non empty for set ;
coherence
for b1 being set st b1 = (() *) \ holds
not b1 is empty
;
end;

registration
let S be Language;
cluster -> non empty for Element of (() *) \ ;
coherence
for b1 being string of S holds not b1 is empty
;
end;

registration
coherence
for b1 being Language holds b1 is infinite
proof end;
end;

registration
let S be Language;
coherence
for b1 being set st b1 = AllSymbolsOf S holds
not b1 is finite
;
end;

definition
let S be Language;
let s be ofAtomicFormula Element of S;
let Strings be set ;
func Compound (s,Strings) -> set equals :: FOMODEL1:def 29
{ (<*s*> ^ (() . StringTuple)) where StringTuple is Element of (() *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } ;
coherence
{ (<*s*> ^ (() . StringTuple)) where StringTuple is Element of (() *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } is set
;
end;

:: deftheorem defines Compound FOMODEL1:def 29 :
for S being Language
for s being ofAtomicFormula Element of S
for Strings being set holds Compound (s,Strings) = { (<*s*> ^ (() . StringTuple)) where StringTuple is Element of (() *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } ;

definition
let S be Language;
let s be ofAtomicFormula Element of S;
let Strings be set ;
:: original: Compound
redefine func Compound (s,Strings) -> Element of bool ((() *) \ );
coherence
Compound (s,Strings) is Element of bool ((() *) \ )
proof end;
end;

definition
let S be Language;
func S -termsOfMaxDepth -> Function means :Def30: :: FOMODEL1:def 30
( dom it = NAT & it . 0 = AtomicTermsOf S & ( for n being Nat holds it . (n + 1) = (union { (Compound (s,(it . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (it . n) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = AtomicTermsOf S & ( for n being Nat holds b1 . (n + 1) = (union { (Compound (s,(b1 . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = AtomicTermsOf S & ( for n being Nat holds b1 . (n + 1) = (union { (Compound (s,(b1 . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b1 . n) ) & dom b2 = NAT & b2 . 0 = AtomicTermsOf S & ( for n being Nat holds b2 . (n + 1) = (union { (Compound (s,(b2 . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def30 defines -termsOfMaxDepth FOMODEL1:def 30 :
for S being Language
for b2 being Function holds
( b2 = S -termsOfMaxDepth iff ( dom b2 = NAT & b2 . 0 = AtomicTermsOf S & ( for n being Nat holds b2 . (n + 1) = (union { (Compound (s,(b2 . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b2 . n) ) ) );

definition
let S be Language;
:: original: AtomicTermsOf
redefine func AtomicTermsOf S -> Subset of (() *);
coherence
AtomicTermsOf S is Subset of (() *)
proof end;
end;

Lm4: for m being Nat
for S being Language holds () . m c= (() *) \

proof end;

Lm5: for m, n being Nat
for S being Language holds () . m c= () . (m + n)

proof end;

definition
let S be Language;
func AllTermsOf S -> set equals :: FOMODEL1:def 31
union ();
coherence
union () is set
;
end;

:: deftheorem defines AllTermsOf FOMODEL1:def 31 :
for S being Language holds AllTermsOf S = union ();

theorem Th2: :: FOMODEL1:2
for mm being Element of NAT
for S being Language holds () . mm c= AllTermsOf S
proof end;

Lm6: for x being set
for S being Language st x in AllTermsOf S holds
ex nn being Element of NAT st x in () . nn

proof end;

definition
let S be Language;
let w be string of S;
attr w is termal means :Def32: :: FOMODEL1:def 32
w in AllTermsOf S;
end;

:: deftheorem Def32 defines termal FOMODEL1:def 32 :
for S being Language
for w being string of S holds
( w is termal iff w in AllTermsOf S );

definition
let m be Nat;
let S be Language;
let w be string of S;
attr w is m -termal means :Def33: :: FOMODEL1:def 33
w in () . m;
end;

:: deftheorem Def33 defines -termal FOMODEL1:def 33 :
for m being Nat
for S being Language
for w being string of S holds
( w is m -termal iff w in () . m );

registration
let m be Nat;
let S be Language;
cluster m -termal -> termal for Element of (() *) \ ;
coherence
for b1 being string of S st b1 is m -termal holds
b1 is termal
proof end;
end;

definition
let S be Language;
:: original: -termsOfMaxDepth
redefine func S -termsOfMaxDepth -> sequence of (bool (() *));
coherence
S -termsOfMaxDepth is sequence of (bool (() *))
proof end;
end;

definition
let S be Language;
:: original: AllTermsOf
redefine func AllTermsOf S -> non empty Subset of (() *);
coherence
AllTermsOf S is non empty Subset of (() *)
proof end;
end;

registration
let S be Language;
cluster AllTermsOf S -> non empty for set ;
coherence
for b1 being set st b1 = AllTermsOf S holds
not b1 is empty
;
end;

registration
let S be Language;
let m be Nat;
cluster () . m -> non empty ;
coherence
not () . m is empty
proof end;
end;

registration
let S be Language;
let m be Nat;
cluster -> non empty for Element of () . m;
coherence
for b1 being Element of () . m holds not b1 is empty
proof end;
end;

registration
let S be Language;
cluster -> non empty for Element of AllTermsOf S;
coherence
for b1 being Element of AllTermsOf S holds not b1 is empty
proof end;
end;

registration
let m be Nat;
let S be Language;
existence
ex b1 being string of S st b1 is m -termal
proof end;
end;

registration
let S be Language;
cluster 0 -termal -> 1 -element for Element of (() *) \ ;
coherence
for b1 being string of S st b1 is 0 -termal holds
b1 is 1 -element
proof end;
end;

registration
let S be Language;
let w be 0 -termal string of S;
cluster () . w -> literal for Element of S;
coherence
for b1 being Element of S st b1 = () . w holds
b1 is literal
proof end;
end;

Lm7: for mm being Element of NAT
for S being Language
for w being b1 + 1 -termal string of S st not w is mm -termal holds
ex s being termal Element of S ex T being Element of (() . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ (() . T) )

proof end;

Lm8: for mm being Element of NAT
for S being Language
for w being b1 + 1 -termal string of S ex s being termal Element of S ex T being Element of (() . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ (() . T) )

proof end;

registration
let S be Language;
let w be termal string of S;
cluster () . w -> termal for Element of S;
coherence
for b1 being Element of S st b1 = () . w holds
b1 is termal
proof end;
end;

definition
let S be Language;
let t be termal string of S;
func ar t -> Element of INT equals :: FOMODEL1:def 34
ar (() . t);
coherence
ar (() . t) is Element of INT
;
end;

:: deftheorem defines ar FOMODEL1:def 34 :
for S being Language
for t being termal string of S holds ar t = ar (() . t);

theorem Th3: :: FOMODEL1:3
for mm being Element of NAT
for S being Language
for w being b1 + 1 -termal string of S ex T being Element of (() . mm) * st
( T is |.(ar (() . w)).| -element & w = <*(() . w)*> ^ (() . T) )
proof end;

Lm9: for m being Nat
for S being Language holds () . m is S -prefix

proof end;

registration
let S be Language;
let m be Nat;
cluster () . m -> S -prefix for set ;
coherence
for b1 being set st b1 = () . m holds
b1 is S -prefix
by Lm9;
end;

registration
let S be Language;
let V be Element of () * ;
cluster () . V -> Relation-like for set ;
coherence
for b1 being set st b1 = () . V holds
b1 is Relation-like
;
end;

registration
let S be Language;
let V be Element of () * ;
cluster () . V -> Function-like for Relation;
coherence
for b1 being Relation st b1 = () . V holds
b1 is Function-like
;
end;

definition
let S be Language;
let phi be string of S;
attr phi is 0wff means :Def35: :: FOMODEL1:def 35
ex s being relational Element of S ex V being |.(ar b1).| -element Element of () * st phi = <*s*> ^ (() . V);
end;

:: deftheorem Def35 defines 0wff FOMODEL1:def 35 :
for S being Language
for phi being string of S holds
( phi is 0wff iff ex s being relational Element of S ex V being |.(ar b3).| -element Element of () * st phi = <*s*> ^ (() . V) );

registration
let S be Language;
existence
ex b1 being string of S st b1 is 0wff
proof end;
end;

registration
let S be Language;
let phi be 0wff string of S;
cluster () . phi -> relational for Element of S;
coherence
for b1 being Element of S st b1 = () . phi holds
b1 is relational
proof end;
end;

definition
let S be Language;
func AtomicFormulasOf S -> set equals :: FOMODEL1:def 36
{ phi where phi is string of S : phi is 0wff } ;
coherence
{ phi where phi is string of S : phi is 0wff } is set
;
end;

:: deftheorem defines AtomicFormulasOf FOMODEL1:def 36 :
for S being Language holds AtomicFormulasOf S = { phi where phi is string of S : phi is 0wff } ;

definition
let S be Language;
:: original: AtomicFormulasOf
redefine func AtomicFormulasOf S -> Subset of ((() *) \ );
coherence
AtomicFormulasOf S is Subset of ((() *) \ )
proof end;
end;

registration
let S be Language;
cluster AtomicFormulasOf S -> non empty for set ;
coherence
for b1 being set st b1 = AtomicFormulasOf S holds
not b1 is empty
proof end;
end;

registration
let S be Language;
cluster -> 0wff for Element of AtomicFormulasOf S;
coherence
for b1 being Element of AtomicFormulasOf S holds b1 is 0wff
proof end;
end;

Lm10: for S being Language holds AllTermsOf S is S -prefix
proof end;

registration
let S be Language;
cluster AllTermsOf S -> S -prefix for set ;
coherence
for b1 being set st b1 = AllTermsOf S holds
b1 is S -prefix
by Lm10;
end;

definition
let S be Language;
let t be termal string of S;
func SubTerms t -> Element of () * means :Def37: :: FOMODEL1:def 37
( it is |.(ar (() . t)).| -element & t = <*(() . t)*> ^ (() . it) );
existence
ex b1 being Element of () * st
( b1 is |.(ar (() . t)).| -element & t = <*(() . t)*> ^ (() . b1) )
proof end;
uniqueness
for b1, b2 being Element of () * st b1 is |.(ar (() . t)).| -element & t = <*(() . t)*> ^ (() . b1) & b2 is |.(ar (() . t)).| -element & t = <*(() . t)*> ^ (() . b2) holds
b1 = b2
proof end;
end;

:: deftheorem Def37 defines SubTerms FOMODEL1:def 37 :
for S being Language
for t being termal string of S
for b3 being Element of () * holds
( b3 = SubTerms t iff ( b3 is |.(ar (() . t)).| -element & t = <*(() . t)*> ^ (() . b3) ) );

registration
let S be Language;
let t be termal string of S;
cluster SubTerms t -> |.(ar t).| -element for Element of () * ;
coherence
for b1 being Element of () * st b1 = SubTerms t holds
b1 is |.(ar t).| -element
by Def37;
end;

registration
let S be Language;
let t0 be 0 -termal string of S;
cluster SubTerms t0 -> empty for Element of () * ;
coherence
for b1 being Element of () * st b1 = SubTerms t0 holds
b1 is empty
proof end;
end;

registration
let mm be Element of NAT ;
let S be Language;
let t be mm + 1 -termal string of S;
cluster SubTerms t -> () . mm -valued for Element of () * ;
coherence
for b1 being Element of () * st b1 = SubTerms t holds
b1 is () . mm -valued
proof end;
end;

definition
let S be Language;
let phi be 0wff string of S;
func SubTerms phi -> |.(ar (() . phi)).| -element Element of () * means :Def38: :: FOMODEL1:def 38
phi = <*(() . phi)*> ^ (() . it);
existence
ex b1 being |.(ar (() . phi)).| -element Element of () * st phi = <*(() . phi)*> ^ (() . b1)
proof end;
uniqueness
for b1, b2 being |.(ar (() . phi)).| -element Element of () * st phi = <*(() . phi)*> ^ (() . b1) & phi = <*(() . phi)*> ^ (() . b2) holds
b1 = b2
proof end;
end;

:: deftheorem Def38 defines SubTerms FOMODEL1:def 38 :
for S being Language
for phi being 0wff string of S
for b3 being |.(ar (() . b2)).| -element Element of () * holds
( b3 = SubTerms phi iff phi = <*(() . phi)*> ^ (() . b3) );

registration
let S be Language;
let phi be 0wff string of S;
cluster SubTerms phi -> |.(ar (() . phi)).| -element for FinSequence;
coherence
for b1 being FinSequence st b1 = SubTerms phi holds
b1 is |.(ar (() . phi)).| -element
;
end;

definition
let S be Language;
:: original: AllTermsOf
redefine func AllTermsOf S -> Element of bool ((() *) \ );
coherence
AllTermsOf S is Element of bool ((() *) \ )
proof end;
end;

registration
let S be Language;
cluster -> termal for Element of AllTermsOf S;
coherence
for b1 being Element of AllTermsOf S holds b1 is termal
;
end;

definition
let S be Language;
func S -subTerms -> Function of (),(() *) means :: FOMODEL1:def 39
for t being Element of AllTermsOf S holds it . t = SubTerms t;
existence
ex b1 being Function of (),(() *) st
for t being Element of AllTermsOf S holds b1 . t = SubTerms t
proof end;
uniqueness
for b1, b2 being Function of (),(() *) st ( for t being Element of AllTermsOf S holds b1 . t = SubTerms t ) & ( for t being Element of AllTermsOf S holds b2 . t = SubTerms t ) holds
b1 = b2
proof end;
end;

:: deftheorem defines -subTerms FOMODEL1:def 39 :
for S being Language
for b2 being Function of (),(() *) holds
( b2 = S -subTerms iff for t being Element of AllTermsOf S holds b2 . t = SubTerms t );

theorem :: FOMODEL1:4
for m, n being Nat
for S being Language holds () . m c= () . (m + n) by Lm5;

theorem :: FOMODEL1:5
for x being set
for S being Language st x in AllTermsOf S holds
ex nn being Element of NAT st x in () . nn by Lm6;

theorem :: FOMODEL1:6
for S being Language holds AllTermsOf S c= (() *) \ ;

theorem :: FOMODEL1:7
for S being Language holds AllTermsOf S is S -prefix ;

theorem :: FOMODEL1:8
for x being set
for S being Language st x in AllTermsOf S holds
x is string of S ;

theorem :: FOMODEL1:9
for S being Language holds \ () = {()}
proof end;

theorem :: FOMODEL1:10
for S being Language holds () \ () = OpSymbolsOf S by FUNCT_1:69;

theorem Th11: :: FOMODEL1:11
for S being Language holds \ () = TermSymbolsOf S
proof end;

registration
let S be Language;
coherence
for b1 being ofAtomicFormula Element of S st not b1 is relational holds
b1 is termal
proof end;
end;

definition
let S be Language;
:: original: OwnSymbolsOf
redefine func OwnSymbolsOf S -> Subset of ();
coherence
OwnSymbolsOf S is Subset of ()
;
end;

registration
let S be Language;
coherence
for b1 being termal Element of S st not b1 is literal holds
b1 is operational
proof end;
end;

theorem Th12: :: FOMODEL1:12
for x being set
for S being Language holds
( x is string of S iff x is non empty Element of () * )
proof end;

theorem :: FOMODEL1:13
for x being set
for S being Language holds
( x is string of S iff x is non empty FinSequence of AllSymbolsOf S ) by Th12;

theorem :: FOMODEL1:14
for S being Language holds S -termsOfMaxDepth is sequence of (bool (() *)) ;

registration
let S be Language;
cluster -> literal for Element of LettersOf S;
coherence
for b1 being Element of LettersOf S holds b1 is literal
;
end;

registration
let S be Language;
cluster TheNorSymbOf S -> non low-compounding for Element of S;
coherence
for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is low-compounding
proof end;
end;

registration
let S be Language;
cluster TheNorSymbOf S -> non own for Element of S;
coherence
for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is own
proof end;
end;

theorem :: FOMODEL1:15
for S being Language
for s being Element of S st s <> TheNorSymbOf S & s <> TheEqSymbOf S holds
s in OwnSymbolsOf S
proof end;

definition
let S be Language;
let t be termal string of S;
func Depth t -> Nat means :Def40: :: FOMODEL1:def 40
( t is it -termal & ( for n being Nat st t is n -termal holds
it <= n ) );
existence
ex b1 being Nat st
( t is b1 -termal & ( for n being Nat st t is n -termal holds
b1 <= n ) )
proof end;
uniqueness
for b1, b2 being Nat st t is b1 -termal & ( for n being Nat st t is n -termal holds
b1 <= n ) & t is b2 -termal & ( for n being Nat st t is n -termal holds
b2 <= n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def40 defines Depth FOMODEL1:def 40 :
for S being Language
for t being termal string of S
for b3 being Nat holds
( b3 = Depth t iff ( t is b3 -termal & ( for n being Nat st t is n -termal holds
b3 <= n ) ) );

registration
let S be Language;
let m0 be zero number ;
let t be m0 -termal string of S;
cluster Depth t -> zero for number ;
coherence
for b1 being number st b1 = Depth t holds
b1 is zero
by Def40;
end;

registration
let S be Language;
let s be low-compounding Element of S;
cluster ar s -> non zero for number ;
coherence
for b1 being number st b1 = ar s holds
not b1 is zero
proof end;
end;

registration
let S be Language;
let s be termal Element of S;
cluster ar s -> non negative for ExtReal;
coherence
for b1 being ExtReal st b1 = ar s holds
not b1 is negative
proof end;
end;

registration
let S be Language;
let s be relational Element of S;
coherence
( ar s is negative & ar s is ext-real )
proof end;
end;

theorem Th16: :: FOMODEL1:16
for S being Language
for t being termal string of S st not t is 0 -termal holds
( () . t is operational & SubTerms t <> {} )
proof end;

registration
let S be Language;
coherence
for b1 being Function st b1 = S -multiCat holds
b1 is FinSequence-yielding
;
end;

registration
let S be Language;
let W be (() *) \ -valued non empty FinSequence;
cluster () . W -> non empty for set ;
coherence
for b1 being set st b1 = () . W holds
not b1 is empty
proof end;
end;

registration
let S be Language;
let l be literal Element of S;
cluster <*l*> -> 0 -termal for string of S;
coherence
for b1 being string of S st b1 = <*l*> holds
b1 is 0 -termal
proof end;
end;

registration
let S be Language;
let m, n be Nat;
cluster m + (0 * n) -termal -> m + n -termal for Element of (() *) \ ;
coherence
for b1 being string of S st b1 is m + (0 * n) -termal holds
b1 is m + n -termal
proof end;
end;

registration
let S be Language;
coherence
for b1 being own Element of S st not b1 is low-compounding holds
b1 is literal
proof end;
end;

registration
let S be Language;
let t be termal string of S;
cluster SubTerms t -> (rng t) * -valued for Relation;
coherence
for b1 being Relation st b1 = SubTerms t holds
b1 is (rng t) * -valued
proof end;
end;

registration
let S be Language;
let phi0 be 0wff string of S;
cluster SubTerms phi0 -> (rng phi0) * -valued for Relation;
coherence
for b1 being Relation st b1 = SubTerms phi0 holds
b1 is (rng phi0) * -valued
proof end;
end;

definition
let S be Language;
:: original: -termsOfMaxDepth
redefine func S -termsOfMaxDepth -> sequence of (bool ((() *) \ ));
coherence
S -termsOfMaxDepth is sequence of (bool ((() *) \ ))
proof end;
end;

registration
let S be Language;
let mm be Element of NAT ;
coherence
for b1 being set st b1 = () . mm holds
b1 is with_non-empty_elements
;
end;

Lm11: for m being Nat
for S being Language holds () . m c= () *

proof end;

registration
let S be Language;
let m be Nat;
let t be termal string of S;
cluster t null m -> () + m -termal for string of S;
coherence
for b1 being string of S st b1 = t null m holds
b1 is () + m -termal
proof end;
end;

registration
let S be Language;
cluster termal -> TermSymbolsOf S -valued for Element of (() *) \ ;
coherence
for b1 being string of S st b1 is termal holds
b1 is TermSymbolsOf S -valued
proof end;
end;

registration
let S be Language;
cluster () \ (() *) -> empty for set ;
coherence
for b1 being set st b1 = () \ (() *) holds
b1 is empty
proof end;
end;

registration
let S be Language;
let phi0 be 0wff string of S;
cluster SubTerms phi0 -> () * -valued |.(ar (() . phi0)).| -element ;
coherence
SubTerms phi0 is () * -valued
proof end;
end;

registration
let S be Language;
coherence
for b1 being string of S st b1 is 0wff holds
b1 is AtomicFormulaSymbolsOf S -valued
proof end;
end;

registration
let S be Language;
cluster OwnSymbolsOf S -> non empty for set ;
coherence
for b1 being set st b1 = OwnSymbolsOf S holds
not b1 is empty
;
end;

theorem :: FOMODEL1:17
for S being Language
for phi0 being 0wff string of S st () . phi0 <> TheEqSymbOf S holds
phi0 is OwnSymbolsOf S -valued
proof end;

registration
existence
ex b1 being Language-like st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
let S1, S2 be Language-like ;
attr S2 is S1 -extending means :Def41: :: FOMODEL1:def 41
( the adicity of S1 c= the adicity of S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 );
end;

:: deftheorem Def41 defines -extending FOMODEL1:def 41 :
for S1, S2 being Language-like holds
( S2 is S1 -extending iff ( the adicity of S1 c= the adicity of S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 ) );

registration
let S be Language;
coherence
for b1 being Language-like st b1 = S null holds
b1 is S -extending
;
end;

registration
let S be Language;
existence
ex b1 being Language st b1 is S -extending
proof end;
end;

registration
let S1 be Language;
let S2 be S1 -extending Language;
cluster () \ () -> empty for set ;
coherence
for b1 being set st b1 = () \ () holds
b1 is empty
proof end;
end;

definition
let f be INT -valued Function;
let L be non empty Language-like ;
set C = the carrier of L;
set z = the ZeroF of L;
set o = the OneF of L;
set a = the adicity of L;
set X = dom f;
set g = f | ((dom f) \ { the OneF of L});
set a1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L;
set C1 = the carrier of L \/ (dom f);
func L extendWith f -> non empty strict Language-like means :Def42: :: FOMODEL1:def 42
( the adicity of it = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of it = the ZeroF of L & the OneF of it = the OneF of L );
existence
ex b1 being non empty strict Language-like st
( the adicity of b1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b1 = the ZeroF of L & the OneF of b1 = the OneF of L )
proof end;
uniqueness
for b1, b2 being non empty strict Language-like st the adicity of b1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b1 = the ZeroF of L & the OneF of b1 = the OneF of L & the adicity of b2 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b2 = the ZeroF of L & the OneF of b2 = the OneF of L holds
b1 = b2
proof end;
end;

:: deftheorem Def42 defines extendWith FOMODEL1:def 42 :
for f being INT -valued Function
for L being non empty Language-like
for b3 being non empty strict Language-like holds
( b3 = L extendWith f iff ( the adicity of b3 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b3 = the ZeroF of L & the OneF of b3 = the OneF of L ) );

registration
let S be non empty Language-like ;
let f be INT -valued Function;
cluster S extendWith f -> non empty strict S -extending for non empty strict Language-like ;
coherence
for b1 being non empty strict Language-like st b1 = S extendWith f holds
b1 is S -extending
proof end;
end;

registration
let S be non degenerated Language-like ;
coherence
for b1 being Language-like st b1 is S -extending holds
not b1 is degenerated
proof end;
end;

registration
let S be eligible Language-like ;
coherence
for b1 being Language-like st b1 is S -extending holds
b1 is eligible
proof end;
end;

registration
let E be empty Relation;
let X be set ;
cluster X | E -> empty ;
coherence
X | E is empty
by RELAT_1:107;
end;

Lm12: for S1 being non empty Language-like
for f being INT -valued Function holds
( LettersOf (S1 extendWith f) = ((f | ((dom f) \ ())) " ) \/ () & the adicity of (S1 extendWith f) | () = the adicity of S1 | () )

proof end;

registration
let X be set ;
let m be Integer;
cluster X --> m -> INT -valued for Function;
coherence
for b1 being Function st b1 = X --> m holds
b1 is INT -valued
proof end;
end;

definition
let S be Language;
let X be functional set ;
func S addLettersNotIn X -> S -extending Language equals :: FOMODEL1:def 43
S extendWith (((() \/ ()) -freeCountableSet) --> 0);
coherence
S extendWith (((() \/ ()) -freeCountableSet) --> 0) is S -extending Language
;
end;

:: deftheorem defines addLettersNotIn FOMODEL1:def 43 :
for S being Language
for X being functional set holds S addLettersNotIn X = S extendWith (((() \/ ()) -freeCountableSet) --> 0);

registration
let S1 be Language;
let X be functional set ;
cluster (LettersOf ()) \ () -> infinite for set ;
coherence
for b1 being set st b1 = (LettersOf ()) \ () holds
not b1 is finite
proof end;
end;

registration
existence
ex b1 being Language st b1 is countable
proof end;
end;

registration
let S be countable Language;
coherence
for b1 being set st b1 = AllSymbolsOf S holds
b1 is countable
by ORDERS_4:def 2;
end;

registration
let S be countable Language;
cluster (() *) \ -> countable for set ;
coherence
for b1 being set st b1 = (() *) \ holds
b1 is countable
proof end;
end;

registration
let L be non empty Language-like ;
let f be INT -valued Function;
cluster (AllSymbolsOf ()) \+\ ((dom f) \/ ()) -> empty for set ;
coherence
for b1 being set st b1 = (AllSymbolsOf ()) \+\ ((dom f) \/ ()) holds
b1 is empty
proof end;
end;

registration
let S be countable Language;
let X be functional set ;
coherence
for b1 being 1-sorted st b1 = S addLettersNotIn X holds
b1 is countable
proof end;
end;

definition
let S be ZeroOneStr ;
redefine attr S is degenerated means :Def44: :: FOMODEL1:def 44
the ZeroF of S = the OneF of S;
compatibility
( S is degenerated iff the ZeroF of S = the OneF of S )
;
end;

:: deftheorem Def44 defines degenerated FOMODEL1:def 44 :
for S being ZeroOneStr holds
( S is degenerated iff the ZeroF of S = the OneF of S );

registration
let S be Language;
coherence
for b1 being set st b1 = AtomicTermsOf S holds
not b1 is finite
proof end;
end;

theorem :: FOMODEL1:18
for X being set
for S2 being Language st X /\ () is infinite holds
ex S1 being Language st
( OwnSymbolsOf S1 = X /\ () & S2 is S1 -extending )
proof end;

definition
let S be Language;
let w1, w2 be string of S;
:: original: ^
redefine func w1 ^ w2 -> string of S;
coherence
w1 ^ w2 is string of S
proof end;
end;

definition
let S be Language;
let s be Element of S;
:: original: <*
redefine func <*s*> -> string of S;
coherence
<*s*> is string of S
proof end;
end;

Lm13: for S being Language
for t1, t2 being termal string of S holds (<*()*> ^ t1) ^ t2 is 0wff string of S

proof end;

registration
let S be Language;
let t1, t2 be termal string of S;
cluster (<*()*> ^ t1) ^ t2 -> 0wff for string of S;
coherence
for b1 being string of S st b1 = (<*()*> ^ t1) ^ t2 holds
b1 is 0wff
by Lm13;
end;