:: FOMODEL1 semantic presentation

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 )
proof
take  - 1 ; ::_thesis: ( - 1 is negative & - 1 is integer )
thus  ( - 1 is negative & - 1 is integer ) ; ::_thesis: verum
end;
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
proof
set z = the ZeroF of S;
set o = the OneF of S;
 ( the ZeroF of S = 0. S & 1. S <> 0. S & 1. S = the OneF of S ) ;
then  the ZeroF of S <> the OneF of S ;
then  ( the ZeroF of S in the carrier of S & not the ZeroF of S in { the OneF of S} ) by TARSKI:def_1;
hence  not the carrier of S \ { the OneF of S} is empty by XBOOLE_0:def_5; ::_thesis: verum
end;
end;

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
proof
set D = the carrier of S \ { the OneF of S};
deffunc H1( Element of the carrier of S \ { the OneF of S}) ->  Element of INT = TrivialArity $1;
consider f being Function of ( the carrier of S \ { the OneF of S}),INT such that
A1: for x being Element of the carrier of S \ { the OneF of S} holds f . x = H1(x) from FUNCT_2:sch_4();
take  f ; ::_thesis: for s being Element of the carrier of S \ { the OneF of S} holds f . s = TrivialArity s
thus  for s being Element of the carrier of S \ { the OneF of S} holds f . s = TrivialArity s by A1; ::_thesis: verum
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
set D = the carrier of S \ { the OneF of S};
let IT1, IT2 be Function of ( the carrier of S \ { the OneF of S}),INT; ::_thesis: ( ( for s being Element of the carrier of S \ { the OneF of S} holds IT1 . s = TrivialArity s ) & ( for s being Element of the carrier of S \ { the OneF of S} holds IT2 . s = TrivialArity s ) implies IT1 = IT2 )
A2: ( dom IT1 = the carrier of S \ { the OneF of S} & dom IT2 = the carrier of S \ { the OneF of S} ) by FUNCT_2:def_1;
assume A3: for s being Element of the carrier of S \ { the OneF of S} holds IT1 . s = TrivialArity s ; ::_thesis: ( ex s being Element of the carrier of S \ { the OneF of S} st not IT2 . s = TrivialArity s or IT1 = IT2 )
assume A4: for s being Element of the carrier of S \ { the OneF of S} holds IT2 . s = TrivialArity s ; ::_thesis: IT1 = IT2
now__::_thesis:_for_x_being_set_st_x_in_dom_IT1_holds_
IT1_._x_=_IT2_._x
let x be set ; ::_thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume  x in dom IT1 ; ::_thesis: IT1 . x = IT2 . x
then reconsider s = x as Element of the carrier of S \ { the OneF of S} ;
IT1 . s = TrivialArity s by A3
.= IT2 . s by A4 ;
hence  IT1 . x = IT2 . x ; ::_thesis: verum
end;
hence  IT1 = IT2 by A2, FUNCT_1:2; ::_thesis: verum
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
set X = the infinite set ;
set Z = the Element of the infinite set ;
set O = the Element of the infinite set \ { the Element of the infinite set };
reconsider Y = the infinite set \ { the Element of the infinite set } as infinite set ;
 not the Element of the infinite set \ { the Element of the infinite set } in { the Element of the infinite set } by XBOOLE_0:def_5;
then A1: the Element of the infinite set \ { the Element of the infinite set } <> the Element of the infinite set by TARSKI:def_1;
reconsider OO = the Element of the infinite set \ { the Element of the infinite set } as Element of the infinite set ;
set S = ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #);
 ( 1. ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #) = OO & 0. ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #) = the Element of the infinite set ) ;
then reconsider SS = ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #) as non degenerated ZeroOneStr by A1, STRUCT_0:def_8;
take  SS ; ::_thesis: SS is infinite
thus  SS is infinite ; ::_thesis: verum
end;
end;

registration
let S be non degenerated infinite ZeroOneStr ;
cluster(S TrivialArity) " {0} ->  infinite ;
coherence
 not (S TrivialArity) " {0} is finite
proof
set I = the carrier of S;
set F0 = { the ZeroF of S};
set F1 = { the OneF of S};
set D1 = the carrier of S \ { the OneF of S};
set D0 = ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S};
set f = S TrivialArity ;
A1: dom (S TrivialArity) = the carrier of S \ { the OneF of S} by FUNCT_2:def_1;
 for x being set st x in ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} holds
x in (S TrivialArity) " {0}
proof
let x be set ; ::_thesis: ( x in ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} implies x in (S TrivialArity) " {0} )
assume A2: x in ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} ; ::_thesis: x in (S TrivialArity) " {0}
then reconsider xx = x as Element of the carrier of S \ { the OneF of S} ;
 not xx in { the ZeroF of S} by A2, XBOOLE_0:def_5;
then  xx <> the ZeroF of S by TARSKI:def_1;
then  ( TrivialArity xx = 0 & (S TrivialArity) . xx = TrivialArity xx ) by Def21, Def22;
then  ( xx in dom (S TrivialArity) & (S TrivialArity) . xx in {0} ) by A1, TARSKI:def_1;
hence  x in (S TrivialArity) " {0} by FUNCT_1:def_7; ::_thesis: verum
end;
then A3: ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} c= (S TrivialArity) " {0} by TARSKI:def_3;
reconsider D11 = the carrier of S \ { the OneF of S} as infinite set ;
thus  not (S TrivialArity) " {0} is finite by A3; ::_thesis: verum
end;
end;

Lm1:  for S being non degenerated ZeroOneStr holds (S TrivialArity) . the ZeroF of S = - 2
proof
let S be non degenerated ZeroOneStr ; ::_thesis: (S TrivialArity) . the ZeroF of S = - 2
set f = S TrivialArity ;
set x0 = the ZeroF of S;
set x1 = the OneF of S;
 ( the ZeroF of S = 0. S & the OneF of S = 1. S & 0. S <> 1. S ) ;
then  not the ZeroF of S in { the OneF of S} by TARSKI:def_1;
then reconsider x = the ZeroF of S as Element of the carrier of S \ { the OneF of S} by XBOOLE_0:def_5;
(S TrivialArity) . x = TrivialArity x by Def22
.= - 2 by Def21 ;
hence  (S TrivialArity) . the ZeroF of S = - 2 ; ::_thesis: verum
end;

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 )
proof
set SS = the non degenerated infinite ZeroOneStr ;
A1: 0. the non degenerated infinite ZeroOneStr <> 1. the non degenerated infinite ZeroOneStr ;
set f = the non degenerated infinite ZeroOneStr TrivialArity ;
take S = Language-like(# the carrier of the non degenerated infinite ZeroOneStr , the ZeroF of the non degenerated infinite ZeroOneStr , the OneF of the non degenerated infinite ZeroOneStr ,( the non degenerated infinite ZeroOneStr TrivialArity) #); ::_thesis: ( not S is degenerated & S is eligible )
 0. S <> 1. S by A1;
hence  not S is degenerated by STRUCT_0:def_8; ::_thesis: S is eligible
set g = the adicity of S;
thus  LettersOf S is infinite ; :: according to FOMODEL1:def_23 ::_thesis: the adicity of S . (TheEqSymbOf S) = - 2
thus  the adicity of S . (TheEqSymbOf S) = - 2 by Lm1; ::_thesis: verum
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 ;
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)}
proof
let S be non degenerated Language-like ; ::_thesis: TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)}
set EQ = TheEqSymbOf S;
set NOR = TheNorSymbOf S;
set SS = AllSymbolsOf S;
 ( 1. S <> 0. S & TheEqSymbOf S = 0. S & TheNorSymbOf S = 1. S ) ;
then  ( TheEqSymbOf S in AllSymbolsOf S & not TheEqSymbOf S in {(TheNorSymbOf S)} ) by TARSKI:def_1;
hence  TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)} by XBOOLE_0:def_5; ::_thesis: verum
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
set E = TheEqSymbOf S;
set R = RelSymbolsOf S;
set a = the adicity of S;
set D = (AllSymbolsOf S) \ {(TheNorSymbOf S)};
 ( - 2 in INT & not - 2 in NAT ) by INT_1:def_2;
then A1: - 2 in INT \ NAT by XBOOLE_0:def_5;
 ( TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)} & dom the adicity of S = (AllSymbolsOf S) \ {(TheNorSymbOf S)} ) by Lm3, FUNCT_2:def_1;
then  ( TheEqSymbOf S in dom the adicity of S & the adicity of S . (TheEqSymbOf S) in INT \ NAT ) by A1, Def23;
then  TheEqSymbOf S in RelSymbolsOf S by FUNCT_1:def_7;
hence  for b1 being Element of S st b1 = TheEqSymbOf S holds
b1 is relational by Def17; ::_thesis: verum
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 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 )
proof
let S be Language; ::_thesis: ( (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 )
set o = the OneF of S;
set z = the ZeroF of S;
set f = the adicity of S;
set R = RelSymbolsOf S;
set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
set e = TheEqSymbOf S;
set n = TheNorSymbOf S;
set A = AtomicFormulaSymbolsOf S;
set D = the carrier of S \ { the OneF of S};
set L = LowerCompoundersOf S;
set T = TermSymbolsOf S;
set OP = OpSymbolsOf S;
set B = LettersOf S;
A1: {0} misses NAT \ {0} by XBOOLE_1:79;
thus (LettersOf S) /\ (OpSymbolsOf S) = the adicity of S " ({0} /\ (NAT \ {0})) by FUNCT_1:68
.= the adicity of S " {} by A1, XBOOLE_0:def_7
.= {} ; ::_thesis: ( (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 )
thus (TermSymbolsOf S) /\ (LowerCompoundersOf S) = the adicity of S " (NAT /\ (INT \ {0})) by FUNCT_1:68
.= the adicity of S " ((NAT /\ INT) \ {0}) by XBOOLE_1:49
.= OpSymbolsOf S by XBOOLE_1:7, XBOOLE_1:28 ; ::_thesis: ( (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 )
A2: TheEqSymbOf S in RelSymbolsOf S by Def17;
OwnSymbolsOf S = (AllSymbolsOf S) \ ({ the ZeroF of S} \/ { the OneF of S}) by ENUMSET1:1
.= ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} by XBOOLE_1:41 ;
then (RelSymbolsOf S) \ (OwnSymbolsOf S) = ((RelSymbolsOf S) \ ( the carrier of S \ { the OneF of S})) \/ ((RelSymbolsOf S) /\ { the ZeroF of S}) by XBOOLE_1:52
.= {} \/ ((RelSymbolsOf S) /\ { the ZeroF of S})
.= { the ZeroF of S} by A2, ZFMISC_1:46 ;
hence  (RelSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)} ; ::_thesis: ( 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 )
thus  OwnSymbolsOf S c= AtomicFormulaSymbolsOf S by XBOOLE_1:34, ZFMISC_1:7; ::_thesis: ( 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 )
 ( the adicity of S " {0} c= the adicity of S " NAT & RelSymbolsOf S = ( the adicity of S " INT) \ ( the adicity of S " NAT) & LowerCompoundersOf S = ( the adicity of S " INT) \ ( the adicity of S " {0}) ) by FUNCT_1:69, RELAT_1:143;
hence  RelSymbolsOf S c= LowerCompoundersOf S by XBOOLE_1:34; ::_thesis: ( 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 )
 OpSymbolsOf S = ( the adicity of S " NAT) \ ( the adicity of S " {0}) by FUNCT_1:69;
hence  OpSymbolsOf S c= TermSymbolsOf S ; ::_thesis: ( LettersOf S c= TermSymbolsOf S & TermSymbolsOf S c= OwnSymbolsOf S & OpSymbolsOf S c= LowerCompoundersOf S & LowerCompoundersOf S c= AtomicFormulaSymbolsOf S )
thus  LettersOf S c= TermSymbolsOf S by RELAT_1:143; ::_thesis: ( TermSymbolsOf S c= OwnSymbolsOf S & OpSymbolsOf S c= LowerCompoundersOf S & LowerCompoundersOf S c= AtomicFormulaSymbolsOf S )
- 2 = the adicity of S . (TheEqSymbOf S) by Def23
.= the adicity of S . the ZeroF of S ;
then  not the adicity of S . the ZeroF of S in NAT ;
then  not the ZeroF of S in the adicity of S " NAT by FUNCT_1:def_7;
then  ( the adicity of S " NAT misses { the ZeroF of S} & the adicity of S " NAT c= the carrier of S \ { the OneF of S} ) by ZFMISC_1:50;
then  the adicity of S " NAT c= ( the carrier of S \ { the OneF of S}) \ { the ZeroF of S} by XBOOLE_1:86;
then  TermSymbolsOf S c= the carrier of S \ ({ the OneF of S} \/ { the ZeroF of S}) by XBOOLE_1:41;
hence  TermSymbolsOf S c= OwnSymbolsOf S by ENUMSET1:1; ::_thesis: ( OpSymbolsOf S c= LowerCompoundersOf S & LowerCompoundersOf S c= AtomicFormulaSymbolsOf S )
 for x being set st x in NAT holds
x in INT by INT_1:def_2;
then  NAT c= INT by TARSKI:def_3;
then  NAT \ {0} c= INT \ {0} by XBOOLE_1:33;
hence  OpSymbolsOf S c= LowerCompoundersOf S by RELAT_1:143; ::_thesis: LowerCompoundersOf S c= AtomicFormulaSymbolsOf S
thus  LowerCompoundersOf S c= AtomicFormulaSymbolsOf S ; ::_thesis: verum
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
 LettersOf S c= TermSymbolsOf S by Th1;
hence  for b1 being set st b1 = TermSymbolsOf S holds
not b1 is empty ; ::_thesis: verum
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
let s be Element of S; ::_thesis: ( s is own implies s is ofAtomicFormula )
assume  s is own ; ::_thesis: s is ofAtomicFormula
then  ( s in OwnSymbolsOf S & OwnSymbolsOf S c= AtomicFormulaSymbolsOf S ) by Th1, Def19;
hence  s is ofAtomicFormula by Def20; ::_thesis: verum
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
let s be Element of S; ::_thesis: ( s is relational implies s is low-compounding )
assume  s is relational ; ::_thesis: s is low-compounding
then  ( s in RelSymbolsOf S & RelSymbolsOf S c= LowerCompoundersOf S ) by Def17, Th1;
hence  s is low-compounding by Def15; ::_thesis: verum
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
let s be Element of S; ::_thesis: ( s is operational implies s is termal )
assume  s is operational ; ::_thesis: s is termal
then  ( s in OpSymbolsOf S & OpSymbolsOf S c= TermSymbolsOf S ) by Th1, Def16;
hence  s is termal by Def18; ::_thesis: verum
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
let s be Element of S; ::_thesis: ( s is literal implies s is termal )
assume  s is literal ; ::_thesis: s is termal
then  ( LettersOf S c= TermSymbolsOf S & s in LettersOf S ) by Def14, Th1;
hence  s is termal by Def18; ::_thesis: verum
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
let s be Element of S; ::_thesis: ( s is termal implies s is own )
assume  s is termal ; ::_thesis: s is own
then  ( TermSymbolsOf S c= OwnSymbolsOf S & s in TermSymbolsOf S ) by Def18, Th1;
hence  s is own by Def19; ::_thesis: verum
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
let s be Element of S; ::_thesis: ( s is operational implies s is low-compounding )
assume  s is operational ; ::_thesis: s is low-compounding
then  ( s in OpSymbolsOf S & OpSymbolsOf S c= LowerCompoundersOf S ) by Def16, Th1;
hence  s is low-compounding by Def15; ::_thesis: verum
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
proof
let s be Element of S; ::_thesis: ( s is low-compounding implies s is ofAtomicFormula )
assume  s is low-compounding ; ::_thesis: s is ofAtomicFormula
then  ( s in LowerCompoundersOf S & LowerCompoundersOf S c= AtomicFormulaSymbolsOf S ) by Def15;
hence  s is ofAtomicFormula by Def20; ::_thesis: verum
end;
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
set T = TermSymbolsOf S;
set R = RelSymbolsOf S;
set f = the adicity of S;
(TermSymbolsOf S) /\ (RelSymbolsOf S) = the adicity of S " (NAT /\ (INT \ NAT)) by FUNCT_1:68
.= the adicity of S " ((NAT /\ INT) \ (NAT /\ NAT))
.= the adicity of S " {}
.= {} ;
then  TermSymbolsOf S misses RelSymbolsOf S by XBOOLE_0:def_7;
then A1: (TermSymbolsOf S) \ (RelSymbolsOf S) = TermSymbolsOf S by XBOOLE_1:83;
let s be Element of S; ::_thesis: ( s is termal implies not s is relational )
assume  s is termal ; ::_thesis: not s is relational
then  s in (TermSymbolsOf S) \ (RelSymbolsOf S) by A1, Def18;
then  not s in RelSymbolsOf S by XBOOLE_0:def_5;
hence  not s is relational by Def17; ::_thesis: verum
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
set L = LettersOf S;
set P = OpSymbolsOf S;
let s be Element of S; ::_thesis: ( s is literal implies not s is operational )
assume A2: s is literal ; ::_thesis: not s is operational
assume  s is operational ; ::_thesis: contradiction
then  ( s in LettersOf S & s in OpSymbolsOf S ) by A2, Def14, Def16;
then  s in (LettersOf S) /\ (OpSymbolsOf S) by XBOOLE_0:def_4;
hence  contradiction by Th1; ::_thesis: verum
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
take s = TheEqSymbOf S; ::_thesis: s is relational
thus  s is relational ; ::_thesis: verum
end;
cluster literal for Element of AllSymbolsOf S;
existence
 ex b1 being Element of S st b1 is literal
proof
take  the Element of LettersOf S ; ::_thesis: the Element of LettersOf S is literal
thus  the Element of LettersOf S is literal by Def14; ::_thesis: verum
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
set L = LowerCompoundersOf S;
set T = TermSymbolsOf S;
set OP = OpSymbolsOf S;
let s be low-compounding Element of S; ::_thesis: ( s is termal implies s is operational )
A1: s in LowerCompoundersOf S by Def15;
assume  s is termal ; ::_thesis: s is operational
then  s in TermSymbolsOf S by Def18;
then  s in (LowerCompoundersOf S) /\ (TermSymbolsOf S) by A1, XBOOLE_0:def_4;
then  s in OpSymbolsOf S by Th1;
hence  s is operational by Def16; ::_thesis: verum
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
take  the literal Element of S ; ::_thesis: the literal Element of S is ofAtomicFormula
thus  the literal Element of S is ofAtomicFormula ; ::_thesis: verum
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
set f = the adicity of S;
reconsider g = the adicity of S as Function of (AtomicFormulaSymbolsOf S),INT ;
reconsider ss = s as Element of AtomicFormulaSymbolsOf S by Def20;
 g . ss in INT ;
hence  the adicity of S . s is Element of INT ; ::_thesis: verum
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 empty
proof
set f = the adicity of S;
 s in LettersOf S by Def14;
then  the adicity of S . s in {0} by FUNCT_1:def_7;
hence  for b1 being number st b1 = ar s holds
b1 is empty ; ::_thesis: verum
end;
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
proof
let S be Language; ::_thesis: S is infinite
set SS = AllSymbolsOf S;
set L = LettersOf S;
reconsider S0 = S as 1-sorted ;
 (LettersOf S) \/ (AllSymbolsOf S) = AllSymbolsOf S by XBOOLE_1:12;
hence  S is infinite ; ::_thesis: verum
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
set Y = Compound (s,Strings);
set SS = AllSymbolsOf S;
reconsider ss = s as Element of AllSymbolsOf S ;
now__::_thesis:_for_x_being_set_st_x_in_Compound_(s,Strings)_holds_
x_in_((AllSymbolsOf_S)_*)_\_{{}}
let x be set ; ::_thesis: ( x in Compound (s,Strings) implies x in ((AllSymbolsOf S) *) \ {{}} )
assume  x in Compound (s,Strings) ; ::_thesis: x in ((AllSymbolsOf S) *) \ {{}}
then consider StringTuple being Element of ((AllSymbolsOf S) *) *  such that
A1: ( x = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= Strings & StringTuple is abs (ar s) -element ) ;
reconsider head = <*ss*> as non empty FinSequence of AllSymbolsOf S ;
reconsider tail = (S -multiCat) . StringTuple as FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
 ( head ^ tail is non empty FinSequence of AllSymbolsOf S & x = head ^ tail ) by A1;
hence  x in ((AllSymbolsOf S) *) \ {{}} by FOMODEL0:5; ::_thesis: verum
end;
hence  Compound (s,Strings) is Element of bool (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def_3; ::_thesis: verum
end;
end;

definition
let S be Language;
funcS -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
deffunc H1( set , set ) ->  set = (union  {  (Compound (s,$2)) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ $2;
 ex f being Function st
( dom f = NAT & f . 0 = AtomicTermsOf S & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_11();
hence  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) ) ) ; ::_thesis: verum
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
deffunc H1( set , set ) ->  set = (union  {  (Compound (s,$2)) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ $2;
let IT1, IT2 be Function; ::_thesis: ( dom IT1 = NAT & IT1 . 0 = AtomicTermsOf S & ( for n being Nat holds IT1 . (n + 1) = (union  {  (Compound (s,(IT1 . n))) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ (IT1 . n) ) & dom IT2 = NAT & IT2 . 0 = AtomicTermsOf S & ( for n being Nat holds IT2 . (n + 1) = (union  {  (Compound (s,(IT2 . n))) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ (IT2 . n) ) implies IT1 = IT2 )
assume A1: ( dom IT1 = NAT & IT1 . 0 = AtomicTermsOf S & ( for n being Nat holds IT1 . (n + 1) = H1(n,IT1 . n) ) ) ; ::_thesis: ( not dom IT2 = NAT or not IT2 . 0 = AtomicTermsOf S or ex n being Nat st not IT2 . (n + 1) = (union  {  (Compound (s,(IT2 . n))) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ (IT2 . n) or IT1 = IT2 )
A2: dom IT1 = NAT by A1;
A3: IT1 . 0 = AtomicTermsOf S by A1;
A4: for n being Nat holds IT1 . (n + 1) = H1(n,IT1 . n) by A1;
assume A5: ( dom IT2 = NAT & IT2 . 0 = AtomicTermsOf S & ( for n being Nat holds IT2 . (n + 1) = H1(n,IT2 . n) ) ) ; ::_thesis: IT1 = IT2
A6: dom IT2 = NAT by A5;
A7: IT2 . 0 = AtomicTermsOf S by A5;
A8: for n being Nat holds IT2 . (n + 1) = H1(n,IT2 . n) by A5;
thus  IT1 = IT2 from NAT_1:sch_15(A2, A3, A4, A6, A7, A8); ::_thesis: verum
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
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
reconsider L = LettersOf S as Subset of (AllSymbolsOf S) ;
 AtomicTermsOf S c= L * by FINSEQ_2:134;
hence  AtomicTermsOf S is Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1; ::_thesis: verum
end;
end;

Lm4:  for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}
proof
let m be Nat; ::_thesis: for S being Language holds (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}
let S be Language; ::_thesis: (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set L = LettersOf S;
defpred S1[ Nat] means (S -termsOfMaxDepth) . $1 c= ((AllSymbolsOf S) *) \ {{}};
A1: S1[ 0 ]
proof
(S -termsOfMaxDepth) . 0 = AtomicTermsOf S by Def30
.= (0 + 1) -tuples_on (LettersOf S) ;
then A2: (S -termsOfMaxDepth) . 0 c= ((LettersOf S) *) \ {{}} by FOMODEL0:9;
 ((LettersOf S) *) \ {{}} c= ((AllSymbolsOf S) *) \ {{}} by XBOOLE_1:33;
hence  S1[ 0 ] by A2, XBOOLE_1:1; ::_thesis: verum
end;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
set TM1 =  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  ;
now__::_thesis:_for_X_being_set_st_X_in__{__(Compound_(s,((S_-termsOfMaxDepth)_._n)))_where_s_is_ofAtomicFormula_Element_of_S_:_s_is_operational__}__holds_
X_c=_((AllSymbolsOf_S)_*)_\_{{}}
let X be set ; ::_thesis: ( X in  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  implies X c= ((AllSymbolsOf S) *) \ {{}} )
assume  X in  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  ; ::_thesis: X c= ((AllSymbolsOf S) *) \ {{}}
then consider s being ofAtomicFormula Element of S such that
A5: ( X = Compound (s,((S -termsOfMaxDepth) . n)) & s is operational ) ;
thus  X c= ((AllSymbolsOf S) *) \ {{}} by A5; ::_thesis: verum
end;
then  ( union  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  c= ((AllSymbolsOf S) *) \ {{}} & (S -termsOfMaxDepth) . (n + 1) = (union  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ ((S -termsOfMaxDepth) . n) ) by Def30, ZFMISC_1:76;
hence  S1[n + 1] by A4, XBOOLE_1:8; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A3);
hence  (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}} ; ::_thesis: verum
end;

Lm5:  for m, n being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n)
proof
let m, n be Nat; ::_thesis: for S being Language holds (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n)
let S be Language; ::_thesis: (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n)
set T = S -termsOfMaxDepth ;
defpred S1[ Nat] means (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + $1);
A1: S1[ 0 ] ;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
 (S -termsOfMaxDepth) . ((m + n) + 1) = ((S -termsOfMaxDepth) . (m + n)) \/ (union  {  (Compound (s,((S -termsOfMaxDepth) . (m + n)))) where s is ofAtomicFormula Element of S : s is operational  }  ) by Def30;
then  (S -termsOfMaxDepth) . (m + n) c= (S -termsOfMaxDepth) . ((m + n) + 1) by XBOOLE_1:7;
hence  S1[n + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n) ; ::_thesis: verum
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
let mm be Element of NAT ; ::_thesis: for S being Language holds (S -termsOfMaxDepth) . mm c= AllTermsOf S
let S be Language; ::_thesis: (S -termsOfMaxDepth) . mm c= AllTermsOf S
set T = S -termsOfMaxDepth ;
 dom (S -termsOfMaxDepth) = NAT by Def30;
hence  (S -termsOfMaxDepth) . mm c= AllTermsOf S by FUNCT_1:3, ZFMISC_1:74; ::_thesis: verum
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
let x be set ; ::_thesis: for S being Language st x in AllTermsOf S holds
ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn
let S be Language; ::_thesis: ( x in AllTermsOf S implies ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn )
set T = S -termsOfMaxDepth ;
assume  x in AllTermsOf S ; ::_thesis: ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn
then consider Y being set  such that
A1: ( x in Y & Y in rng (S -termsOfMaxDepth) ) by TARSKI:def_4;
consider mmm being set  such that
A2: ( mmm in dom (S -termsOfMaxDepth) & Y = (S -termsOfMaxDepth) . mmm ) by A1, FUNCT_1:def_3;
reconsider mm = mmm as Element of NAT by A2, Def30;
take nn = mm; ::_thesis: x in (S -termsOfMaxDepth) . nn
thus  x in (S -termsOfMaxDepth) . nn by A1, A2; ::_thesis: verum
end;

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
proof
reconsider mm = m as Element of NAT by ORDINAL1:def_12;
let w be string of S; ::_thesis: ( w is m -termal implies w is termal )
assume  w is m -termal ; ::_thesis: w is termal
then  ( w in (S -termsOfMaxDepth) . m & (S -termsOfMaxDepth) . mm c= AllTermsOf S ) by Th2, Def33;
hence  w is termal by Def32; ::_thesis: verum
end;
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) *))
proof
set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
A1: dom (S -termsOfMaxDepth) = NAT by Def30;
now__::_thesis:_for_y_being_set_st_y_in_rng_(S_-termsOfMaxDepth)_holds_
y_in_bool_((AllSymbolsOf_S)_*)
let y be set ; ::_thesis: ( y in rng (S -termsOfMaxDepth) implies y in bool ((AllSymbolsOf S) *) )
assume  y in rng (S -termsOfMaxDepth) ; ::_thesis: y in bool ((AllSymbolsOf S) *)
then consider x being set  such that
A2: ( x in dom (S -termsOfMaxDepth) & y = (S -termsOfMaxDepth) . x ) by FUNCT_1:def_3;
reconsider m = x as Element of NAT by Def30, A2;
 y = (S -termsOfMaxDepth) . m by A2;
then  ( y c= ((AllSymbolsOf S) *) \ {{}} & ((AllSymbolsOf S) *) \ {{}} c= (AllSymbolsOf S) * ) by Lm4;
then  y c= (AllSymbolsOf S) * by XBOOLE_1:1;
hence  y in bool ((AllSymbolsOf S) *) ; ::_thesis: verum
end;
then  rng (S -termsOfMaxDepth) c= bool ((AllSymbolsOf S) *) by TARSKI:def_3;
hence  S -termsOfMaxDepth is Function of NAT,(bool ((AllSymbolsOf S) *)) by A1, FUNCT_2:67, RELSET_1:4; ::_thesis: verum
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
set A = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
A1: now__::_thesis:_for_x_being_set_st_x_in_AllTermsOf_S_holds_
x_in_(AllSymbolsOf_S)_*
let x be set ; ::_thesis: ( x in AllTermsOf S implies x in (AllSymbolsOf S) * )
assume  x in AllTermsOf S ; ::_thesis: x in (AllSymbolsOf S) *
then consider mm being Element of NAT  such that
A2: x in (S -termsOfMaxDepth) . mm by Lm6;
thus  x in (AllSymbolsOf S) * by A2; ::_thesis: verum
end;
AllTermsOf S = ((S -termsOfMaxDepth) . 0) \/ (AllTermsOf S) by Th2, XBOOLE_1:12
.= (AtomicTermsOf S) \/ (AllTermsOf S) by Def30 ;
hence  AllTermsOf S is non empty Subset of ((AllSymbolsOf S) *) by A1, TARSKI:def_3; ::_thesis: verum
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
set T = S -termsOfMaxDepth ;
set Z = AtomicTermsOf S;
set SS = AllSymbolsOf S;
set x = the Element of AtomicTermsOf S;
 ( the Element of AtomicTermsOf S in AtomicTermsOf S & AtomicTermsOf S = (S -termsOfMaxDepth) . 0 ) by Def30;
then  ( the Element of AtomicTermsOf S in (S -termsOfMaxDepth) . 0 & (S -termsOfMaxDepth) . 0 c= (S -termsOfMaxDepth) . (0 + m) ) by Lm5;
hence  not (S -termsOfMaxDepth) . m is empty ; ::_thesis: verum
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
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
A1: (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}} by Lm4;
let w be Element of (S -termsOfMaxDepth) . m; ::_thesis: not w is empty
 w in ((AllSymbolsOf S) *) \ {{}} by A1, TARSKI:def_3;
hence  not w is empty ; ::_thesis: verum
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
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
set AA = AllTermsOf S;
let t be Element of AllTermsOf S; ::_thesis: not t is empty
consider mm being Element of NAT  such that
A1: t in (S -termsOfMaxDepth) . mm by Lm6;
reconsider tt = t as Element of (S -termsOfMaxDepth) . mm by A1;
 not tt is empty ;
hence  not t is empty ; ::_thesis: verum
end;
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
proof
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
set w = the Element of AtomicTermsOf S;
A1: the Element of AtomicTermsOf S in AtomicTermsOf S ;
then  ( the Element of AtomicTermsOf S in (S -termsOfMaxDepth) . 0 & (S -termsOfMaxDepth) . 0 c= ((AllSymbolsOf S) *) \ {{}} ) by Lm4, Def30;
then reconsider ww = the Element of AtomicTermsOf S as string of S ;
take  ww ; ::_thesis: ww is m -termal
 ( ww in (S -termsOfMaxDepth) . 0 & (S -termsOfMaxDepth) . 0 c= (S -termsOfMaxDepth) . (0 + m) ) by Lm5, A1, Def30;
hence  ww is m -termal by Def33; ::_thesis: verum
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
set A = AtomicTermsOf S;
set L = LettersOf S;
set T = S -termsOfMaxDepth ;
let w be string of S; ::_thesis: ( w is 0 -termal implies w is 1 -element )
assume  w is 0 -termal ; ::_thesis: w is 1 -element
then  w in (S -termsOfMaxDepth) . 0 by Def33;
then  w in AtomicTermsOf S by Def30;
then reconsider ww = w as Element of 1 -tuples_on (LettersOf S) ;
 ww is 1 -element ;
hence  w is 1 -element ; ::_thesis: verum
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
set A = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set Z = AtomicTermsOf S;
set SS = AllSymbolsOf S;
set s = (S -firstChar) . w;
set ss = ((AllSymbolsOf S) -firstChar) . w;
set L = LettersOf S;
reconsider ww = w as non empty FinSequence of AllSymbolsOf S by FOMODEL0:5;
A1: ((AllSymbolsOf S) -firstChar) . w = ww . 1 by FOMODEL0:6;
 w in (S -termsOfMaxDepth) . 0 by Def33;
then  w in AtomicTermsOf S by Def30;
then consider x being set  such that
A2: ( x in LettersOf S & w = <*x*> ) by FINSEQ_2:135;
 w = <*x*> ^ {} by A2;
then  ((AllSymbolsOf S) -firstChar) . w in LettersOf S by A2, A1, FINSEQ_1:41;
hence  for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is literal by Def14; ::_thesis: verum
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 abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
proof
let mm be Element of NAT ; ::_thesis: for S being Language
for w being mm + 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) )
let S be Language; ::_thesis: for w being mm + 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) )
set fam =  {  (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational  }  ;
let w be mm + 1 -termal string of S; ::_thesis: ( not w is mm -termal implies 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) ) )
assume  not w is mm -termal ; ::_thesis: 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) )
then  ( w in (S -termsOfMaxDepth) . (mm + 1) & not w in (S -termsOfMaxDepth) . mm ) by Def33;
then  ( w in (union  {  (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ ((S -termsOfMaxDepth) . mm) & not w in (S -termsOfMaxDepth) . mm ) by Def30;
then  w in union  {  (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational  }  by XBOOLE_0:def_3;
then consider C being set  such that
A1: ( w in C & C in  {  (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational  }  ) by TARSKI:def_4;
consider sss being ofAtomicFormula Element of S such that
A2: ( C = Compound (sss,((S -termsOfMaxDepth) . mm)) & sss is operational ) by A1;
reconsider ss = sss as termal Element of S by A2;
take s = ss; ::_thesis: ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
consider StringTuple being Element of ((AllSymbolsOf S) *) *  such that
A3: ( w = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= (S -termsOfMaxDepth) . mm & StringTuple is abs (ar ss) -element ) by A1, A2;
reconsider TT = StringTuple as FinSequence of (S -termsOfMaxDepth) . mm by A3, FINSEQ_1:def_4;
reconsider TTT = TT as Element of ((S -termsOfMaxDepth) . mm) * by FINSEQ_1:def_11;
take T = TTT; ::_thesis: ( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
thus  T is abs (ar s) -element by A3; ::_thesis: w = <*s*> ^ ((S -multiCat) . T)
thus  w = <*s*> ^ ((S -multiCat) . T) by A3; ::_thesis: verum
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 abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
proof
let mm be Element of NAT ; ::_thesis: for S being Language
for w being mm + 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) )
let S be Language; ::_thesis: for w being mm + 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) )
set TS = TermSymbolsOf S;
set T = S -termsOfMaxDepth ;
set C = S -multiCat ;
set L = LettersOf S;
defpred S1[ Element of NAT ] means  for w being $1 + 1 -termal string of S ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . $1) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) );
defpred S2[ Nat] means  ex mm being Element of NAT st
( mm = $1 & S1[mm] );
A1: S2[ 0 ]
proof
take  0 ; ::_thesis: ( 0 = 0 & S1[ 0 ] )
thus  0 = 0 ; ::_thesis: S1[ 0 ]
thus  S1[ 0 ] ::_thesis: verum
proof
let w be 0 + 1 -termal string of S; ::_thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
percases ( w is 0 -termal or not w is 0 -termal ) ;
suppose w is 0 -termal ; ::_thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
then  w in (S -termsOfMaxDepth) . 0 by Def33;
then  w in AtomicTermsOf S by Def30;
then  w in  {  <*ss*> where ss is Element of LettersOf S : verum  }  by FINSEQ_2:96;
then consider ss being Element of LettersOf S such that
A2: w = <*ss*> ;
reconsider sss = ss as literal Element of S by Def14;
reconsider TT = {} as FinSequence ;
 rng TT = {} ;
then  rng TT c= (S -termsOfMaxDepth) . 0 by XBOOLE_1:2;
then reconsider TTT = TT as FinSequence of (S -termsOfMaxDepth) . 0 by FINSEQ_1:def_4;
reconsider TTTT = TTT as Element of ((S -termsOfMaxDepth) . 0) * by FINSEQ_1:def_11;
take s = sss; ::_thesis: ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
take T = TTTT; ::_thesis: ( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
thus  T is abs (ar s) -element ; ::_thesis: w = <*s*> ^ ((S -multiCat) . T)
reconsider s = sss as Element of TermSymbolsOf S by Def18;
 ( (S -multiCat) . {} = {} & <*sss*> ^ {} = <*sss*> ) ;
hence  w = <*s*> ^ ((S -multiCat) . T) by A2; ::_thesis: verum
end;
suppose not w is 0 -termal ; ::_thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
hence  ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) ) by Lm7; ::_thesis: verum
end;
end;
end;
end;
A3: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] )
reconsider mm = m, mmm = m + 1 as Element of NAT by ORDINAL1:def_12;
assume A4: S2[m] ; ::_thesis: S2[m + 1]
take  mmm ; ::_thesis: ( mmm = m + 1 & S1[mmm] )
thus  mmm = m + 1 ; ::_thesis: S1[mmm]
let w be mmm + 1 -termal string of S; ::_thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
percases ( not w is mmm -termal or w is mmm -termal ) ;
suppose not w is mmm -termal ; ::_thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
hence  ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) ) by Lm7; ::_thesis: verum
end;
suppose w is mmm -termal ; ::_thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
then consider s being termal Element of S, T being Element of ((S -termsOfMaxDepth) . mm) *  such that
A5: ( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) ) by A4;
set high = (S -termsOfMaxDepth) . mmm;
reconsider low = (S -termsOfMaxDepth) . mm as Subset of ((S -termsOfMaxDepth) . mmm) by Lm5;
 ( T in low * & low * is Subset of (((S -termsOfMaxDepth) . mmm) *) ) ;
then reconsider TT = T as Element of ((S -termsOfMaxDepth) . mmm) * ;
take  s ; ::_thesis: ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
take  TT ; ::_thesis: ( TT is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . TT) )
thus  ( TT is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . TT) ) by A5; ::_thesis: verum
end;
end;
end;
A6: for m being Nat holds S2[m] from NAT_1:sch_2(A1, A3);
now__::_thesis:_for_mm_being_Element_of_NAT_holds_S1[mm]
let mm be Element of NAT ; ::_thesis: S1[mm]
reconsider m = mm as Nat ;
consider nn being Element of NAT  such that
A7: ( nn = m & S1[nn] ) by A6;
thus  S1[mm] by A7; ::_thesis: verum
end;
hence  for w being mm + 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) ) ; ::_thesis: verum
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
set A = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set Z = AtomicTermsOf S;
set SS = AllSymbolsOf S;
set s = (S -firstChar) . w;
set ss = ((AllSymbolsOf S) -firstChar) . w;
set L = LettersOf S;
 w in AllTermsOf S by Def32;
then consider mm being Element of NAT  such that
A1: w in (S -termsOfMaxDepth) . mm by Lm6;
reconsider ww = w as non empty FinSequence of AllSymbolsOf S by FOMODEL0:5;
A2: ((AllSymbolsOf S) -firstChar) . w = ww . 1 by FOMODEL0:6;
percases ( mm = 0 or mm <> 0 ) ;
suppose mm = 0 ; ::_thesis: for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is termal
then reconsider www = w as 0 -termal string of S by Def33, A1;
 (S -firstChar) . www is literal ;
hence  for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is termal ; ::_thesis: verum
end;
suppose mm <> 0 ; ::_thesis: for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is termal
then consider n being Nat such that
A3: mm = n + 1 by NAT_1:6;
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
reconsider www = w as nn + 1 -termal string of S by A3, A1, Def33;
consider s1 being termal Element of S, T1 being Element of ((S -termsOfMaxDepth) . nn) *  such that
A4: ( T1 is abs (ar s1) -element & www = <*s1*> ^ ((S -multiCat) . T1) ) by Lm8;
thus  for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is termal by A4, A2, FINSEQ_1:41; ::_thesis: verum
end;
end;
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 abs (ar ((S -firstChar) . w)) -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
proof
let mm be Element of NAT ; ::_thesis: for S being Language
for w being mm + 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) )
let S be Language; ::_thesis: for w being mm + 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) )
let w be mm + 1 -termal string of S; ::_thesis: ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is abs (ar ((S -firstChar) . w)) -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
consider s being termal Element of S, T being Element of ((S -termsOfMaxDepth) . mm) *  such that
A1: ( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) ) by Lm8;
reconsider ww = w as non empty FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
s = w . 1 by A1, FINSEQ_1:41
.= (S -firstChar) . w by FOMODEL0:6 ;
hence  ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is abs (ar ((S -firstChar) . w)) -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) ) by A1; ::_thesis: verum
end;

Lm9:  for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m is S -prefix
proof
let m be Nat; ::_thesis: for S being Language holds (S -termsOfMaxDepth) . m is S -prefix
let S be Language; ::_thesis: (S -termsOfMaxDepth) . m is S -prefix
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set L = LettersOf S;
set S1 = 1 -tuples_on (AllSymbolsOf S);
set f = S -cons ;
set F = S -multiCat ;
set ff = (AllSymbolsOf S) -concatenation ;
set FF = (AllSymbolsOf S) -multiCat ;
A1: dom ((AllSymbolsOf S) -multiCat) = ((AllSymbolsOf S) *) * by FUNCT_2:def_1;
reconsider LS = LettersOf S as non empty Subset of (AllSymbolsOf S) ;
set L1 = 1 -tuples_on LS;
defpred S1[ Nat] means (S -termsOfMaxDepth) . $1 is S -prefix ;
A2: S1[ 0 ]
proof
(1 -tuples_on LS) /\ (1 -tuples_on (AllSymbolsOf S)) = 1 -tuples_on (LS /\ (AllSymbolsOf S)) by FOMODEL0:3
.= 1 -tuples_on LS by XBOOLE_1:28 ;
then reconsider L11 = 1 -tuples_on LS as Subset of (1 -tuples_on (AllSymbolsOf S)) ;
(S -termsOfMaxDepth) . 0 = AtomicTermsOf S by Def30
.= L11 ;
hence  S1[ 0 ] ; ::_thesis: verum
end;
A3: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A4: S1[m] ; ::_thesis: S1[m + 1]
reconsider mm = m, mm1 = m + 1 as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_for_t1,_t2,_w1,_w2_being_set_st_t1_in_((S_-termsOfMaxDepth)_._(m_+_1))_/\_((AllSymbolsOf_S)_*)_&_t2_in_((S_-termsOfMaxDepth)_._(m_+_1))_/\_((AllSymbolsOf_S)_*)_&_w1_in_(AllSymbolsOf_S)_*_&_w2_in_(AllSymbolsOf_S)_*_&_(S_-cons)_._(t1,w1)_=_(S_-cons)_._(t2,w2)_holds_
(_t1_=_t2_&_w1_=_w2_)
let t1, t2, w1, w2 be set ; ::_thesis: ( t1 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & t2 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & (S -cons) . (t1,w1) = (S -cons) . (t2,w2) implies ( t1 = t2 & w1 = w2 ) )
assume A5: ( t1 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & t2 in ((S -termsOfMaxDepth) . (m + 1)) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * ) ; ::_thesis: ( (S -cons) . (t1,w1) = (S -cons) . (t2,w2) implies ( t1 = t2 & w1 = w2 ) )
 ( t1 in (S -termsOfMaxDepth) . mm1 & not t1 in {{}} & t2 in (S -termsOfMaxDepth) . mm1 & not t2 in {{}} ) by A5;
then reconsider t11 = t1, t22 = t2 as mm + 1 -termal string of S by Def33, XBOOLE_0:def_5;
reconsider t111 = t11, t222 = t22 as FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
consider T1 being Element of ((S -termsOfMaxDepth) . mm) *  such that
A6: ( T1 is abs (ar ((S -firstChar) . t11)) -element & t11 = <*((S -firstChar) . t11)*> ^ ((S -multiCat) . T1) ) by Th3;
consider T2 being Element of ((S -termsOfMaxDepth) . mm) *  such that
A7: ( T2 is abs (ar ((S -firstChar) . t22)) -element & t22 = <*((S -firstChar) . t22)*> ^ ((S -multiCat) . T2) ) by Th3;
reconsider T11 = T1, T22 = T2 as FinSequence of (S -termsOfMaxDepth) . mm by FINSEQ_1:def_11;
reconsider w11 = w1, w22 = w2 as Element of (AllSymbolsOf S) * by A5;
reconsider head1 = (S -multiCat) . T1, head2 = (S -multiCat) . T2, tail1 = w11, tail2 = w22 as FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
assume  (S -cons) . (t1,w1) = (S -cons) . (t2,w2) ; ::_thesis: ( t1 = t2 & w1 = w2 )
then  t111 ^ w11 = (S -cons) . (t222,w22) by FOMODEL0:4;
then  (<*((S -firstChar) . t11)*> ^ ((S -multiCat) . T1)) ^ w11 = t222 ^ w22 by A6, FOMODEL0:4;
then  <*((S -firstChar) . t11)*> ^ (((S -multiCat) . T1) ^ w11) = (<*((S -firstChar) . t22)*> ^ ((S -multiCat) . T2)) ^ w22 by A7, FINSEQ_1:32;
then  <*((S -firstChar) . t11)*> ^ (head1 ^ tail1) = <*((S -firstChar) . t22)*> ^ (head2 ^ tail2) by FINSEQ_1:32;
then A8: (S -cons) . (<*((S -firstChar) . t11)*>,(head1 ^ tail1)) = <*((S -firstChar) . t22)*> ^ (head2 ^ tail2) by FOMODEL0:4;
 1 -tuples_on (AllSymbolsOf S) c= 1 -tuples_on (AllSymbolsOf S) ;
then reconsider S1 = 1 -tuples_on (AllSymbolsOf S) as Subset of (1 -tuples_on (AllSymbolsOf S)) ;
A9: S1 is S -cons -unambiguous by FOMODEL0:def_3;
 S1 /\ ((AllSymbolsOf S) *) = S1 by FINSEQ_2:134, XBOOLE_1:28;
then  ( <*((S -firstChar) . t11)*> in S1 /\ ((AllSymbolsOf S) *) & <*((S -firstChar) . t22)*> in S1 /\ ((AllSymbolsOf S) *) & head1 ^ tail1 in (AllSymbolsOf S) * & head2 ^ tail2 in (AllSymbolsOf S) * & (S -cons) . (<*((S -firstChar) . t11)*>,(head1 ^ tail1)) = (S -cons) . (<*((S -firstChar) . t22)*>,(head2 ^ tail2)) ) by A8, FOMODEL0:4;
then A10: ( <*((S -firstChar) . t11)*> = <*((S -firstChar) . t22)*> & head1 ^ tail1 = head2 ^ tail2 & head1 ^ tail1 = ((AllSymbolsOf S) -concatenation) . (head1,tail1) ) by A9, FOMODEL0:4, FOMODEL0:def_9;
A11: (S -firstChar) . t11 = (S -firstChar) . t22 by A10, FINSEQ_1:76;
set n = abs (ar ((S -firstChar) . t11));
 ( len T11 = abs (ar ((S -firstChar) . t11)) & len T22 = abs (ar ((S -firstChar) . t11)) ) by A6, A11, A7, CARD_1:def_7;
then  ( T11 in (abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m) & T22 in (abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m) & T11 in dom ((AllSymbolsOf S) -multiCat) & T22 in dom ((AllSymbolsOf S) -multiCat) ) by A1, FINSEQ_2:133;
then  ( ((AllSymbolsOf S) -multiCat) . T11 in ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) & ((AllSymbolsOf S) -multiCat) . T22 in ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) & ((AllSymbolsOf S) -multiCat) . T1 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -multiCat) . T2 in (AllSymbolsOf S) * ) by FUNCT_1:def_6;
then A12: ( ((AllSymbolsOf S) -multiCat) . T1 in (((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m))) /\ ((AllSymbolsOf S) *) & ((AllSymbolsOf S) -multiCat) . T2 in (((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m))) /\ ((AllSymbolsOf S) *) & w11 in (AllSymbolsOf S) * & w22 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . ((((AllSymbolsOf S) -multiCat) . T1),w11) = ((AllSymbolsOf S) -concatenation) . ((((AllSymbolsOf S) -multiCat) . T2),w22) ) by A10, FOMODEL0:4, XBOOLE_0:def_4;
 ( (S -termsOfMaxDepth) . m is AllSymbolsOf S -prefix & ( (S -termsOfMaxDepth) . m is AllSymbolsOf S -prefix implies ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) is AllSymbolsOf S -prefix ) ) by A4, Def28;
then  ((AllSymbolsOf S) -multiCat) .: ((abs (ar ((S -firstChar) . t11))) -tuples_on ((S -termsOfMaxDepth) . m)) is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def_3;
hence  ( t1 = t2 & w1 = w2 ) by A6, A7, A10, A12, FOMODEL0:def_9; ::_thesis: verum
end;
then  (S -termsOfMaxDepth) . (m + 1) is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def_9;
then  (S -termsOfMaxDepth) . (m + 1) is AllSymbolsOf S -prefix by FOMODEL0:def_3;
hence  S1[m + 1] ; ::_thesis: verum
end;
 for m being Nat holds S1[m] from NAT_1:sch_2(A2, A3);
hence  (S -termsOfMaxDepth) . m is S -prefix ; ::_thesis: verum
end;

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
proof
set SS = AllSymbolsOf S;
set s = the relational Element of S;
set V = the abs (ar the relational Element of S) -element Element of (AllTermsOf S) * ;
reconsider ss = the relational Element of S as Element of AllSymbolsOf S ;
reconsider tail = (S -multiCat) . the abs (ar the relational Element of S) -element Element of (AllTermsOf S) * as FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
reconsider IT = <*ss*> ^ tail as Element of ((AllSymbolsOf S) *) \ {{}} by FOMODEL0:5;
take  IT ; ::_thesis: IT is 0wff
thus  IT is 0wff by Def35; ::_thesis: verum
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
set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
consider s being relational Element of S, V being abs (ar s) -element Element of (AllTermsOf S) *  such that
A1: phi = <*s*> ^ ((S -multiCat) . V) by Def35;
reconsider ss = s as Element of AllSymbolsOf S ;
reconsider head = <*ss*> as FinSequence of AllSymbolsOf S ;
reconsider tail = (S -multiCat) . V as FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
(S -firstChar) . phi = (head ^ tail) . 1 by A1, FOMODEL0:6
.= s by FINSEQ_1:41 ;
hence  for b1 being Element of S st b1 = (S -firstChar) . phi holds
b1 is relational ; ::_thesis: verum
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
set SS = AllSymbolsOf S;
set AF = AtomicFormulasOf S;
defpred S1[ Element of ((AllSymbolsOf S) *) \ {{}}] means $1 is 0wff ;
  {  phi where phi is Element of ((AllSymbolsOf S) *) \ {{}} : S1[phi]  }  is Subset of (((AllSymbolsOf S) *) \ {{}}) from DOMAIN_1:sch_7();
hence  AtomicFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}}) ; ::_thesis: verum
end;
end;

registration
let S be Language;
cluster AtomicFormulasOf S ->  non empty ;
coherence
 not AtomicFormulasOf S is empty
proof
set AF = AtomicFormulasOf S;
set phi = the 0wff string of S;
 the 0wff string of S in AtomicFormulasOf S ;
hence  not AtomicFormulasOf S is empty ; ::_thesis: verum
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
set AF = AtomicFormulasOf S;
let phi be Element of AtomicFormulasOf S; ::_thesis: phi is 0wff
 phi in AtomicFormulasOf S ;
then consider x being string of S such that
A1: ( phi = x & x is 0wff ) ;
thus  phi is 0wff by A1; ::_thesis: verum
end;
end;

Lm10:  for S being Language holds AllTermsOf S is S -prefix
proof
let S be Language; ::_thesis: AllTermsOf S is S -prefix
set SS = AllSymbolsOf S;
set f = (AllSymbolsOf S) -concatenation ;
set F = (AllSymbolsOf S) -multiCat ;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
now__::_thesis:_for_t1,_t2,_w1,_w2_being_set_st_t1_in_(AllTermsOf_S)_/\_((AllSymbolsOf_S)_*)_&_t2_in_(AllTermsOf_S)_/\_((AllSymbolsOf_S)_*)_&_w1_in_(AllSymbolsOf_S)_*_&_w2_in_(AllSymbolsOf_S)_*_&_((AllSymbolsOf_S)_-concatenation)_._(t1,w1)_=_((AllSymbolsOf_S)_-concatenation)_._(t2,w2)_holds_
(_t1_=_t2_&_w1_=_w2_)
let t1, t2, w1, w2 be set ; ::_thesis: ( t1 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & t2 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) implies ( t1 = t2 & w1 = w2 ) )
assume A1: ( t1 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & t2 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) ) ; ::_thesis: ( t1 = t2 & w1 = w2 )
consider mm being Element of NAT  such that
A2: t1 in (S -termsOfMaxDepth) . mm by Lm6, A1;
consider nn being Element of NAT  such that
A3: t2 in (S -termsOfMaxDepth) . nn by Lm6, A1;
set p = mm + nn;
A4: (S -termsOfMaxDepth) . (mm + nn) is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def_3;
 ( (S -termsOfMaxDepth) . mm c= (S -termsOfMaxDepth) . (mm + nn) & (S -termsOfMaxDepth) . nn c= (S -termsOfMaxDepth) . (mm + nn) ) by Lm5;
then  ( t1 in ((S -termsOfMaxDepth) . (mm + nn)) /\ ((AllSymbolsOf S) *) & t2 in ((S -termsOfMaxDepth) . (mm + nn)) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) ) by A1, A2, A3, XBOOLE_0:def_4;
hence  ( t1 = t2 & w1 = w2 ) by A4, FOMODEL0:def_9; ::_thesis: verum
end;
then  AllTermsOf S is (AllSymbolsOf S) -concatenation -unambiguous by FOMODEL0:def_9;
then  AllTermsOf S is AllSymbolsOf S -prefix by FOMODEL0:def_3;
hence  AllTermsOf S is S -prefix ; ::_thesis: verum
end;

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 & 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
set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set s = (S -firstChar) . t;
set n = abs (ar ((S -firstChar) . t));
 t in AllTermsOf S by Def32;
then consider mmm being Element of NAT  such that
A1: t in (S -termsOfMaxDepth) . mmm by Lm6;
reconsider tt = t as mmm -termal string of S by A1, Def33;
reconsider tttt = t as non empty FinSequence of AllSymbolsOf S by FOMODEL0:5;
percases ( mmm = 0 or mmm <> 0 ) ;
suppose mmm = 0 ; ::_thesis: ex b1 being Element of (AllTermsOf S) * st
( b1 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b1) )
then reconsider ttt = tt as 0 -termal string of S ;
reconsider e = {} as Element of (AllTermsOf S) * by FINSEQ_1:49;
take  e ; ::_thesis: ( e is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e) )
 abs (ar ((S -firstChar) . ttt)) is zero ;
hence  e is abs (ar ((S -firstChar) . t)) -element ; ::_thesis: t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e)
A2: len ttt = 1 by CARD_1:def_7;
then tttt = <*(tttt /. 1)*> by FINSEQ_5:14
.= <*(tttt . 1)*> by A2, FINSEQ_4:15
.= <*(((AllSymbolsOf S) -firstChar) . t)*> ^ {} by FOMODEL0:6
.= <*(((AllSymbolsOf S) -firstChar) . t)*> ^ ((S -multiCat) . e) ;
hence  t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e) ; ::_thesis: verum
end;
suppose mmm <> 0 ; ::_thesis: ex b1 being Element of (AllTermsOf S) * st
( b1 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b1) )
then consider m being Nat such that
A3: mmm = m + 1 by NAT_1:6;
reconsider mm = m as Element of NAT by ORDINAL1:def_12;
reconsider ttt = tt as mm + 1 -termal string of S by A3;
consider ST being Element of ((S -termsOfMaxDepth) . mm) *  such that
A4: ( ST is abs (ar ((S -firstChar) . t)) -element & ttt = <*((S -firstChar) . ttt)*> ^ ((S -multiCat) . ST) ) by Th3;
reconsider TM = (S -termsOfMaxDepth) . mm as Subset of (AllTermsOf S) by Th2;
 ( ST in TM * & TM * c= (AllTermsOf S) * ) ;
then reconsider STT = ST as Element of (AllTermsOf S) * ;
take  STT ; ::_thesis: ( STT is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . STT) )
thus  ( STT is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . STT) ) by A4; ::_thesis: verum
end;
end;
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
set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set s = (S -firstChar) . t;
set n = abs (ar ((S -firstChar) . t));
A5: (AllSymbolsOf S) -multiCat is (abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S) -one-to-one by FOMODEL0:8;
A6: dom ((AllSymbolsOf S) -multiCat) = ((AllSymbolsOf S) *) * by FUNCT_2:def_1;
let IT1, IT2 be Element of (AllTermsOf S) * ; ::_thesis: ( IT1 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT1) & IT2 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) implies IT1 = IT2 )
reconsider IT11 = IT1, IT22 = IT2 as FinSequence of AllTermsOf S by FINSEQ_1:def_11;
assume A7: ( IT1 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT1) ) ; ::_thesis: ( not IT2 is abs (ar ((S -firstChar) . t)) -element or not t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) or IT1 = IT2 )
then  len IT11 = abs (ar ((S -firstChar) . t)) by CARD_1:def_7;
then reconsider IT111 = IT11 as Element of (abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S) by FINSEQ_2:133;
assume A8: ( IT2 is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . IT2) ) ; ::_thesis: IT1 = IT2
then  len IT22 = abs (ar ((S -firstChar) . t)) by CARD_1:def_7;
then reconsider IT222 = IT22 as Element of (abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S) by FINSEQ_2:133;
A9: ((AllSymbolsOf S) -multiCat) . IT111 = ((AllSymbolsOf S) -multiCat) . IT222 by A7, A8, FINSEQ_1:33;
 ( IT111 in ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S)) /\ (dom ((AllSymbolsOf S) -multiCat)) & IT222 in ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S)) /\ (dom ((AllSymbolsOf S) -multiCat)) ) by A6, XBOOLE_0:def_4;
hence  IT1 = IT2 by A9, A5, FOMODEL0:def_5; ::_thesis: verum
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 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 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
proof
 abs (ar t0) = 0 ;
hence  for b1 being Element of (AllTermsOf S) * st b1 = SubTerms t0 holds
b1 is empty ; ::_thesis: verum
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
set T = S -termsOfMaxDepth ;
set F = S -firstChar ;
set C = S -multiCat ;
set A = AllTermsOf S;
set SS = AllSymbolsOf S;
consider TT being Element of ((S -termsOfMaxDepth) . mm) *  such that
A1: ( TT is abs (ar t) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . TT) ) by Th3;
reconsider X = (S -termsOfMaxDepth) . mm as Subset of (AllTermsOf S) by Th2;
reconsider Y = X * as non empty Subset of ((AllTermsOf S) *) ;
reconsider TTTT = TT as Element of Y ;
reconsider TTT = TTTT as Element of (AllTermsOf S) * ;
 TTT = SubTerms t by Def37, A1;
hence  for b1 being Element of (AllTermsOf S) * st b1 = SubTerms t holds
b1 is (S -termsOfMaxDepth) . mm -valued ; ::_thesis: verum
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 :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)
proof
set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
consider s being relational Element of S, V being abs (ar s) -element Element of (AllTermsOf S) *  such that
A1: phi = <*s*> ^ ((S -multiCat) . V) by Def35;
reconsider ss = s as Element of AllSymbolsOf S ;
reconsider head = <*ss*> as FinSequence of AllSymbolsOf S ;
reconsider tail = (S -multiCat) . V as FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
A2: (S -firstChar) . phi = (head ^ tail) . 1 by A1, FOMODEL0:6
.= s by FINSEQ_1:41 ;
reconsider VV = V as abs (ar ((S -firstChar) . phi)) -element Element of (AllTermsOf S) * by A2;
take  VV ; ::_thesis: phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . VV)
thus  phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . VV) by A2, A1; ::_thesis: verum
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
set SS = AllSymbolsOf S;
set A = AllTermsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
set n = abs (ar ((S -firstChar) . phi));
A3: ( dom (S -multiCat) = ((AllSymbolsOf S) *) * & (AllTermsOf S) * c= ((AllSymbolsOf S) *) * ) by FUNCT_2:def_1;
reconsider s = (S -firstChar) . phi as Element of AllSymbolsOf S ;
reconsider head = <*s*> as FinSequence of AllSymbolsOf S ;
let IT1, IT2 be abs (ar ((S -firstChar) . phi)) -element Element of (AllTermsOf S) * ; ::_thesis: ( phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT1) & phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT2) implies IT1 = IT2 )
reconsider I1 = IT1, I2 = IT2 as FinSequence of AllTermsOf S by FINSEQ_1:def_11;
 ( len IT1 = abs (ar ((S -firstChar) . phi)) & len IT2 = abs (ar ((S -firstChar) . phi)) ) by CARD_1:def_7;
then reconsider I11 = I1, I22 = I2 as Element of (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) by FINSEQ_2:133;
reconsider tail1 = (S -multiCat) . IT1, tail2 = (S -multiCat) . IT2 as FinSequence of AllSymbolsOf S by FINSEQ_1:def_11;
assume A4: ( phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT1) & phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . IT2) ) ; ::_thesis: IT1 = IT2
 ( IT1 in dom (S -multiCat) & I11 in (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) & IT2 in dom (S -multiCat) & I22 in (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) ) by A3;
then A5: ( IT1 in ((abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S)) /\ (dom (S -multiCat)) & IT2 in ((abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S)) /\ (dom (S -multiCat)) & (S -multiCat) . IT1 = (S -multiCat) . IT2 ) by A4, FINSEQ_1:33, XBOOLE_0:def_4;
 S -multiCat is (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) -one-to-one by FOMODEL0:8;
hence  IT1 = IT2 by A5, FOMODEL0:def_5; ::_thesis: verum
end;
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) *) \ {{}})
proof
set SS = AllSymbolsOf S;
set A = AllTermsOf S;
now__::_thesis:_for_x_being_set_st_x_in_AllTermsOf_S_holds_
x_in_((AllSymbolsOf_S)_*)_\_{{}}
let x be set ; ::_thesis: ( x in AllTermsOf S implies x in ((AllSymbolsOf S) *) \ {{}} )
assume A1: x in AllTermsOf S ; ::_thesis: x in ((AllSymbolsOf S) *) \ {{}}
then reconsider t = x as Element of AllTermsOf S ;
 ( not x in {{}} & x in (AllSymbolsOf S) * ) by A1;
hence  x in ((AllSymbolsOf S) *) \ {{}} by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  AllTermsOf S is Element of bool (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def_3; ::_thesis: verum
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 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
proof
set SS = AllSymbolsOf S;
set A = AllTermsOf S;
deffunc H1( Element of AllTermsOf S) ->  Element of (AllTermsOf S) * = SubTerms $1;
consider f being Function of (AllTermsOf S),((AllTermsOf S) *) such that
A1: for t being Element of AllTermsOf S holds f . t = H1(t) from FUNCT_2:sch_4();
take  f ; ::_thesis: for t being Element of AllTermsOf S holds f . t = SubTerms t
thus  for t being Element of AllTermsOf S holds f . t = SubTerms t by A1; ::_thesis: verum
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
set A = AllTermsOf S;
let IT1, IT2 be Function of (AllTermsOf S),((AllTermsOf S) *); ::_thesis: ( ( for t being Element of AllTermsOf S holds IT1 . t = SubTerms t ) & ( for t being Element of AllTermsOf S holds IT2 . t = SubTerms t ) implies IT1 = IT2 )
assume A2: for t being Element of AllTermsOf S holds IT1 . t = SubTerms t ; ::_thesis: ( ex t being Element of AllTermsOf S st not IT2 . t = SubTerms t or IT1 = IT2 )
assume A3: for t being Element of AllTermsOf S holds IT2 . t = SubTerms t ; ::_thesis: IT1 = IT2
now__::_thesis:_for_t_being_Element_of_AllTermsOf_S_holds_IT1_._t_=_IT2_._t
let t be Element of AllTermsOf S; ::_thesis: IT1 . t = IT2 . t
thus IT1 . t = SubTerms t by A2
.= IT2 . t by A3 ; ::_thesis: verum
end;
hence  IT1 = IT2 by FUNCT_2:63; ::_thesis: verum
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
let S be Language; ::_thesis: (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)}
set o = the OneF of S;
set z = the ZeroF of S;
set f = the adicity of S;
set R = RelSymbolsOf S;
set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
set e = TheEqSymbOf S;
set n = TheNorSymbOf S;
set A = AtomicFormulaSymbolsOf S;
set D = the carrier of S \ { the OneF of S};
A1: TheEqSymbOf S in AtomicFormulaSymbolsOf S ;
(AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) = (AtomicFormulaSymbolsOf S) \ ((AllSymbolsOf S) \ ({ the ZeroF of S} \/ { the OneF of S})) by ENUMSET1:1
.= (AtomicFormulaSymbolsOf S) \ ((AtomicFormulaSymbolsOf S) \ { the ZeroF of S}) by XBOOLE_1:41
.= ((AtomicFormulaSymbolsOf S) \ (AtomicFormulaSymbolsOf S)) \/ ((AtomicFormulaSymbolsOf S) /\ { the ZeroF of S}) by XBOOLE_1:52
.= { the ZeroF of S} by A1, ZFMISC_1:46 ;
hence  (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)} ; ::_thesis: verum
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
let S be Language; ::_thesis: (AtomicFormulaSymbolsOf S) \ (RelSymbolsOf S) = TermSymbolsOf S
set R = RelSymbolsOf S;
set SSS = AtomicFormulaSymbolsOf S;
set f = the adicity of S;
 the adicity of S " INT = AtomicFormulaSymbolsOf S by FUNCT_2:40;
hence (AtomicFormulaSymbolsOf S) \ (RelSymbolsOf S) = the adicity of S " (INT \ (INT \ NAT)) by FUNCT_1:69
.= the adicity of S " ((INT \ INT) \/ (INT /\ NAT)) by XBOOLE_1:52
.= TermSymbolsOf S by XBOOLE_1:7, XBOOLE_1:28 ;
::_thesis: verum
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
set R = RelSymbolsOf S;
set SSS = AtomicFormulaSymbolsOf S;
set T = TermSymbolsOf S;
let s be ofAtomicFormula Element of S; ::_thesis: ( not s is relational implies s is termal )
assume  not s is relational ; ::_thesis: s is termal
then  ( s in AtomicFormulaSymbolsOf S & not s in RelSymbolsOf S ) by Def17, Def20;
then  s in (AtomicFormulaSymbolsOf S) \ (RelSymbolsOf S) by XBOOLE_0:def_5;
then  s in TermSymbolsOf S by Th11;
hence  s is termal by Def18; ::_thesis: verum
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
set L = LettersOf S;
set P = OpSymbolsOf S;
set T = TermSymbolsOf S;
set f = the adicity of S;
let s be termal Element of S; ::_thesis: ( not s is literal implies s is operational )
A1: s in TermSymbolsOf S by Def18;
assume  not s is literal ; ::_thesis: s is operational
then  not s in LettersOf S by Def14;
then  ( s in (TermSymbolsOf S) \ (LettersOf S) & (TermSymbolsOf S) \ (LettersOf S) = OpSymbolsOf S ) by A1, FUNCT_1:69, XBOOLE_0:def_5;
hence  s is operational by Def16; ::_thesis: verum
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
let x be set ; ::_thesis: for S being Language holds
( x is string of S iff x is non empty Element of (AllSymbolsOf S) * )
let S be Language; ::_thesis: ( x is string of S iff x is non empty Element of (AllSymbolsOf S) * )
set SS = AllSymbolsOf S;
 ( x is string of S iff ( x in (AllSymbolsOf S) * & not x in {{}} ) ) by XBOOLE_0:def_5;
hence  ( x is string of S iff x is non empty Element of (AllSymbolsOf S) * ) ; ::_thesis: verum
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 )
proof
let x be set ; ::_thesis: for S being Language holds
( x is string of S iff x is non empty FinSequence of AllSymbolsOf S )
let S be Language; ::_thesis: ( x is string of S iff x is non empty FinSequence of AllSymbolsOf S )
 ( x is non empty FinSequence of AllSymbolsOf S iff x is non empty Element of (AllSymbolsOf S) * ) by FINSEQ_1:def_11;
hence  ( x is string of S iff x is non empty FinSequence of AllSymbolsOf S ) by Th12; ::_thesis: verum
end;

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
proof
set N = TheNorSymbOf S;
set f = the adicity of S;
set Low = LowerCompoundersOf S;
set SS = AllSymbolsOf S;
A1: ( dom the adicity of S = (AllSymbolsOf S) \ {(TheNorSymbOf S)} & TheNorSymbOf S in {(TheNorSymbOf S)} ) by FUNCT_2:def_1, TARSKI:def_1;
 not TheNorSymbOf S in LowerCompoundersOf S by A1, XBOOLE_0:def_5;
hence  for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is low-compounding by Def15; ::_thesis: verum
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
set N = TheNorSymbOf S;
set f = the adicity of S;
set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
 TheNorSymbOf S in { the ZeroF of S,(TheNorSymbOf S)} by TARSKI:def_2;
then  not TheNorSymbOf S in OwnSymbolsOf S by XBOOLE_0:def_5;
hence  for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is own by Def19; ::_thesis: verum
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
let S be Language; ::_thesis: for s being Element of S st s <> TheNorSymbOf S & s <> TheEqSymbOf S holds
s in OwnSymbolsOf S
let s be Element of S; ::_thesis: ( s <> TheNorSymbOf S & s <> TheEqSymbOf S implies s in OwnSymbolsOf S )
set O = OwnSymbolsOf S;
set R = RelSymbolsOf S;
set E = TheEqSymbOf S;
set X = (RelSymbolsOf S) \ (OwnSymbolsOf S);
set N = TheNorSymbOf S;
set SS = AllSymbolsOf S;
assume  ( s <> TheNorSymbOf S & s <> TheEqSymbOf S ) ; ::_thesis: s in OwnSymbolsOf S
then  ( not s in {(TheNorSymbOf S)} & not s in {(TheEqSymbOf S)} ) by TARSKI:def_1;
then  not s in {(TheNorSymbOf S)} \/ {(TheEqSymbOf S)} by XBOOLE_0:def_3;
then  not s in {(TheNorSymbOf S),(TheEqSymbOf S)} by ENUMSET1:1;
hence  s in OwnSymbolsOf S by XBOOLE_0:def_5; ::_thesis: verum
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
defpred S1[ Nat] means t is $1 -termal ;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
reconsider TF = S -termsOfMaxDepth as Function ;
 t in AllTermsOf S by Def32;
then consider mm being Element of NAT  such that
A1: t in TF . mm by Lm6;
 t is mm -termal by Def33, A1;
then A2: ex n being Nat st S1[n] ;
consider IT being Nat such that
A3: ( S1[IT] & ( for n being Nat st S1[n] holds
IT <= n ) ) from NAT_1:sch_5(A2);
take  IT ; ::_thesis: ( t is IT -termal & ( for n being Nat st t is n -termal holds
IT <= n ) )
thus  ( t is IT -termal & ( for n being Nat st t is n -termal holds
IT <= n ) ) by A3; ::_thesis: verum
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
let IT1, IT2 be Nat; ::_thesis: ( t is IT1 -termal & ( for n being Nat st t is n -termal holds
IT1 <= n ) & t is IT2 -termal & ( for n being Nat st t is n -termal holds
IT2 <= n ) implies IT1 = IT2 )
set phi = t;
assume A4: ( t is IT1 -termal & ( for n being Nat st t is n -termal holds
IT1 <= n ) ) ; ::_thesis: ( not t is IT2 -termal or ex n being Nat st
( t is n -termal & not IT2 <= n ) or IT1 = IT2 )
assume A5: ( t is IT2 -termal & ( for n being Nat st t is n -termal holds
IT2 <= n ) ) ; ::_thesis: IT1 = IT2
A6: IT2 <= IT1 by A5, A4;
 IT1 <= IT2 by A4, A5;
hence  IT1 = IT2 by A6, XXREAL_0:1; ::_thesis: verum
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 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
proof
set f = the adicity of S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
 s in LowerCompoundersOf S by Def15;
then  ( s in dom the adicity of S & the adicity of S . s in INT \ {0} ) by FUNCT_1:def_7;
then  not the adicity of S . s in {0} by XBOOLE_0:def_5;
hence  for b1 being number st b1 = ar s holds
not b1 is empty by TARSKI:def_1; ::_thesis: verum
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
set f = the adicity of S;
set T = TermSymbolsOf S;
 s in TermSymbolsOf S by Def18;
then reconsider nn = ar s as Element of NAT by FUNCT_1:def_7;
 not nn is negative ;
hence  ( not ar s is negative & ar s is ext-real ) ; ::_thesis: verum
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
set f = the adicity of S;
set R = RelSymbolsOf S;
 s in RelSymbolsOf S by Def17;
then  ( s in dom the adicity of S & the adicity of S . s in INT \ NAT ) by FUNCT_1:def_7;
then A1: ( ar s in INT & not ar s in NAT ) by XBOOLE_0:def_5;
reconsider IT = ar s as Element of INT ;
thus  ( ar s is negative & ar s is ext-real ) by A1, INT_1:3; ::_thesis: verum
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
let S be Language; ::_thesis: for t being termal string of S st not t is 0 -termal holds
( (S -firstChar) . t is operational & SubTerms t <> {} )
let t be termal string of S; ::_thesis: ( not t is 0 -termal implies ( (S -firstChar) . t is operational & SubTerms t <> {} ) )
set T = S -termsOfMaxDepth ;
set m = Depth t;
set ST = SubTerms t;
set TT = AllTermsOf S;
assume  not t is 0 -termal ; ::_thesis: ( (S -firstChar) . t is operational & SubTerms t <> {} )
then  Depth t <> 0 by Def40;
then consider n being Nat such that
A1: Depth t = n + 1 by NAT_1:6;
set F = S -firstChar ;
set C = S -multiCat ;
set Fam =  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  ;
 n < Depth t by A1, NAT_1:16;
then  ( not t is n -termal & t is Depth t -termal ) by Def40;
then  ( not t in (S -termsOfMaxDepth) . n & t in (S -termsOfMaxDepth) . (n + 1) ) by A1, Def33;
then  ( t in (union  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  ) \/ ((S -termsOfMaxDepth) . n) & not t in (S -termsOfMaxDepth) . n ) by Def30;
then  t in union  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  by XBOOLE_0:def_3;
then consider x being set  such that
A2: ( t in x & x in  {  (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational  }  ) by TARSKI:def_4;
consider s being ofAtomicFormula Element of S such that
A3: ( x = Compound (s,((S -termsOfMaxDepth) . n)) & s is operational ) by A2;
set k = abs (ar s);
consider StringTuple being Element of ((AllSymbolsOf S) *) *  such that
A4: ( t = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= (S -termsOfMaxDepth) . n & StringTuple is abs (ar s) -element ) by A2, A3;
A5: (S -firstChar) . t = (<*s*> ^ ((S -multiCat) . StringTuple)) . 1 by A4, FOMODEL0:6
.= <*s*> . 1 by FOMODEL0:28
.= s by FINSEQ_1:40 ;
hence  (S -firstChar) . t is operational by A3; ::_thesis: SubTerms t <> {}
reconsider k1 = abs (ar s) as non zero Nat by A3;
reconsider STT = SubTerms t as k1 + 0 -element Element of (AllTermsOf S) * by A5;
 STT <> {} ;
hence  SubTerms t <> {} ; ::_thesis: verum
end;

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
proof
set C = S -multiCat ;
set SS = AllSymbolsOf S;
set g = (AllSymbolsOf S) -concatenation ;
set G = MultPlace ((AllSymbolsOf S) -concatenation);
consider m being Nat such that
A1: m + 1 = len W by NAT_1:6;
reconsider WW = W as (m + 1) + 0 -element FinSequence by A1, CARD_1:def_7;
A2: {(WW . (m + 1))} \ (((AllSymbolsOf S) *) \ {{}}) = {} ;
then A3: WW . (m + 1) in ((AllSymbolsOf S) *) \ {{}} by ZFMISC_1:60;
reconsider last = WW . (m + 1) as string of S by A2, ZFMISC_1:60;
reconsider lastt = WW . (m + 1) as Element of (AllSymbolsOf S) * by A3;
set VV = WW | (Seg m);
reconsider VVV = WW | (Seg m) as (AllSymbolsOf S) * -valued FinSequence ;
 ((WW | (Seg m)) ^ <*(WW . (m + 1))*>) \+\ WW = {} ;
then A4: (MultPlace ((AllSymbolsOf S) -concatenation)) . W = (MultPlace ((AllSymbolsOf S) -concatenation)) . (VVV ^ <*lastt*>) by FOMODEL0:29;
percases ( VVV is empty or not VVV is empty ) ;
suppose VVV is empty ; ::_thesis: for b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty
then (MultPlace ((AllSymbolsOf S) -concatenation)) . W = (MultPlace ((AllSymbolsOf S) -concatenation)) . <*lastt*> by A4, FINSEQ_1:34
.= last by FOMODEL0:31 ;
hence  for b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty by FOMODEL0:32; ::_thesis: verum
end;
supposeA5: not VVV is empty ; ::_thesis: for b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty
then reconsider VVVV = VVV as Element of (((AllSymbolsOf S) *) *) \ {{}} by FOMODEL0:30;
(MultPlace ((AllSymbolsOf S) -concatenation)) . W = ((AllSymbolsOf S) -concatenation) . (((MultPlace ((AllSymbolsOf S) -concatenation)) . VVV),lastt) by A5, A4, FOMODEL0:31
.= ((MultPlace ((AllSymbolsOf S) -concatenation)) . VVVV) ^ last by FOMODEL0:4 ;
hence  for b1 being set st b1 = (S -multiCat) . W holds
not b1 is empty by FOMODEL0:32; ::_thesis: verum
end;
end;
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
set w = <*l*>;
set L = LettersOf S;
set AT = AtomicTermsOf S;
set T = S -termsOfMaxDepth ;
reconsider ll = l as Element of LettersOf S by Def14;
 <*l*> = <*ll*> ;
then  <*l*> in AtomicTermsOf S ;
then  <*l*> in (S -termsOfMaxDepth) . 0 by Def30;
hence  for b1 being string of S st b1 = <*l*> holds
b1 is 0 -termal by Def33; ::_thesis: verum
end;
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
proof
set T = S -termsOfMaxDepth ;
let t be string of S; ::_thesis: ( t is m + (0 * n) -termal implies t is m + n -termal )
assume  t is m + (0 * n) -termal ; ::_thesis: t is m + n -termal
then  ( t in (S -termsOfMaxDepth) . m & (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n) ) by Def33, Lm5;
hence  t is m + n -termal by Def33; ::_thesis: verum
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
set L = LettersOf S;
set P = OpSymbolsOf S;
set O = OwnSymbolsOf S;
set T = TermSymbolsOf S;
A1: (TermSymbolsOf S) \ (LettersOf S) = OpSymbolsOf S by FUNCT_1:69;
let s be own Element of S; ::_thesis: ( not s is low-compounding implies s is literal )
reconsider ss = s as ofAtomicFormula Element of S ;
assume A2: not s is low-compounding ; ::_thesis: s is literal
then  not ss is relational ;
then reconsider sss = ss as termal ofAtomicFormula Element of S ;
assume  not s is literal ; ::_thesis: contradiction
then  ( sss in TermSymbolsOf S & not s in LettersOf S ) by Def18;
then  s in (TermSymbolsOf S) \ (LettersOf S) by XBOOLE_0:def_5;
then  ( s is operational & not s is operational ) by A2, A1, Def16;
hence  contradiction ; ::_thesis: verum
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
set SS = AllSymbolsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
set ST = SubTerms t;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
reconsider TTT = AllTermsOf S as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
 t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . (SubTerms t)) by Def37;
then  rng ((S -multiCat) . (SubTerms t)) c= rng t by FINSEQ_1:30;
then  (S -multiCat) . (SubTerms t) is rng t -valued by RELAT_1:def_19;
hence  for b1 being Relation st b1 = SubTerms t holds
b1 is (rng t) * -valued by FOMODEL0:42; ::_thesis: verum
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
set SS = AllSymbolsOf S;
set C = S -multiCat ;
set F = S -firstChar ;
set ST = SubTerms phi0;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
reconsider TTT = AllTermsOf S as non empty Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
 phi0 = <*((S -firstChar) . phi0)*> ^ ((S -multiCat) . (SubTerms phi0)) by Def38;
then  rng ((S -multiCat) . (SubTerms phi0)) c= rng phi0 by FINSEQ_1:30;
then  (S -multiCat) . (SubTerms phi0) is rng phi0 -valued by RELAT_1:def_19;
hence  for b1 being Relation st b1 = SubTerms phi0 holds
b1 is (rng phi0) * -valued by FOMODEL0:42; ::_thesis: verum
end;
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) *) \ {{}}))
proof
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
now__::_thesis:_for_y_being_set_st_y_in_rng_(S_-termsOfMaxDepth)_holds_
y_in_bool_(((AllSymbolsOf_S)_*)_\_{{}})
let y be set ; ::_thesis: ( y in rng (S -termsOfMaxDepth) implies y in bool (((AllSymbolsOf S) *) \ {{}}) )
assume  y in rng (S -termsOfMaxDepth) ; ::_thesis: y in bool (((AllSymbolsOf S) *) \ {{}})
then consider x being set  such that
A1: ( x in dom (S -termsOfMaxDepth) & (S -termsOfMaxDepth) . x = y ) by FUNCT_1:def_3;
reconsider mm = x as Element of NAT by A1;
 (S -termsOfMaxDepth) . mm misses {{}}
proof
assume  (S -termsOfMaxDepth) . mm meets {{}} ; ::_thesis: contradiction
then  ((S -termsOfMaxDepth) . mm) /\ {{}} <> {} by XBOOLE_0:def_7;
then consider z being set  such that
A2: z in ((S -termsOfMaxDepth) . mm) /\ {{}} by XBOOLE_0:def_1;
thus  contradiction by A2; ::_thesis: verum
end;
then  (S -termsOfMaxDepth) . mm c= ((AllSymbolsOf S) *) \ {{}} by XBOOLE_1:86;
hence  y in bool (((AllSymbolsOf S) *) \ {{}}) by A1; ::_thesis: verum
end;
then  rng (S -termsOfMaxDepth) c= bool (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def_3;
hence  S -termsOfMaxDepth is Function of NAT,(bool (((AllSymbolsOf S) *) \ {{}})) by FUNCT_2:6; ::_thesis: verum
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
let m be Nat; ::_thesis: for S being Language holds (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) *
let S be Language; ::_thesis: (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) *
set TS = TermSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
set P = OpSymbolsOf S;
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set CC = (TermSymbolsOf S) -multiCat ;
defpred S1[ Nat] means (S -termsOfMaxDepth) . $1 c= (TermSymbolsOf S) * ;
A1: S1[ 0 ]
proof
now__::_thesis:_for_x_being_set_st_x_in_(S_-termsOfMaxDepth)_._0_holds_
x_in_(TermSymbolsOf_S)_*
let x be set ; ::_thesis: ( x in (S -termsOfMaxDepth) . 0 implies x in (TermSymbolsOf S) * )
assume  x in (S -termsOfMaxDepth) . 0 ; ::_thesis: x in (TermSymbolsOf S) *
then reconsider t = x as 0 -termal string of S by Def33;
reconsider s = (S -firstChar) . t as termal Element of S ;
set sub = SubTerms t;
reconsider ss = s as Element of TermSymbolsOf S by Def18;
t = <*s*> ^ ((S -multiCat) . (SubTerms t)) by Def37
.= <*s*> ^ {}
.= <*ss*> ;
then  t is FinSequence of TermSymbolsOf S ;
hence  x in (TermSymbolsOf S) * by FINSEQ_1:def_11; ::_thesis: verum
end;
hence  S1[ 0 ] by TARSKI:def_3; ::_thesis: verum
end;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def_12;
assume  S1[n] ; ::_thesis: S1[n + 1]
then reconsider Tn = (S -termsOfMaxDepth) . nn as non empty Subset of ((TermSymbolsOf S) *) ;
now__::_thesis:_for_x_being_set_st_x_in_(S_-termsOfMaxDepth)_._(n_+_1)_holds_
x_in_(TermSymbolsOf_S)_*
let x be set ; ::_thesis: ( x in (S -termsOfMaxDepth) . (n + 1) implies b1 in (TermSymbolsOf S) * )
assume  x in (S -termsOfMaxDepth) . (n + 1) ; ::_thesis: b1 in (TermSymbolsOf S) *
then  x in (S -termsOfMaxDepth) . NN ;
then reconsider t = x as n + 1 -termal string of S by Def33;
set s = (S -firstChar) . t;
set m = abs (ar ((S -firstChar) . t));
reconsider tt = t as nn + 1 -termal string of S ;
percases ( not t is 0 -termal or t is 0 -termal ) ;
suppose not t is 0 -termal ; ::_thesis: b1 in (TermSymbolsOf S) *
then A3: (S -firstChar) . t is operational by Th16;
then  ( (S -firstChar) . t in OpSymbolsOf S & OpSymbolsOf S c= TermSymbolsOf S ) by Def16, Th1;
then reconsider ss = (S -firstChar) . t as Element of TermSymbolsOf S ;
reconsider m1 = abs (ar ((S -firstChar) . t)) as non zero Nat by A3;
 SubTerms tt is (S -termsOfMaxDepth) . nn -valued ;
then reconsider sub = SubTerms t as m1 + 0 -element FinSequence of Tn by FOMODEL0:26;
 ( sub in Tn * & Tn * c= ((TermSymbolsOf S) *) * ) by FINSEQ_1:def_11;
then reconsider subb = sub as m1 + 0 -element Element of ((TermSymbolsOf S) *) * ;
 ( sub is Tn -valued & Tn c= (TermSymbolsOf S) * & TermSymbolsOf S c= AllSymbolsOf S ) by XBOOLE_1:1;
then <*ss*> ^ (((TermSymbolsOf S) -multiCat) . subb) = <*((S -firstChar) . t)*> ^ ((S -multiCat) . (SubTerms t)) by FOMODEL0:53
.= t by Def37 ;
then reconsider tt = t as FinSequence of TermSymbolsOf S by FOMODEL0:26;
 tt in (TermSymbolsOf S) * by FINSEQ_1:def_11;
hence  x in (TermSymbolsOf S) * ; ::_thesis: verum
end;
suppose t is 0 -termal ; ::_thesis: b1 in (TermSymbolsOf S) *
then  x in (S -termsOfMaxDepth) . 0 by Def33;
hence  x in (TermSymbolsOf S) * by A1; ::_thesis: verum
end;
end;
end;
hence  S1[n + 1] by TARSKI:def_3; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) * ; ::_thesis: verum
end;

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
proof
set d = Depth t;
 t is (Depth t) + (0 * m) -termal by Def40;
hence  for b1 being string of S st b1 = t null m holds
b1 is (Depth t) + m -termal ; ::_thesis: verum
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
set T = S -termsOfMaxDepth ;
set TS = TermSymbolsOf S;
let w be string of S; ::_thesis: ( w is termal implies w is TermSymbolsOf S -valued )
assume  w is termal ; ::_thesis: w is TermSymbolsOf S -valued
then reconsider tt = w as termal string of S ;
set d = Depth tt;
reconsider t = tt null 0 as (Depth tt) + 0 -termal string of S ;
 ( t in (S -termsOfMaxDepth) . (Depth tt) & (S -termsOfMaxDepth) . (Depth tt) c= (TermSymbolsOf S) * ) by Lm11, Def33;
hence  w is TermSymbolsOf S -valued ; ::_thesis: verum
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
set TT = AllTermsOf S;
set TS = TermSymbolsOf S;
now__::_thesis:_for_x_being_set_st_x_in_AllTermsOf_S_holds_
x_in_(TermSymbolsOf_S)_*
let x be set ; ::_thesis: ( x in AllTermsOf S implies x in (TermSymbolsOf S) * )
assume  x in AllTermsOf S ; ::_thesis: x in (TermSymbolsOf S) *
then reconsider t = x as termal string of S ;
 t is FinSequence of TermSymbolsOf S by FOMODEL0:26;
hence  x in (TermSymbolsOf S) * by FINSEQ_1:def_11; ::_thesis: verum
end;
then  AllTermsOf S c= (TermSymbolsOf S) * by TARSKI:def_3;
hence  for b1 being set st b1 = (AllTermsOf S) \ ((TermSymbolsOf S) *) holds
b1 is empty ; ::_thesis: verum
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
set sub = SubTerms phi0;
set TS = TermSymbolsOf S;
set TT = AllTermsOf S;
 (AllTermsOf S) \ ((TermSymbolsOf S) *) = {} ;
then reconsider TTT = AllTermsOf S as non empty Subset of ((TermSymbolsOf S) *) by XBOOLE_1:37;
 SubTerms phi0 is TTT -valued ;
hence  SubTerms phi0 is (TermSymbolsOf S) * -valued ; ::_thesis: verum
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
set TS = TermSymbolsOf S;
set AS = AtomicFormulaSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
set TT = AllTermsOf S;
set CC = (TermSymbolsOf S) -multiCat ;
set SS = AllSymbolsOf S;
let w be string of S; ::_thesis: ( w is 0wff implies w is AtomicFormulaSymbolsOf S -valued )
assume  w is 0wff ; ::_thesis: w is AtomicFormulaSymbolsOf S -valued
then reconsider phi = w as 0wff string of S ;
reconsider r = (S -firstChar) . phi as relational Element of S ;
set m = abs (ar r);
reconsider rr = r as Element of AtomicFormulaSymbolsOf S by Def20;
reconsider sub = SubTerms phi as (abs (ar r)) + 0 -element Element of (AllTermsOf S) * ;
 (AllTermsOf S) \ ((TermSymbolsOf S) *) = {} ;
then  ( TermSymbolsOf S c= AllSymbolsOf S & AllTermsOf S c= (TermSymbolsOf S) * & sub is AllTermsOf S -valued ) by XBOOLE_1:1, XBOOLE_1:37;
then <*rr*> ^ (((TermSymbolsOf S) -multiCat) . sub) = <*r*> ^ ((S -multiCat) . sub) by FOMODEL0:53
.= phi by Def38 ;
hence  w is AtomicFormulaSymbolsOf S -valued ; ::_thesis: verum
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
let S be Language; ::_thesis: for phi0 being 0wff string of S st (S -firstChar) . phi0 <> TheEqSymbOf S holds
phi0 is OwnSymbolsOf S -valued
let phi0 be 0wff string of S; ::_thesis: ( (S -firstChar) . phi0 <> TheEqSymbOf S implies phi0 is OwnSymbolsOf S -valued )
set O = OwnSymbolsOf S;
set F = S -firstChar ;
set r = (S -firstChar) . phi0;
set C = S -multiCat ;
set sub = SubTerms phi0;
set E = TheEqSymbOf S;
set R = RelSymbolsOf S;
reconsider TS = TermSymbolsOf S as non empty Subset of (OwnSymbolsOf S) by Th1;
assume  (S -firstChar) . phi0 <> TheEqSymbOf S ; ::_thesis: phi0 is OwnSymbolsOf S -valued
then  not (S -firstChar) . phi0 in {(TheEqSymbOf S)} by TARSKI:def_1;
then  not (S -firstChar) . phi0 in (RelSymbolsOf S) \ (OwnSymbolsOf S) by Th1;
then  ( (S -firstChar) . phi0 in OwnSymbolsOf S or not (S -firstChar) . phi0 in RelSymbolsOf S ) by XBOOLE_0:def_5;
then reconsider rr = (S -firstChar) . phi0 as Element of OwnSymbolsOf S by Def17;
 (S -multiCat) . (SubTerms phi0) is TS -valued by FOMODEL0:54;
then reconsider tail = (S -multiCat) . (SubTerms phi0) as OwnSymbolsOf S -valued FinSequence ;
 phi0 = <*rr*> ^ tail by Def38;
hence  phi0 is OwnSymbolsOf S -valued ; ::_thesis: verum
end;

registration
cluster non empty strict for Language-like ;
existence
 ex b1 being Language-like st
( b1 is strict & not b1 is empty )
proof
set a = the Function of (NAT \ {0}),INT;
take IT = Language-like(# NAT,0,0, the Function of (NAT \ {0}),INT #); ::_thesis: ( IT is strict & not IT is empty )
thus  ( IT is strict & not IT is empty ) ; ::_thesis: verum
end;
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 & 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;
clusterS null  -> S -extending for Language-like ;
coherence
 for b1 being Language-like st b1 = S null holds
b1 is S -extending
proof
set E = TheEqSymbOf S;
set N = TheNorSymbOf S;
set f = the adicity of S;
 ( the adicity of S c= the adicity of S & TheEqSymbOf S = TheEqSymbOf S & TheNorSymbOf S = TheNorSymbOf S ) ;
hence  for b1 being Language-like st b1 = S null holds
b1 is S -extending by Def41; ::_thesis: verum
end;
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
reconsider SS = S null as Language ;
take  SS ; ::_thesis: SS is S -extending
thus  SS is S -extending ; ::_thesis: verum
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
set O1 = OwnSymbolsOf S1;
set O2 = OwnSymbolsOf S2;
set f1 = the adicity of S1;
set f2 = the adicity of S2;
set A1 = AtomicFormulaSymbolsOf S1;
set SS1 = AllSymbolsOf S1;
set SS2 = AllSymbolsOf S2;
set z1 = the ZeroF of S1;
set o1 = the OneF of S1;
set z2 = the ZeroF of S2;
set o2 = the OneF of S2;
set E1 = TheEqSymbOf S1;
set E2 = TheEqSymbOf S2;
set N1 = TheNorSymbOf S1;
set N2 = TheNorSymbOf S2;
A1: ( dom the adicity of S1 = (AllSymbolsOf S1) \ { the OneF of S1} & dom the adicity of S2 = (AllSymbolsOf S2) \ { the OneF of S2} ) by FUNCT_2:def_1;
 the adicity of S1 c= the adicity of S2 by Def41;
then  (AllSymbolsOf S1) \ { the OneF of S1} c= (AllSymbolsOf S2) \ { the OneF of S2} by A1, GRFUNC_1:2;
then  ((AllSymbolsOf S1) \ {(TheNorSymbOf S1)}) \ {(TheEqSymbOf S1)} c= ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) \ {(TheEqSymbOf S1)} by XBOOLE_1:33;
then  (AllSymbolsOf S1) \ ({(TheNorSymbOf S1)} \/ {(TheEqSymbOf S1)}) c= ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) \ {(TheEqSymbOf S1)} by XBOOLE_1:41;
then  (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= ((AllSymbolsOf S2) \ {(TheNorSymbOf S2)}) \ {(TheEqSymbOf S1)} by ENUMSET1:1;
then  (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= (AllSymbolsOf S2) \ ({(TheNorSymbOf S2)} \/ {(TheEqSymbOf S1)}) by XBOOLE_1:41;
then  (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= (AllSymbolsOf S2) \ ({(TheNorSymbOf S2)} \/ {(TheEqSymbOf S2)}) by Def41;
then  (AllSymbolsOf S1) \ {(TheNorSymbOf S1),(TheEqSymbOf S1)} c= (AllSymbolsOf S2) \ {(TheNorSymbOf S2),(TheEqSymbOf S2)} by ENUMSET1:1;
hence  (OwnSymbolsOf S1) \ (OwnSymbolsOf S2) is empty ; ::_thesis: verum
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);
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 & 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
 the ZeroF of L is Element of the carrier of L null (dom f) ;
then reconsider z1 = the ZeroF of L as Element of the carrier of L \/ (dom f) by TARSKI:def_3;
 the OneF of L is Element of the carrier of L null (dom f) ;
then reconsider o1 = the OneF of L as Element of the carrier of L \/ (dom f) by TARSKI:def_3;
A1: dom the adicity of L = the carrier of L \ { the OneF of L} by FUNCT_2:def_1;
A2: dom (f | ((dom f) \ { the OneF of L})) = (dom f) /\ ((dom f) \ { the OneF of L}) by RELAT_1:61
.= (dom f) \ ({ the OneF of L} null (dom f)) ;
dom ((f | ((dom f) \ { the OneF of L})) +* the adicity of L) = ((dom f) \ { the OneF of L}) \/ ( the carrier of L \ { the OneF of L}) by A1, A2, FUNCT_4:def_1
.= ((dom f) \/ the carrier of L) \ { the OneF of L} by XBOOLE_1:42 ;
then  ( dom ((f | ((dom f) \ { the OneF of L})) +* the adicity of L) = ( the carrier of L \/ (dom f)) \ {o1} & rng ((f | ((dom f) \ { the OneF of L})) +* the adicity of L) c= INT ) ;
then  (f | ((dom f) \ { the OneF of L})) +* the adicity of L is Element of Funcs ((( the carrier of L \/ (dom f)) \ {o1}),INT) by FUNCT_2:def_2;
then reconsider a11 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L as Function of (( the carrier of L \/ (dom f)) \ {o1}),INT ;
set new = Language-like(# ( the carrier of L \/ (dom f)),z1,o1,a11 #);
reconsider new = Language-like(# ( the carrier of L \/ (dom f)),z1,o1,a11 #) as non empty strict Language-like ;
take  new ; ::_thesis: ( the adicity of new = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of new = the ZeroF of L & the OneF of new = the OneF of L )
thus  ( the adicity of new = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of new = the ZeroF of L & the OneF of new = the OneF of L ) ; ::_thesis: verum
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
let IT1, IT2 be non empty strict Language-like ; ::_thesis: ( the adicity of IT1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of IT1 = the ZeroF of L & the OneF of IT1 = the OneF of L & the adicity of IT2 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of IT2 = the ZeroF of L & the OneF of IT2 = the OneF of L implies IT1 = IT2 )
set c1 = the carrier of IT1;
set z1 = the ZeroF of IT1;
set o1 = the OneF of IT1;
set a1 = the adicity of IT1;
set c2 = the carrier of IT2;
set z2 = the ZeroF of IT2;
set o2 = the OneF of IT2;
set a2 = the adicity of IT2;
set ITT1 = Language-like(# the carrier of IT1, the ZeroF of IT1, the OneF of IT1, the adicity of IT1 #);
set ITT2 = Language-like(# the carrier of IT2, the ZeroF of IT2, the OneF of IT2, the adicity of IT2 #);
reconsider ITT1 = Language-like(# the carrier of IT1, the ZeroF of IT1, the OneF of IT1, the adicity of IT1 #), ITT2 = Language-like(# the carrier of IT2, the ZeroF of IT2, the OneF of IT2, the adicity of IT2 #) as non empty Language-like ;
defpred S1[ Language-like ] means ( the adicity of $1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of $1 = the ZeroF of L & the OneF of $1 = the OneF of L );
assume A3: ( S1[IT1] & S1[IT2] ) ; ::_thesis: IT1 = IT2
 dom the adicity of IT1 = the carrier of IT2 \ { the OneF of IT1} by A3, FUNCT_2:def_1;
then ( the carrier of IT1 \ { the OneF of IT1}) \/ ({ the OneF of IT1} null the carrier of IT1) = ( the carrier of IT2 \ { the OneF of IT2}) \/ ({ the OneF of IT2} null the carrier of IT2) by A3, FUNCT_2:def_1
.= the carrier of IT2 by FOMODEL0:48 ;
hence  IT1 = IT2 by A3, FOMODEL0:48; ::_thesis: verum
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;
clusterS extendWith f ->  non empty strict S -extending ;
coherence
 S extendWith f is S -extending
proof
set S1 = S;
set S2 = S extendWith f;
set a1 = the adicity of S;
set a2 = the adicity of (S extendWith f);
set o1 = the OneF of S;
A1: ( TheEqSymbOf S = TheEqSymbOf (S extendWith f) & TheNorSymbOf S = TheNorSymbOf (S extendWith f) ) by Def42;
 the adicity of (S extendWith f) = (f | ((dom f) \ { the OneF of S})) +* the adicity of S by Def42;
then  the adicity of S c= the adicity of (S extendWith f) by FUNCT_4:25;
hence  S extendWith f is S -extending by A1, Def41; ::_thesis: verum
end;
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
proof
set S1 = S;
let S2 be Language-like ; ::_thesis: ( S2 is S -extending implies not S2 is degenerated )
assume  S2 is S -extending ; ::_thesis: not S2 is degenerated
then  ( TheEqSymbOf S = TheEqSymbOf S2 & TheNorSymbOf S = TheNorSymbOf S2 ) by Def41;
then  ( 0. S = 0. S2 & 1. S = 1. S2 ) ;
hence  not S2 is degenerated by STRUCT_0:def_8; ::_thesis: verum
end;
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
proof
set S1 = S;
let S2 be Language-like ; ::_thesis: ( S2 is S -extending implies S2 is eligible )
set L1 = LettersOf S;
set L2 = LettersOf S2;
set AS1 = AtomicFormulaSymbolsOf S;
set AS2 = AtomicFormulaSymbolsOf S2;
set a1 = the adicity of S;
set a2 = the adicity of S2;
set E1 = TheEqSymbOf S;
set E2 = TheEqSymbOf S2;
assume A1: S2 is S -extending ; ::_thesis: S2 is eligible
then A2: ( dom the adicity of S = AtomicFormulaSymbolsOf S & dom the adicity of S2 = AtomicFormulaSymbolsOf S2 & TheEqSymbOf S = TheEqSymbOf S2 & the adicity of S c= the adicity of S2 ) by Def41, FUNCT_2:def_1;
reconsider a11 = the adicity of S as Subset of the adicity of S2 by A1, Def41;
 a11 " {0} c= the adicity of S2 " {0} by RELAT_1:144;
then reconsider L11 = LettersOf S as Subset of (LettersOf S2) ;
 (LettersOf S2) null L11 is infinite ;
hence  LettersOf S2 is infinite ; :: according to FOMODEL1:def_23 ::_thesis: the adicity of S2 . (TheEqSymbOf S2) = - 2
 the adicity of S . (TheEqSymbOf S) = - 2 by Def23;
then  TheEqSymbOf S in dom the adicity of S by FUNCT_1:def_2;
then  the adicity of S . (TheEqSymbOf S) = ( the adicity of S2 +* a11) . (TheEqSymbOf S) by FUNCT_4:13
.= the adicity of S2 . (TheEqSymbOf S2) by A2, FUNCT_4:98 ;
hence  the adicity of S2 . (TheEqSymbOf S2) = - 2 by Def23; ::_thesis: verum
end;
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) & the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = the adicity of S1 | (OwnSymbolsOf S1) )
proof
let S1 be non empty Language-like ; ::_thesis: 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) )
let f be INT -valued Function; ::_thesis: ( 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) )
set S2 = S1 extendWith f;
set L1 = LettersOf S1;
set a1 = the adicity of S1;
set a2 = the adicity of (S1 extendWith f);
set z1 = the ZeroF of S1;
set o1 = the OneF of S1;
set X = (dom f) \ { the OneF of S1};
set C1 = the carrier of S1;
set O1 = OwnSymbolsOf S1;
set L2 = LettersOf (S1 extendWith f);
set f1 = f | (((dom f) \ { the OneF of S1}) \ (dom the adicity of S1));
set SS1 = AllSymbolsOf S1;
the carrier of S1 = ( the carrier of S1 \ { the OneF of S1}) \/ ({ the OneF of S1} null the carrier of S1) by FOMODEL0:48
.= (dom the adicity of S1) \/ { the OneF of S1} by FUNCT_2:def_1 ;
then  f | (((dom f) \ { the OneF of S1}) \ (dom the adicity of S1)) = f | ((dom f) \ the carrier of S1) by XBOOLE_1:41;
then A1: (f | ((dom f) \ the carrier of S1)) \/ the adicity of S1 = (f | ((dom f) \ { the OneF of S1})) +* the adicity of S1 by FOMODEL0:57
.= the adicity of (S1 extendWith f) by Def42 ;
hence  LettersOf (S1 extendWith f) = ((f | ((dom f) \ (AllSymbolsOf S1))) " {0}) \/ (LettersOf S1) by FOMODEL0:23; ::_thesis: the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = the adicity of S1 | (OwnSymbolsOf S1)
reconsider Y = (OwnSymbolsOf S1) /\ (dom f) as Subset of the carrier of S1 by XBOOLE_1:1;
thus  the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = ( the adicity of S1 | (OwnSymbolsOf S1)) \/ ((f | ((dom f) \ the carrier of S1)) | (OwnSymbolsOf S1)) by A1, FOMODEL0:56
.= ( the adicity of S1 | (OwnSymbolsOf S1)) \/ (f | ((OwnSymbolsOf S1) /\ ((dom f) \ the carrier of S1))) by RELAT_1:71
.= ( the adicity of S1 | (OwnSymbolsOf S1)) \/ (f | (((OwnSymbolsOf S1) /\ (dom f)) \ the carrier of S1)) by XBOOLE_1:49
.= ( the adicity of S1 | (OwnSymbolsOf S1)) \/ (f | (Y \ the carrier of S1))
.= the adicity of S1 | (OwnSymbolsOf S1) ; ::_thesis: verum
end;

registration
let X be set ;
let m be integer number ;
clusterX --> m ->  INT -valued ;
coherence
 X --> m is INT -valued
proof
reconsider mm = m as Element of INT by INT_1:def_2;
 X --> m is {mm} -valued ;
hence  X --> m is INT -valued ; ::_thesis: verum
end;
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
proof
set L1 = LettersOf S1;
set S2 = S1 addLettersNotIn X;
set no = SymbolsOf X;
set L2 = LettersOf (S1 addLettersNotIn X);
set IT = (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X);
set a1 = the adicity of S1;
set a2 = the adicity of (S1 addLettersNotIn X);
set SS1 = AllSymbolsOf S1;
set fresh = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet ;
reconsider f = (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) --> 0 as INT -valued Function ;
A1: ( 0 in {0} & dom ((((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) --> 0) = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet ) by FUNCT_2:def_1, TARSKI:def_1;
 (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) /\ ((AllSymbolsOf S1) \/ (SymbolsOf X)) = {} ;
then  ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet misses (AllSymbolsOf S1) \/ (SymbolsOf X) by XBOOLE_0:def_7;
then  ( ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet misses (AllSymbolsOf S1) null (SymbolsOf X) & ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet misses (SymbolsOf X) null (AllSymbolsOf S1) ) by XBOOLE_1:63;
then A2: ( (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) \ (AllSymbolsOf S1) = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet & (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) \ (SymbolsOf X) = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet ) by XBOOLE_1:83;
 LettersOf (S1 addLettersNotIn X) = ((f | ((dom f) \ (AllSymbolsOf S1))) " {0}) \/ (LettersOf S1) by Lm12;
then (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X) = ((((f null {}) | ({} \/ (dom f))) " {0}) \ (SymbolsOf X)) \/ ((LettersOf S1) \ (SymbolsOf X)) by A2, A1, XBOOLE_1:42
.= (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) \/ ((LettersOf S1) \ (SymbolsOf X)) by A1, A2, FUNCOP_1:14 ;
hence  not (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X) is finite ; ::_thesis: verum
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
reconsider z = 0 , o = 1 as Element of NAT ;
set D = NAT \ {o};
 ( z in NAT & not z in {o} ) by TARSKI:def_1;
then reconsider zz = z as Element of NAT \ {o} by XBOOLE_0:def_5;
reconsider f = (NAT \ {o}) --> 0, g = zz .--> (- 2) as INT -valued Function ;
set a = f +* g;
A1: ( zz in {zz} & dom g = {zz} & dom f = NAT \ {o} ) by FUNCOP_1:13, TARSKI:def_1;
then  dom (f +* g) = (NAT \ {o}) null {zz} by FUNCT_4:def_1;
then  ( rng (f +* g) c= INT & dom (f +* g) = NAT \ {o} ) ;
then  f +* g is Element of Funcs ((NAT \ {o}),INT) by FUNCT_2:def_2;
then reconsider aa = f +* g as Function of (NAT \ {o}),INT ;
set IT = Language-like(# NAT,z,o,aa #);
A2: 0. Language-like(# NAT,z,o,aa #) <> 1. Language-like(# NAT,z,o,aa #) ;
aa . z = g . zz by A1, FUNCT_4:13
.= - 2 by A1, FUNCOP_1:7 ;
then A3: aa . (TheEqSymbOf Language-like(# NAT,z,o,aa #)) = - 2 ;
now__::_thesis:_for_x_being_set_st_x_in_(NAT_\_{o})_\_{z}_holds_
x_in_aa_"_{0}
let x be set ; ::_thesis: ( x in (NAT \ {o}) \ {z} implies x in aa " {0} )
assume A4: x in (NAT \ {o}) \ {z} ; ::_thesis: x in aa " {0}
then A5: ( x in NAT \ {o} & not x in {zz} ) by XBOOLE_0:def_5;
then  ( x in dom aa & not x in dom g ) by FUNCT_2:def_1;
then aa . x = f . x by FUNCT_4:11
.= 0 by A4, FUNCOP_1:7 ;
then  ( x in dom aa & aa . x in {0} ) by A5, FUNCT_2:def_1, TARSKI:def_1;
hence  x in aa " {0} by FUNCT_1:def_7; ::_thesis: verum
end;
then reconsider E = (NAT \ {o}) \ {z} as Subset of (aa " {0}) by TARSKI:def_3;
 ( E is infinite & (aa " {0}) \/ E = (aa " {0}) null E ) ;
then  LettersOf Language-like(# NAT,z,o,aa #) is infinite ;
then reconsider IT = Language-like(# NAT,z,o,aa #) as Language by A2, A3, Def23, STRUCT_0:def_8;
take  IT ; ::_thesis: IT is countable
thus  IT is countable by ORDERS_4:def_2; ::_thesis: verum
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
set SS = AllSymbolsOf S;
reconsider C = (AllSymbolsOf S) * as countable set by CARD_4:13;
reconsider IT = C \ {{}} as Subset of C ;
 IT is countable ;
hence  ((AllSymbolsOf S) *) \ {{}} is countable ; ::_thesis: verum
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
set L1 = L;
set a1 = the adicity of L;
set SS1 = AllSymbolsOf L;
set L2 = L extendWith f;
set SS2 = AllSymbolsOf (L extendWith f);
set a2 = the adicity of (L extendWith f);
set X = dom f;
set E1 = TheEqSymbOf L;
set N1 = TheNorSymbOf L;
set E2 = TheEqSymbOf (L extendWith f);
set N2 = TheNorSymbOf (L extendWith f);
reconsider Y = (dom f) \ {(TheNorSymbOf L)} as Subset of (dom f) ;
A1: dom (f | ((dom f) \ {(TheNorSymbOf L)})) = (dom f) /\ Y by RELAT_1:61
.= Y ;
 the adicity of (L extendWith f) = (f | ((dom f) \ {(TheNorSymbOf L)})) +* the adicity of L by Def42;
then  dom the adicity of (L extendWith f) = (dom (f | Y)) \/ (dom the adicity of L) by FUNCT_4:def_1;
then A2: (AllSymbolsOf (L extendWith f)) \ {(TheNorSymbOf (L extendWith f))} = Y \/ (dom the adicity of L) by A1, FUNCT_2:def_1
.= Y \/ ((AllSymbolsOf L) \ {(TheNorSymbOf L)}) by FUNCT_2:def_1 ;
reconsider NN1 = {(TheNorSymbOf L)} as non empty Subset of (AllSymbolsOf L) by ZFMISC_1:31;
reconsider NN2 = {(TheNorSymbOf (L extendWith f))} as non empty Subset of (AllSymbolsOf (L extendWith f)) by ZFMISC_1:31;
 ( NN1 c= AllSymbolsOf L & (AllSymbolsOf L) null (dom f) c= (AllSymbolsOf L) \/ (dom f) ) ;
then reconsider NN11 = NN1 as non empty Subset of ((AllSymbolsOf L) \/ (dom f)) by XBOOLE_1:1;
 ( AllSymbolsOf (L extendWith f) = NN2 \/ ((AllSymbolsOf (L extendWith f)) \ NN2) & AllSymbolsOf L = NN1 \/ ((AllSymbolsOf L) \ NN1) ) by XBOOLE_1:45;
then  AllSymbolsOf (L extendWith f) = (NN2 \/ ((AllSymbolsOf L) \ NN1)) \/ Y by A2, XBOOLE_1:4
.= (NN1 \/ ((AllSymbolsOf L) \ NN1)) \/ Y by Def41
.= NN1 \/ (((AllSymbolsOf L) \ NN1) \/ Y) by XBOOLE_1:4
.= NN11 \/ (((AllSymbolsOf L) \/ (dom f)) \ NN11) by XBOOLE_1:42
.= (AllSymbolsOf L) \/ (dom f) by XBOOLE_1:45 ;
hence  for b1 being set st b1 = (AllSymbolsOf (L extendWith f)) \+\ ((dom f) \/ (AllSymbolsOf L)) holds
b1 is empty ; ::_thesis: verum
end;
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
proof
set S1 = S;
set SS1 = AllSymbolsOf S;
set SX = SymbolsOf X;
set add = ((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet ;
set f = (((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0;
set S2 = S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0);
set SS2 = AllSymbolsOf (S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0));
 (AllSymbolsOf (S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0))) \+\ ((dom ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0)) \/ (AllSymbolsOf S)) = {} ;
then  AllSymbolsOf (S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0)) = (dom ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0)) \/ (AllSymbolsOf S) by FOMODEL0:29
.= (((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) \/ (AllSymbolsOf S) by FUNCOP_1:13 ;
then  AllSymbolsOf (S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0)) is countable by CARD_2:85;
hence  for b1 being 1-sorted st b1 = S addLettersNotIn X holds
b1 is countable by ORDERS_4:def_2; ::_thesis: verum
end;
end;