:: 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-2011 Association of Mizar Users


begin

registration
let z be zero integer number ;
cluster K320(z) -> zero integer integer number ;
coherence
for b1 being integer number st b1 = abs z holds
b1 is empty by COMPLEX1:133;
end;

registration
cluster complex real integer ext-real negative set ;
existence
ex b1 being real number st
( b1 is negative & b1 is integer )
proof end;
cluster integer positive -> natural integer set ;
coherence
for b1 being integer number st b1 is positive holds
b1 is natural ;
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
proof end;
end;

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 :DefLiteral: :: FOMODEL1:def 14
s in LettersOf S;
attr s is low-compounding means :DefLowCompounding: :: FOMODEL1:def 15
s in LowerCompoundersOf S;
attr s is operational means :DefOperational: :: FOMODEL1:def 16
s in OpSymbolsOf S;
attr s is relational means :DefRelational: :: FOMODEL1:def 17
s in RelSymbolsOf S;
attr s is termal means :DefTermal0: :: FOMODEL1:def 18
s in TermSymbolsOf S;
attr s is own means :DefOwn: :: FOMODEL1:def 19
s in OwnSymbolsOf S;
attr s is ofAtomicFormula means :DefOfAtomicFormula: :: FOMODEL1:def 20
s in AtomicFormulaSymbolsOf S;
end;

:: deftheorem DefLiteral 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 DefLowCompounding 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 DefOperational 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 DefRelational 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 DefTermal0 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 DefOwn 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 DefOfAtomicFormula 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 number equals :DefTrivialArity1: :: FOMODEL1:def 21
 - 2 if s = the ZeroF of S
otherwise 0 ;
coherence
( ( s = the ZeroF of S implies - 2 is integer number ) & ( not s = the ZeroF of S implies 0 is integer number ) ) ;
consistency
for b1 being integer number holds verum ;
end;

:: deftheorem DefTrivialArity1 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 :DefTrivialArity2: :: 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 DefTrivialArity2 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 ZeroOneStr ;
existence
not for b1 being non degenerated ZeroOneStr holds b1 is finite
proof end;
end;

registration
let S be non degenerated infinite ZeroOneStr ;
cluster (S TrivialArity) " {0} -> infinite ;
coherence
not (S TrivialArity) " {0} is finite
proof end;
end;

Lm6: 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 :DefEligible: :: FOMODEL1:def 23
( not LettersOf S is finite & the adicity of S . (TheEqSymbOf S) = - 2 );
end;

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

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

registration
cluster non degenerated Language-like ;
existence
not for b1 being Language-like holds b1 is degenerated by Lm7;
end;

registration
cluster non empty non degenerated non trivial eligible Language-like ;
existence
ex b1 being non degenerated Language-like st b1 is eligible by Lm7;
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 ;
coherence
not LettersOf S is finite by DefEligible;
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;

Lm5: 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 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 non degenerated Language-like ;
:: original: TheEqSymbOf
redefine func TheEqSymbOf S -> Element of AtomicFormulaSymbolsOf S;
coherence
TheEqSymbOf S is Element of AtomicFormulaSymbolsOf S by Lm5;
end;

theorem Lm8: :: 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 set ;
coherence
for b1 being set st b1 = TermSymbolsOf S holds
not b1 is empty
proof end;
cluster own -> ofAtomicFormula 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 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 Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is operational holds
b1 is termal
proof end;
cluster literal -> termal Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is literal holds
b1 is termal
proof end;
cluster termal -> own 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 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 Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is low-compounding holds
b1 is ofAtomicFormula
proof end;
cluster termal -> non relational 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 Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is literal holds
not b1 is relational ;
cluster literal -> non operational 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 Element of AllSymbolsOf S;
existence
ex b1 being Element of S st b1 is relational
proof end;
cluster literal 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 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 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 number ;
coherence
for b1 being number st b1 = ar s holds
b1 is empty
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 :DefSPrefix: :: FOMODEL1:def 28
X is AllSymbolsOf S -prefix ;
end;

:: deftheorem DefSPrefix 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 set ;
coherence
for b1 being set st b1 is S -prefix holds
b1 is AllSymbolsOf S -prefix by DefSPrefix;
cluster AllSymbolsOf S -prefix -> S -prefix set ;
coherence
for b1 being set st b1 is AllSymbolsOf S -prefix holds
b1 is S -prefix by DefSPrefix;
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 set ;
coherence
for b1 being set st b1 = ((AllSymbolsOf S) *) \ {{}} holds
not b1 is empty ;
end;

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

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

registration
let S be Language;
cluster AllSymbolsOf S -> infinite ;
coherence
not AllSymbolsOf S 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 abs (ar s) -element ) } ;
coherence
{ (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is abs (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 abs (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 :DefTerm: :: 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 DefTerm 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;

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

Lm2: 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 Lm4: :: FOMODEL1:2
for mm being Element of NAT
for S being Language holds (S -termsOfMaxDepth) . mm c= AllTermsOf S
proof end;

Lm26: 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 :DefTermal2: :: FOMODEL1:def 32
w in AllTermsOf S;
end;

:: deftheorem DefTermal2 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 :DefTermal: :: FOMODEL1:def 33
w in (S -termsOfMaxDepth) . m;
end;

:: deftheorem DefTermal 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 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 -> Function of NAT,(bool ((AllSymbolsOf S) *));
coherence
S -termsOfMaxDepth is Function of NAT,(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 ;
coherence
not AllTermsOf S 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 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 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 non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like countable finite-support m -termal 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 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 Element of S;
coherence
for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is literal
proof end;
end;

Lm1: 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 abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
proof end;

Lm19: 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 abs (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 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 Lm333: :: 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 abs (ar ((S -firstChar) . w)) -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
proof end;

Lm27: 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 ;
coherence
(S -termsOfMaxDepth) . m is S -prefix by Lm27;
end;

registration
let S be Language;
let V be Element of (AllTermsOf S) * ;
cluster (S -multiCat) . V -> Relation-like ;
coherence
(S -multiCat) . V is Relation-like ;
end;

registration
let S be Language;
let V be Element of (AllTermsOf S) * ;
cluster (S -multiCat) . V -> Function-like 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 :DefAtomic: :: FOMODEL1:def 35
 ex s being relational Element of S ex V being abs (ar b1) -element Element of (AllTermsOf S) * st phi = <*s*> ^ ((S -multiCat) . V);
end;

:: deftheorem DefAtomic 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 abs (ar b3) -element Element of (AllTermsOf S) * st phi = <*s*> ^ ((S -multiCat) . V) );

registration
let S be Language;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like countable finite-support 0wff 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 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 ;
coherence
not AtomicFormulasOf S is empty
proof end;
end;

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

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

registration
let S be Language;
cluster AllTermsOf S -> S -prefix ;
coherence
AllTermsOf S is S -prefix by Lm3;
end;

definition
let S be Language;
let t be termal string of S;
func SubTerms t -> Element of (AllTermsOf S) * means :DefSubTerms1: :: FOMODEL1:def 37
( it is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . it) );
existence
ex b1 being Element of (AllTermsOf S) * st
( b1 is abs (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 abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b1) & b2 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b2) holds
b1 = b2
proof end;
end;

:: deftheorem DefSubTerms1 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 abs (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 -> abs (ar t) -element Element of (AllTermsOf S) * ;
coherence
for b1 being Element of (AllTermsOf S) * st b1 = SubTerms t holds
b1 is abs (ar t) -element by DefSubTerms1;
end;

registration
let S be Language;
let t0 be 0 -termal string of S;
cluster SubTerms t0 -> empty 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 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 -> abs (ar ((S -firstChar) . phi)) -element Element of (AllTermsOf S) * means :DefSubTerms2: :: FOMODEL1:def 38
phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . it);
existence
ex b1 being abs (ar ((S -firstChar) . phi)) -element Element of (AllTermsOf S) * st phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b1)
proof end;
uniqueness
for b1, b2 being abs (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 DefSubTerms2 defines SubTerms FOMODEL1:def 38 :
for S being Language
for phi being 0wff string of S
for b3 being abs (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 -> abs (ar ((S -firstChar) . phi)) -element FinSequence;
coherence
for b1 being FinSequence st b1 = SubTerms phi holds
b1 is abs (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 Element of AllTermsOf S;
coherence
for b1 being Element of AllTermsOf S holds b1 is termal by DefTermal2;
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 Lm2;

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 Lm26;

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:138;

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 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 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 Function of NAT,(bool ((AllSymbolsOf S) *)) ;

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

registration
let S be Language;
cluster TheNorSymbOf S -> non low-compounding 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 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 :DefDepth2: :: 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 DefDepth2 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 number ;
coherence
for b1 being number st b1 = Depth t holds
b1 is empty by DefDepth2;
end;

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

registration
let S be Language;
let s be termal Element of S;
cluster ar s -> ext-real non negative ;
coherence
( not ar s is negative & ar s is ext-real )
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 Function;
coherence
for b1 being Function st b1 = S -multiCat holds
b1 is FinSequence-yielding ;
end;

registration
let S be Language;
let W be non empty ((AllSymbolsOf S) *) \ {{}} -valued FinSequence;
cluster (S -multiCat) . W -> non empty 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 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 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 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 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 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 -> Function of NAT,(bool (((AllSymbolsOf S) *) \ {{}}));
coherence
S -termsOfMaxDepth is Function of NAT,(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 ;
coherence
(S -termsOfMaxDepth) . mm 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 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 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 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 abs (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 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 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 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 :DefExt0: :: FOMODEL1:def 41
( the adicity of S1 c= the adicity of S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 );
end;

:: deftheorem DefExt0 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 Language-like ;
coherence
for b1 being Language-like st b1 = S null holds
b1 is S -extending
proof end;
end;

registration
let S be Language;
cluster non empty non degenerated non trivial infinite eligible S -extending 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 ;
coherence
(OwnSymbolsOf S1) \ (OwnSymbolsOf S2) 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 :DefExt1: :: 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 DefExt1 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 ;
coherence
S extendWith f is S -extending
proof end;
end;

registration
let S be non degenerated Language-like ;
cluster S -extending -> 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 ;
cluster S -extending -> 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:138;
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 number ;
cluster X --> m -> INT -valued ;
coherence
X --> m 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 ;
coherence
not (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X) is finite
proof end;
end;

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

registration
let S be countable Language;
cluster AllSymbolsOf S -> countable ;
coherence
AllSymbolsOf S is countable by ORDERS_4:def 2;
end;

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