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


begin

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

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

::########## First-order structure (theory) formalization ###########
::###################### basic definitions ##########################
::#####################################################################
::#####################################################################
definition
attrc1 is strict ;
struct Language-like  ->  ZeroOneStr ;
aggrLanguage-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 ;
attrS is operational  means :: FOMODEL1:def 12
 not OpSymbolsOf S is empty ;
attrS 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;
attrs is literal  means :Def14: :: FOMODEL1:def 14
s in LettersOf S;
attrs is low-compounding  means :Def15: :: FOMODEL1:def 15
s in LowerCompoundersOf S;
attrs is operational  means :Def16: :: FOMODEL1:def 16
s in OpSymbolsOf S;
attrs is relational  means :Def17: :: FOMODEL1:def 17
s in RelSymbolsOf S;
attrs is termal  means :Def18: :: FOMODEL1:def 18
s in TermSymbolsOf S;
attrs is own  means :Def19: :: FOMODEL1:def 19
s in OwnSymbolsOf S;
attrs 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 Def19 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 number  equals :Def21: :: 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 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 ;
funcS 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
proofend;
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
proofend;
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
proofend;
end;

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

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

definition
let S be Language-like ;
attrS 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 )
proofend;

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 ;
coherence
 not LettersOf S 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)}
proofend;

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
proofend;
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 Lm3;
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 )
proofend;

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
proofend;
cluster own  ->  ofAtomicFormula for Element of AllSymbolsOf S;
coherence
 for b1 being Element of S st b1 is own holds
b1 is ofAtomicFormula
proofend;
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
proofend;
cluster operational  ->  termal for Element of AllSymbolsOf S;
coherence
 for b1 being Element of S st b1 is operational holds
b1 is termal
proofend;
cluster literal  ->  termal for Element of AllSymbolsOf S;
coherence
 for b1 being Element of S st b1 is literal holds
b1 is termal
proofend;
cluster termal  ->  own for Element of AllSymbolsOf S;
coherence
 for b1 being Element of S st b1 is termal holds
b1 is own
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
end;

registration
let S be Language;
cluster relational for Element of AllSymbolsOf S;
existence
 ex b1 being Element of S st b1 is relational
proofend;
cluster literal for Element of AllSymbolsOf S;
existence
 ex b1 being Element of S st b1 is literal
proofend;
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
proofend;
end;

registration
let S be Language;
cluster ofAtomicFormula for Element of AllSymbolsOf S;
existence
 ex b1 being Element of S st b1 is ofAtomicFormula
proofend;
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
proofend;
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 empty
proofend;
end;

definition
let S be Language;
funcS -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;
funcS -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;
funcS -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 ;
attrX 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;
clusterS -prefix  ->  AllSymbolsOf S -prefix for set ;
coherence
 for b1 being set st b1 is S -prefix holds
b1 is AllSymbolsOf S -prefix by Def28;
cluster AllSymbolsOf S -prefix  -> S -prefix for set ;
coherence
 for b1 being set st b1 is AllSymbolsOf S -prefix holds
b1 is S -prefix by Def28;
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 by FOMODEL0:5;
end;

registration
cluster non degenerated eligible  ->  infinite for Language-like ;
coherence
 for b1 being Language holds b1 is infinite
proofend;
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 &amp; StringTuple is abs (ar s) -element )  }  ;
coherence
  {  (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings &amp; 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 &amp; 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) *) \ {{}})
proofend;
end;

definition
let S be Language;
funcS -termsOfMaxDepth  ->  Function means :Def30: :: FOMODEL1:def 30
( dom it = NAT &amp; it . 0 = AtomicTermsOf S &amp; ( 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 &amp; b1 . 0 = AtomicTermsOf S &amp; ( 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) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = NAT &amp; b1 . 0 = AtomicTermsOf S &amp; ( 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) ) &amp; dom b2 = NAT &amp; b2 . 0 = AtomicTermsOf S &amp; ( 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
proofend;
end;

:: deftheorem Def30 defines -termsOfMaxDepth FOMODEL1:def_30_:_
 for S being Language
for b2 being Function holds
( b2 = S -termsOfMaxDepth iff ( dom b2 = NAT &amp; b2 . 0 = AtomicTermsOf S &amp; ( 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) *)
proofend;
end;

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

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

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

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

definition
let S be Language;
let w be string of S;
attrw 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;
attrw 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;
clusterm -termal  ->  termal for Element of ((AllSymbolsOf S) *) \ {{}};
coherence
 for b1 being string of S st b1 is m -termal holds
b1 is termal
proofend;
end;

definition
let S be Language;
:: original:-termsOfMaxDepth
redefine funcS -termsOfMaxDepth  ->  Function of NAT,(bool ((AllSymbolsOf S) *));
coherence
 S -termsOfMaxDepth is Function of NAT,(bool ((AllSymbolsOf S) *))
proofend;
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) *)
proofend;
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
proofend;
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
proofend;
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
proofend;
end;

registration
let m be Nat;
let S be Language;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support m -termal for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 ex b1 being string of S st b1 is m -termal
proofend;
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
proofend;
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
proofend;
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 abs (ar s) -element &amp; w = <*s*> ^ ((S -multiCat) . T) )
proofend;

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

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
proofend;
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 abs (ar ((S -firstChar) . w)) -element &amp; w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
proofend;

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

registration
let S be Language;
let m be Nat;
cluster(S -termsOfMaxDepth) . m -> S -prefix ;
coherence
 (S -termsOfMaxDepth) . m is S -prefix by Lm9;
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 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;
attrphi is 0wff  means :Def35: :: 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 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 abs (ar b3) -element Element of (AllTermsOf S) * st phi = <*s*> ^ ((S -multiCat) . V) );

registration
let S be Language;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support 0wff for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 ex b1 being string of S st b1 is 0wff
proofend;
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
proofend;
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) *) \ {{}})
proofend;
end;

registration
let S be Language;
cluster AtomicFormulasOf S ->  non empty ;
coherence
 not AtomicFormulasOf S is empty
proofend;
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
proofend;
end;

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

registration
let S be Language;
cluster AllTermsOf S -> S -prefix ;
coherence
 AllTermsOf S 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 abs (ar ((S -firstChar) . t)) -element &amp; t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . it) );
existence
 ex b1 being Element of (AllTermsOf S) * st
( b1 is abs (ar ((S -firstChar) . t)) -element &amp; t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b1) )
proofend;
uniqueness
 for b1, b2 being Element of (AllTermsOf S) * st b1 is abs (ar ((S -firstChar) . t)) -element &amp; t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b1) &amp; b2 is abs (ar ((S -firstChar) . t)) -element &amp; t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b2) holds
b1 = b2
proofend;
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 abs (ar ((S -firstChar) . t)) -element &amp; 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 for Element of (AllTermsOf S) * ;
coherence
 for b1 being Element of (AllTermsOf S) * st b1 = SubTerms t holds
b1 is abs (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
proofend;
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
proofend;
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 :Def38: :: 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)
proofend;
uniqueness
 for b1, b2 being abs (ar ((S -firstChar) . phi)) -element Element of (AllTermsOf S) * st phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b1) &amp; phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b2) holds
b1 = b2
proofend;
end;

:: deftheorem Def38 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 for 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) *) \ {{}})
proofend;
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 by Def32;
end;

definition
let S be Language;
funcS -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
proofend;
uniqueness
 for b1, b2 being Function of (AllTermsOf S),((AllTermsOf S) *) st ( for t being Element of AllTermsOf S holds b1 . t = SubTerms t ) &amp; ( for t being Element of AllTermsOf S holds b2 . t = SubTerms t ) holds
b1 = b2
proofend;
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)}
proofend;

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

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
proofend;
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
proofend;
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) * )
proofend;

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 )
proofend;

theorem :: FOMODEL1:14
for S being Language holds S -termsOfMaxDepth is Function of NAT,(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 by Def14;
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
proofend;
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
proofend;
end;

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

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 &amp; ( for n being Nat st t is n -termal holds
it <= n ) );
existence
 ex b1 being Nat st
( t is b1 -termal &amp; ( for n being Nat st t is n -termal holds
b1 <= n ) )
proofend;
uniqueness
 for b1, b2 being Nat st t is b1 -termal &amp; ( for n being Nat st t is n -termal holds
b1 <= n ) &amp; t is b2 -termal &amp; ( for n being Nat st t is n -termal holds
b2 <= n ) holds
b1 = b2
proofend;
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 &amp; ( 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 empty 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 empty
proofend;
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 &amp; ar s is ext-real )
proofend;
end;

registration
let S be Language;
let s be relational Element of S;
cluster ar s ->  ext-real negative ;
coherence
 ( ar s is negative &amp; ar s is ext-real )
proofend;
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 &amp; SubTerms t <> {} )
proofend;

registration
let S be Language;
clusterS -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 non empty ((AllSymbolsOf S) *) \ {{}} -valued FinSequence;
cluster(S -multiCat) . W ->  non empty for set ;
coherence
 for b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty
proofend;
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
proofend;
end;

registration
let S be Language;
let m, n be Nat;
clusterm + (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
proofend;
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
proofend;
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
proofend;
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
proofend;
end;

definition
let S be Language;
:: original:-termsOfMaxDepth
redefine funcS -termsOfMaxDepth  ->  Function of NAT,(bool (((AllSymbolsOf S) *) \ {{}}));
coherence
 S -termsOfMaxDepth is Function of NAT,(bool (((AllSymbolsOf S) *) \ {{}}))
proofend;
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) *
proofend;

registration
let S be Language;
let m be Nat;
let t be termal string of S;
clustert 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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;

registration
cluster non empty strict for Language-like ;
existence
 ex b1 being Language-like st
( b1 is strict &amp; not b1 is empty )
proofend;
end;

definition
let S1, S2 be Language-like ;
attrS2 is S1 -extending  means :Def41: :: FOMODEL1:def 41
( the adicity of S1 c= the adicity of S2 &amp; TheEqSymbOf S1 = TheEqSymbOf S2 &amp; 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 &amp; TheEqSymbOf S1 = TheEqSymbOf S2 &amp; TheNorSymbOf S1 = TheNorSymbOf S2 ) );

registration
let S be Language;
clusterS null  -> S -extending for Language-like ;
coherence
 for b1 being Language-like st b1 = S null holds
b1 is S -extending
proofend;
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
proofend;
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
proofend;
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);
funcL 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 &amp; the ZeroF of it = the ZeroF of L &amp; 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 &amp; the ZeroF of b1 = the ZeroF of L &amp; the OneF of b1 = the OneF of L )
proofend;
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 &amp; the ZeroF of b1 = the ZeroF of L &amp; the OneF of b1 = the OneF of L &amp; the adicity of b2 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L &amp; the ZeroF of b2 = the ZeroF of L &amp; the OneF of b2 = the OneF of L holds
b1 = b2
proofend;
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 &amp; the ZeroF of b3 = the ZeroF of L &amp; the OneF of b3 = the OneF of L ) );

registration
let S be non empty Language-like ;
let f be INT -valued Function;
clusterS extendWith f ->  non empty strict S -extending ;
coherence
 S extendWith f is S -extending
proofend;
end;

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

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

registration
let E be empty Relation;
let X be set ;
clusterX |` 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) &amp; the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = the adicity of S1 | (OwnSymbolsOf S1) )
proofend;

registration
let X be set ;
let m be integer number ;
clusterX --> m ->  INT -valued ;
coherence
 X --> m is INT -valued
proofend;
end;

definition
let S be Language;
let X be functional set ;
funcS 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
proofend;
end;

registration
cluster non empty non degenerated non trivial infinite countable eligible for Language-like ;
existence
 ex b1 being Language st b1 is countable
proofend;
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
proofend;
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
proofend;
end;

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