:: Definition of first order language with arbitrary alphabet. Syntax of terms, atomic formulas and their subterms
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: 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 " {0};
coherence
the adicity of S " {0} is set ;
func OpSymbolsOf S -> set equals :: FOMODEL1:def 3
 the adicity of S " (NAT \ {0});
coherence
the adicity of S " (NAT \ {0}) is set ;
func RelSymbolsOf S -> set equals :: FOMODEL1:def 4
 the adicity of S " (INT \ NAT);
coherence
the adicity of S " (INT \ NAT) 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 " (INT \ {0});
coherence
the adicity of S " (INT \ {0}) 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 " {0};

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

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

:: 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 " (INT \ {0});

:: 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;
func AtomicFormulaSymbolsOf S -> set equals :: FOMODEL1:def 10
(AllSymbolsOf S) \ {(TheNorSymbOf S)};
coherence
(AllSymbolsOf S) \ {(TheNorSymbOf S)} is set ;
func AtomicTermsOf S -> set equals :: FOMODEL1:def 11
1 -tuples_on (LettersOf S);
coherence
1 -tuples_on (LettersOf S) is set ;
attr S is operational means :: FOMODEL1:def 12
 not OpSymbolsOf S is empty ;
attr S is relational means :: FOMODEL1:def 13
 not (RelSymbolsOf S) \ {(TheEqSymbOf S)} is empty ;
end;

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

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

:: 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 (RelSymbolsOf S) \ {(TheEqSymbOf S)} 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
TrivialArity s is Element of INT 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 (S TrivialArity) " {0} -> infinite for set ;
coherence
for b1 being set st b1 = (S TrivialArity) " {0} holds
not b1 is finite
proof end;
end;

Lm1: for S being non degenerated ZeroOneStr holds (S TrivialArity) . 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 . (TheEqSymbOf 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 . (TheEqSymbOf S) = - 2 ) );

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

registration
cluster non degenerated for Language-like ;
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
mode Language is non degenerated eligible Language-like ;
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 (AllSymbolsOf S);
coherence
LettersOf S is non empty Subset of (AllSymbolsOf S) by XBOOLE_1:1;
end;

Lm3: for S being non degenerated Language-like holds TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)}
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 (AllSymbolsOf S);
coherence
AtomicFormulaSymbolsOf S is non empty Subset of (AllSymbolsOf S) ;
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
for S being Language holds
( (LettersOf S) /\ (OpSymbolsOf S) = {} & (TermSymbolsOf S) /\ (LowerCompoundersOf S) = OpSymbolsOf S & (RelSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)} & OwnSymbolsOf S c= AtomicFormulaSymbolsOf S & RelSymbolsOf S c= LowerCompoundersOf S & OpSymbolsOf S c= TermSymbolsOf S & LettersOf S c= TermSymbolsOf S & TermSymbolsOf S c= OwnSymbolsOf S & OpSymbolsOf S c= LowerCompoundersOf S & LowerCompoundersOf S c= AtomicFormulaSymbolsOf S )
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;
cluster own -> ofAtomicFormula for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is own holds
b1 is ofAtomicFormula
proof end;
cluster relational -> low-compounding for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is relational holds
b1 is low-compounding
proof end;
cluster operational -> termal for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is operational holds
b1 is termal
proof end;
cluster literal -> termal for Element of AllSymbolsOf S;
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;
cluster operational -> low-compounding for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is operational holds
b1 is low-compounding
proof end;
cluster low-compounding -> ofAtomicFormula for Element of AllSymbolsOf S;
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;
cluster relational for Element of AllSymbolsOf S;
existence
ex b1 being Element of S st b1 is relational
proof end;
cluster literal for Element of AllSymbolsOf S;
existence
ex b1 being Element of S st b1 is literal
proof end;
end;

registration
let S be Language;
cluster low-compounding termal -> low-compounding operational for Element of AllSymbolsOf S;
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;
cluster ofAtomicFormula for Element of AllSymbolsOf S;
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 ((AllSymbolsOf S) *) equals :: FOMODEL1:def 25
(AllSymbolsOf S) -concatenation ;
coherence
(AllSymbolsOf S) -concatenation is BinOp of ((AllSymbolsOf S) *) ;
end;

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

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

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

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

:: deftheorem defines -firstChar FOMODEL1:def 27 :
for S being Language holds S -firstChar = (AllSymbolsOf S) -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;
cluster S -prefix -> AllSymbolsOf S -prefix for set ;
coherence
for b1 being set st b1 is S -prefix holds
b1 is AllSymbolsOf S -prefix ;
cluster AllSymbolsOf S -prefix -> S -prefix for set ;
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 ((AllSymbolsOf S) *) \ {{}};
end;

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

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

registration
cluster non degenerated eligible -> infinite for Language-like ;
coherence
for b1 being Language holds b1 is infinite
proof end;
end;

registration
let S be Language;
cluster AllSymbolsOf S -> infinite for set ;
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*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } ;
coherence
{ (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( 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*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( 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 (((AllSymbolsOf S) *) \ {{}});
coherence
Compound (s,Strings) is Element of bool (((AllSymbolsOf S) *) \ {{}})
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 ((AllSymbolsOf S) *);
coherence
AtomicTermsOf S is Subset of ((AllSymbolsOf S) *)
proof end;
end;

Lm4: for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}
proof end;

Lm5: for m, n being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n)
proof end;

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

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

theorem Th2: :: FOMODEL1:2
for mm being Element of NAT
for S being Language holds (S -termsOfMaxDepth) . 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 (S -termsOfMaxDepth) . 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 (S -termsOfMaxDepth) . 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 (S -termsOfMaxDepth) . m );

registration
let m be Nat;
let S be Language;
cluster m -termal -> termal for Element of ((AllSymbolsOf S) *) \ {{}};
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 ((AllSymbolsOf S) *));
coherence
S -termsOfMaxDepth is sequence of (bool ((AllSymbolsOf S) *))
proof end;
end;

definition
let S be Language;
:: original: AllTermsOf
redefine func AllTermsOf S -> non empty Subset of ((AllSymbolsOf S) *);
coherence
AllTermsOf S is non empty Subset of ((AllSymbolsOf S) *)
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 (S -termsOfMaxDepth) . m -> non empty ;
coherence
not (S -termsOfMaxDepth) . m is empty
proof end;
end;

registration
let S be Language;
let m be Nat;
cluster -> non empty for Element of (S -termsOfMaxDepth) . m;
coherence
for b1 being Element of (S -termsOfMaxDepth) . 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;
cluster Relation-like omega -defined non empty non zero Function-like finite FinSequence-like FinSubsequence-like countable m -termal for Element of ((AllSymbolsOf S) *) \ {{}};
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 ((AllSymbolsOf S) *) \ {{}};
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 (S -firstChar) . w -> literal for Element of S;
coherence
for b1 being Element of S st b1 = (S -firstChar) . 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 ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . 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 ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
proof end;

registration
let S be Language;
let w be termal string of S;
cluster (S -firstChar) . w -> termal for Element of S;
coherence
for b1 being Element of S st b1 = (S -firstChar) . 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 ((S -firstChar) . t);
coherence
ar ((S -firstChar) . 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 ((S -firstChar) . 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 ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar ((S -firstChar) . w)).| -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
proof end;

Lm9: for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m is S -prefix
proof end;

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

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

registration
let S be Language;
let V be Element of (AllTermsOf S) * ;
cluster (S -multiCat) . V -> Function-like for Relation;
coherence
for b1 being Relation st b1 = (S -multiCat) . 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 (AllTermsOf S) * st phi = <*s*> ^ ((S -multiCat) . 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 (AllTermsOf S) * st phi = <*s*> ^ ((S -multiCat) . V) );

registration
let S be Language;
cluster Relation-like omega -defined non empty non zero Function-like finite FinSequence-like FinSubsequence-like countable 0wff for Element of ((AllSymbolsOf S) *) \ {{}};
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 (S -firstChar) . phi -> relational for Element of S;
coherence
for b1 being Element of S st b1 = (S -firstChar) . 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 (((AllSymbolsOf S) *) \ {{}});
coherence
AtomicFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
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 (AllTermsOf S) * means :Def37: :: FOMODEL1:def 37
( it is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . it) );
existence
ex b1 being Element of (AllTermsOf S) * st
( b1 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b1) )
proof end;
uniqueness
for b1, b2 being Element of (AllTermsOf S) * st b1 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b1) & b2 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . 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 (AllTermsOf S) * holds
( b3 = SubTerms t iff ( b3 is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b3) ) );

registration
let S be Language;
let t be termal string of S;
cluster SubTerms t -> |.(ar t).| -element for Element of (AllTermsOf S) * ;
coherence
for b1 being Element of (AllTermsOf S) * 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 (AllTermsOf S) * ;
coherence
for b1 being Element of (AllTermsOf S) * 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 -> (S -termsOfMaxDepth) . mm -valued for Element of (AllTermsOf S) * ;
coherence
for b1 being Element of (AllTermsOf S) * st b1 = SubTerms t holds
b1 is (S -termsOfMaxDepth) . mm -valued
proof end;
end;

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

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

definition
let S be Language;
:: original: AllTermsOf
redefine func AllTermsOf S -> Element of bool (((AllSymbolsOf S) *) \ {{}});
coherence
AllTermsOf S is Element of bool (((AllSymbolsOf S) *) \ {{}})
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 (AllTermsOf S),((AllTermsOf S) *) means :: FOMODEL1:def 39
 for t being Element of AllTermsOf S holds it . t = SubTerms t;
existence
ex b1 being Function of (AllTermsOf S),((AllTermsOf S) *) st
for t being Element of AllTermsOf S holds b1 . t = SubTerms t
proof end;
uniqueness
for b1, b2 being Function of (AllTermsOf S),((AllTermsOf S) *) 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 (AllTermsOf S),((AllTermsOf S) *) 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 (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (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 (S -termsOfMaxDepth) . nn by Lm6;

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

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 (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)}
proof end;

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

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

registration
let S be Language;
cluster non relational ofAtomicFormula -> termal ofAtomicFormula for Element of AllSymbolsOf S;
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 (AllSymbolsOf S);
coherence
OwnSymbolsOf S is Subset of (AllSymbolsOf S) ;
end;

registration
let S be Language;
cluster non literal termal -> operational termal for Element of AllSymbolsOf S;
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 (AllSymbolsOf S) * )
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 ((AllSymbolsOf S) *)) ;

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;
cluster ar s -> ext-real negative ;
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
( (S -firstChar) . t is operational & SubTerms t <> {} )
proof end;

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

registration
let S be Language;
let W be ((AllSymbolsOf S) *) \ {{}} -valued non empty FinSequence;
cluster (S -multiCat) . W -> non empty for set ;
coherence
for b1 being set st b1 = (S -multiCat) . 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 ((AllSymbolsOf S) *) \ {{}};
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;
cluster non low-compounding own -> literal own for Element of AllSymbolsOf S;
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 (((AllSymbolsOf S) *) \ {{}}));
coherence
S -termsOfMaxDepth is sequence of (bool (((AllSymbolsOf S) *) \ {{}}))
proof end;
end;

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

Lm11: for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) *
proof end;

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

registration
let S be Language;
cluster termal -> TermSymbolsOf S -valued for Element of ((AllSymbolsOf S) *) \ {{}};
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 (AllTermsOf S) \ ((TermSymbolsOf S) *) -> empty for set ;
coherence
for b1 being set st b1 = (AllTermsOf S) \ ((TermSymbolsOf S) *) holds
b1 is empty
proof end;
end;

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

registration
let S be Language;
cluster 0wff -> AtomicFormulaSymbolsOf S -valued for Element of ((AllSymbolsOf S) *) \ {{}};
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 (S -firstChar) . phi0 <> TheEqSymbOf S holds
phi0 is OwnSymbolsOf S -valued
proof end;

registration
cluster non empty strict for Language-like ;
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;
cluster S null -> S -extending for Language-like ;
coherence
for b1 being Language-like st b1 = S null holds
b1 is S -extending ;
end;

registration
let S be Language;
cluster non empty non degenerated non trivial infinite eligible S -extending for Language-like ;
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 (OwnSymbolsOf S1) \ (OwnSymbolsOf S2) -> empty for set ;
coherence
for b1 being set st b1 = (OwnSymbolsOf S1) \ (OwnSymbolsOf S2) 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 ;
cluster S -extending -> non degenerated for 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 ;
cluster S -extending -> eligible for 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) \ (AllSymbolsOf S1))) " {0}) \/ (LettersOf S1) & the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = the adicity of S1 | (OwnSymbolsOf 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 ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0);
coherence
S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -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 ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0);

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

registration
cluster non empty non degenerated non trivial infinite countable eligible for Language-like ;
existence
ex b1 being Language st b1 is countable
proof end;
end;

registration
let S be countable Language;
cluster AllSymbolsOf S -> countable for set ;
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 ((AllSymbolsOf S) *) \ {{}} -> countable for set ;
coherence
for b1 being set st b1 = ((AllSymbolsOf S) *) \ {{}} holds
b1 is countable
proof end;
end;

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

registration
let S be countable Language;
let X be functional set ;
cluster S addLettersNotIn X -> countable for 1-sorted ;
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;
cluster AtomicTermsOf S -> infinite for set ;
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 /\ (LettersOf S2) is infinite holds
ex S1 being Language st
( OwnSymbolsOf S1 = X /\ (OwnSymbolsOf S2) & 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 (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S
proof end;

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