FOMODEL1

:: Definition of first order language with arbitrary alphabet. Syntax of
:: terms, atomic formulas and their subterms
::  by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, INT_1,
      RELAT_1, FINSEQ_1, FUNCT_1, ARYTM_3, XCMPLX_0, CARD_1, MONOID_0,
      ORDINAL1, ARYTM_1, STRUCT_0, XXREAL_0, ORDINAL4, BINOP_1, FINSEQ_2,
      COMPLEX1, PARTFUN1, FINSET_1, SUPINF_2, MESFUNC1, PRE_POLY, SETFAM_1,
      FUNCT_4, FUNCOP_1, FUNCT_2, CARD_3, FOMODEL0, FOMODEL1;
 notations TARSKI, CARD_1, XBOOLE_0, SUBSET_1, NAT_1, ZFMISC_1, ORDINAL1,
      NUMBERS, INT_1, PRE_POLY, FINSEQ_1, XCMPLX_0, RELAT_1, FUNCT_1, FUNCT_2,
      MONOID_0, XXREAL_0, XREAL_0, ALGSTR_0, BINOP_1, FINSEQ_2, ENUMSET1,
      MCART_1, PARTFUN1, INT_2, FINSEQOP, FINSET_1, MATRIX_1, STRUCT_0,
      RELSET_1, SETFAM_1, FUNCT_4, FUNCOP_1, DOMAIN_1, CARD_3, ORDERS_4,
      FOMODEL0;
 constructors TARSKI, NAT_1, CARD_1, ZFMISC_1, NUMBERS, INT_1, ARYTM_3,
      FINSEQ_1, MONOID_0, STRUCT_0, XXREAL_0, BINOP_1, FINSEQ_2, COMPLEX1,
      RELSET_1, INT_2, FINSEQOP, DOMAIN_1, FINSET_1, MATRIX_1, REAL_1,
      PRE_POLY, SETFAM_1, FUNCT_4, FUNCOP_1, RELAT_1, FUNCT_1, FUNCT_2, CARD_3,
      ORDERS_4, WELLORD2, FOMODEL0;
 registrations ORDINAL1, XCMPLX_0, NAT_1, RELAT_1, NUMBERS, FUNCT_1, INT_1,
      FINSEQ_1, STRUCT_0, FINSEQ_2, CARD_1, FINSET_1, PRALG_1, FINSEQ_6,
      FOMODEL0, XBOOLE_0, XXREAL_0, XREAL_0, FUNCT_4, RELSET_1, RAMSEY_1,
      CARD_3;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
 equalities FINSEQ_1, XBOOLE_0, STRUCT_0, FUNCOP_1, FOMODEL0, ORDINAL1;
 expansions XBOOLE_0, STRUCT_0, FOMODEL0;
 theorems TARSKI, XBOOLE_0, INT_1, FUNCT_1, FINSEQ_1, RELAT_1, XBOOLE_1,
      STRUCT_0, ZFMISC_1, FUNCT_2, XXREAL_0, NAT_1, ORDINAL1, FINSEQ_5,
      FUNCT_4, FINSEQ_2, COMPLEX1, FINSEQ_4, RELSET_1, GRFUNC_1, FUNCOP_1,
      CARD_4, ORDERS_4, PARTFUN1, FOMODEL0, CARD_1, ABSVALUE;
 schemes NAT_1, FUNCT_2, DOMAIN_1;

begin

reserve k,m,n for Nat, kk,mm,nn for Element of NAT, X,Y,x,y,z for set;

registration
let z be zero Integer;
cluster |.z.| -> zero for Integer;
coherence by COMPLEX1:47;
end;

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

::##########  First-order structure (theory) formalization  ###########
::######################  basic definitions  ##########################
::#####################################################################
::#####################################################################

definition
struct (ZeroOneStr) Language-like
(#carrier -> set, ZeroF, OneF -> Element of the carrier,
adicity->Function of the carrier\{the OneF}, INT#);
end;

definition
let S be Language-like;
func AllSymbolsOf S -> set equals the carrier of S;
coherence;
func LettersOf S -> set equals (the adicity of S) " {0};
coherence;
func OpSymbolsOf S -> set equals (the adicity of S) " (NAT \ {0});
coherence;
func RelSymbolsOf S -> set equals (the adicity of S) " (INT \ NAT);
coherence;
func TermSymbolsOf S -> set equals (the adicity of S) " NAT;
coherence;
func LowerCompoundersOf S -> set equals (the adicity of S) " (INT \ {0});
coherence;
func TheEqSymbOf S -> set equals the ZeroF of S;
coherence;
func TheNorSymbOf S -> set equals the OneF of S;
coherence;
func OwnSymbolsOf S -> set equals
(the carrier of S)\{the ZeroF of S,the OneF of S};
coherence;
end;

definition
let S be Language-like;
mode Element of S is Element of (AllSymbolsOf S);
func AtomicFormulaSymbolsOf S -> set equals
(AllSymbolsOf S) \ {TheNorSymbOf S};
coherence;
func AtomicTermsOf S -> set equals
1-tuples_on (LettersOf S);
coherence;
attr S is operational means (OpSymbolsOf S) is non empty;
attr S is relational means
(RelSymbolsOf S) \ {TheEqSymbOf S} is non empty;
end;

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

definition
let S be ZeroOneStr;
let s be Element of (the carrier of S)\{the OneF of S};
func TrivialArity(s) -> Integer equals :Def21:
-2 if s=the ZeroF of S otherwise 0;
coherence;
consistency;
end;

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

definition
let S be non degenerated ZeroOneStr;
func S TrivialArity->Function of (the carrier of S)\{the OneF of S},INT means
:Def22: for s being Element of (the carrier of S)\{the OneF of S}
holds it.s=TrivialArity(s);
existence
proof
set D=(the carrier of S)\{the OneF of S};
deffunc F(Element of D) = TrivialArity($1);
consider f being Function of D,INT such that A1:
for x being Element of D holds f.x=F(x) from FUNCT_2:sch 4; take f;
thus thesis by A1;
end;
uniqueness
proof
set D=(the carrier of S)\{the OneF of S}; let IT1,IT2 be Function of D,INT;
A2: dom IT1=D & dom IT2=D by FUNCT_2:def 1;
assume A3: for s being Element of D holds IT1.s=TrivialArity(s);
assume A4: for s being Element of D holds IT2.s=TrivialArity(s);
now
let x be object; assume x in dom IT1; then reconsider s=x as Element of D;
IT1.s = TrivialArity(s) by A3 .= IT2.s by A4; hence IT1.x=IT2.x;
end;
hence thesis by A2, FUNCT_1:2;
end;
end;

registration
cluster infinite for non degenerated ZeroOneStr;
existence
proof
set X = the infinite set, Z = the Element of X, O = the Element of X\{Z};
reconsider Y=X\{Z} as infinite set;
not O in {Z} by XBOOLE_0:def 5; then A1: O<>Z by TARSKI:def 1;
reconsider OO=O as Element of X;
set S=ZeroOneStr(# X, Z, OO #); 1.S=OO & 0.S=Z;
then reconsider SS=S as non degenerated ZeroOneStr by A1, STRUCT_0:def 8;
take SS;
thus thesis;
end;
end;

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

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

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

Lm2: ex S being Language-like st S is non degenerated & S is eligible
proof
set SS = the infinite non degenerated ZeroOneStr;
A1: 0.SS<>1.SS; set f=SS TrivialArity; take S=
Language-like (# the carrier of SS, the ZeroF of SS, the OneF of SS, f#);
0.S<>1.S by A1; hence S is non degenerated;
set g=(the adicity of S); thus LettersOf S is infinite;
thus thesis by Lm1;
end;

registration
cluster non degenerated for Language-like;
existence by Lm2;
end;

registration
cluster eligible for non degenerated Language-like;
existence by Lm2;
end;

definition
mode Language is eligible non degenerated Language-like;
end;

reserve S,S1,S2 for Language, s,s1,s2 for Element of S;

definition
let S be non empty Language-like;
redefine func AllSymbolsOf S -> non empty set;  :: redefines AllSymbolsOf (FOMODEL1, definition)
coherence;
end;

registration
let S be eligible Language-like;
cluster LettersOf S -> infinite for set;
coherence by Def23;
end;

definition
let S be Language;
redefine func LettersOf S -> non empty Subset of (AllSymbolsOf S);  :: redefines LettersOf (FOMODEL1, definition)
coherence 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;
set EQ=TheEqSymbOf S, NOR=TheNorSymbOf S, SS=AllSymbolsOf S;
1.S <> 0.S & EQ=0.S & NOR=1.S;
then EQ in SS & not EQ in {NOR} by TARSKI:def 1; hence thesis by
XBOOLE_0:def 5;
end;

registration
let S be Language;
cluster TheEqSymbOf S -> relational for Element of S;
coherence
proof
set E=TheEqSymbOf S, R=RelSymbolsOf S,
a=the adicity of S, 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;
E in D & dom a= D by FUNCT_2:def 1, Lm3; then
E in dom a & a.E in (INT\NAT) by A1, Def23;
then E in R by FUNCT_1:def 7; hence thesis;
end;
end;

definition
let S be non degenerated Language-like;
redefine func AtomicFormulaSymbolsOf S  :: redefines AtomicFormulaSymbolsOf (FOMODEL1, definition)
-> non empty Subset of (AllSymbolsOf S);
coherence;
end;

definition
let S;
redefine func TheEqSymbOf S -> Element of S;  :: redefines TheEqSymbOf (FOMODEL1, definition)
coherence;
end;

theorem Th1: 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;
set o=the OneF of S, z=the ZeroF of S, f=the adicity of S, R=RelSymbolsOf S,
O=OwnSymbolsOf S, SS=AllSymbolsOf S, e=TheEqSymbOf S, n=TheNorSymbOf S,
A=AtomicFormulaSymbolsOf S, D = (the carrier of S) \ {o},
L=LowerCompoundersOf S, T=TermSymbolsOf S, OP=OpSymbolsOf S,
B=LettersOf S;
thus B/\OP=f"({0}/\(NAT\{0}))
by FUNCT_1:68 .= f"({}) by XBOOLE_1:79, XBOOLE_0:def 7 .= {};
thus T/\L = f"(NAT /\ (INT \{0})) by FUNCT_1:68
.= f"((NAT/\INT)\{0}) by XBOOLE_1:49 .= OP by XBOOLE_1:28, XBOOLE_1:7;
A1: TheEqSymbOf S in R by Def17;
O =
D \ {z} by XBOOLE_1:41; then
R\O = (R\D) \/ (R /\ {z}) by XBOOLE_1:52 .=
{} \/ R /\ {z} .= {z} by ZFMISC_1:46, A1; hence R\O={TheEqSymbOf S}; thus
OwnSymbolsOf S c= AtomicFormulaSymbolsOf S by XBOOLE_1:34, ZFMISC_1:7;
f"{0} c= f"NAT & RelSymbolsOf S = f"INT \ (f"NAT) &
LowerCompoundersOf S = f"INT \ (f"{0}) by FUNCT_1:69, RELAT_1:143;
hence RelSymbolsOf S c= LowerCompoundersOf S by XBOOLE_1:34;
OpSymbolsOf S = f"NAT \ (f"{0}) by FUNCT_1:69;
hence OpSymbolsOf S c= TermSymbolsOf S;
thus LettersOf S c= TermSymbolsOf S by RELAT_1:143;
-2 = f.(TheEqSymbOf S) by Def23 .= f.z;
then not f.z in NAT; then not z in f"NAT by FUNCT_1:def 7; then
f"NAT misses {z} & f"NAT c= (( the carrier of S) \ {o}) by ZFMISC_1:50;
then f"NAT c= ((the carrier of S) \{o})\{z} by XBOOLE_1:86;
hence TermSymbolsOf S c= OwnSymbolsOf S by XBOOLE_1:41;
for x being object st x in NAT holds x in INT by INT_1:def 2;
then NAT \{0} c= INT\{0} by XBOOLE_1:33, TARSKI:def 3;
hence OpSymbolsOf S c= LowerCompoundersOf S by RELAT_1:143;
thus thesis;
end;

registration
let S be Language;
cluster TermSymbolsOf S -> non empty for set;
coherence proof LettersOf S c= TermSymbolsOf S by Th1; hence thesis; end;
cluster own -> ofAtomicFormula for Element of S;
coherence
proof
let s be Element of S; assume s is own; then s in OwnSymbolsOf S &
OwnSymbolsOf S c= AtomicFormulaSymbolsOf S by Th1;
hence thesis;
end;
cluster relational -> low-compounding for Element of S;
coherence
proof
let s be Element of S; assume s is relational;
then s in RelSymbolsOf S & RelSymbolsOf S c= LowerCompoundersOf S by Th1;
hence s is low-compounding;
end;
cluster operational -> termal for Element of S;
coherence
proof
let s be Element of S; assume s is operational; then
s in OpSymbolsOf S & OpSymbolsOf S c= TermSymbolsOf S by Th1;
hence thesis;
end;
cluster literal -> termal for Element of S;
coherence
proof
let s be Element of S; assume s is literal; then
LettersOf S c= TermSymbolsOf S & s in LettersOf S by Th1;
hence thesis;
end;
cluster termal -> own for Element of S;
coherence
proof
let s be Element of S; assume s is termal; then
TermSymbolsOf S c= OwnSymbolsOf S & s in TermSymbolsOf S by Th1;
hence thesis;
end;
cluster operational -> low-compounding for Element of S;
coherence
proof
let s be Element of S; assume s is operational; then
s in OpSymbolsOf S & OpSymbolsOf S c= LowerCompoundersOf S by Th1;
hence thesis;
end;
cluster low-compounding -> ofAtomicFormula for Element of S;
coherence;
cluster termal -> non relational for Element of S;
coherence
proof
set T=TermSymbolsOf S, R=RelSymbolsOf S,f=the adicity of S;
T/\R= f"(NAT/\(INT\NAT)) by FUNCT_1:68 .=
f"(NAT/\INT \ (NAT/\NAT)) .= {}; then
A1: T\R=T by XBOOLE_1:83, XBOOLE_0:def 7;
let s be Element of S; assume s is termal;
then s in T\R by A1; then not s in R by XBOOLE_0:def 5;
hence thesis;
end;
cluster literal -> non relational for Element of S;
coherence;
cluster literal -> non operational for Element of S;
coherence
proof
set L=LettersOf S, P=OpSymbolsOf S; let s be Element of S; assume
A2: s is literal; assume s is operational; then s in L & s in P by A2;
then s in L/\P by XBOOLE_0:def 4; hence contradiction by Th1;
end;
end;

registration
let S be Language;
cluster relational for Element of S;
existence proof take s=TheEqSymbOf S; thus thesis; end;
cluster literal for Element of S;
existence
proof
set s = the Element of LettersOf S; take s; thus thesis;
end;
end;

registration
let S be Language;
cluster termal -> operational for low-compounding Element of S;
coherence
proof
set L=LowerCompoundersOf S, T=TermSymbolsOf S, OP=OpSymbolsOf S;
let s be low-compounding Element of S; A1: s in L by Def15;
assume s is termal; then s in T; then
s in L /\ T by XBOOLE_0:def 4, A1; then s in OP by Th1;
hence thesis;
end;
end;

registration
let S be Language;
cluster ofAtomicFormula for Element of S; existence
proof
set s = the literal Element of S; take s; thus thesis;
end;
end;

definition
let S be Language;
let s be ofAtomicFormula Element of S;
func ar(s) -> Element of INT equals (the adicity of S).s;
coherence
proof
set f=(the adicity of S);
reconsider g=f as Function of AtomicFormulaSymbolsOf S, INT;
reconsider ss=s as Element of AtomicFormulaSymbolsOf S by Def20;
g.ss in INT; hence thesis;
end;
end;

registration
let S be Language; let s be literal Element of S;
cluster ar(s) -> zero for number;
coherence
proof
set f=the adicity of S; s in LettersOf S by Def14;
then f.s in {0} by FUNCT_1:def 7;
hence thesis;
end;
end;

definition
let S be Language;
func S-cons -> BinOp of (AllSymbolsOf S)*
equals (AllSymbolsOf S)-concatenation;
coherence;
end;

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

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

definition
let S be Language;
let X be set;
attr X is S-prefix means :Def28: X is (AllSymbolsOf S)-prefix;
end;

registration
let S be Language;
cluster S-prefix -> (AllSymbolsOf S)-prefix for set;
coherence;
cluster (AllSymbolsOf S)-prefix -> S-prefix for set;
coherence;
end;

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

registration
let S;
cluster (AllSymbolsOf S)*\{{}} -> non empty for set;
coherence;
end;

registration
let S;
cluster -> non empty for string of S;
coherence;
end;

registration
cluster -> infinite for Language;
coherence
proof
let S be Language; set SS=AllSymbolsOf S, L=LettersOf S;
reconsider S0=S as 1-sorted;
L \/ SS = SS by XBOOLE_1:12;
hence thesis;
end;
end;

registration
let S be Language; cluster AllSymbolsOf S -> infinite for set; coherence;
end;

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

definition
let S be Language;
let s be ofAtomicFormula Element of S;
let Strings be set;
redefine func Compound(s,Strings) -> Element of bool ((AllSymbolsOf S)*\{{}});  :: redefines Compound (FOMODEL1, definition)
coherence
proof
set Y=Compound(s,Strings), SS=AllSymbolsOf S;
reconsider ss=s as Element of SS;
now
let x be object; assume x in Y;
then consider StringTuple being Element of SS** such that A1:
x=<*s*>^(S-multiCat.StringTuple) & rng StringTuple c= Strings &
StringTuple is (|.ar s.|)-element;
reconsider head=<*ss*> as non empty FinSequence of SS;
reconsider tail=(S-multiCat.StringTuple) as FinSequence of SS
by FINSEQ_1:def 11;
head ^ tail is non empty FinSequence of SS & x=head ^ tail by A1;
hence x in SS*\{{}} by FOMODEL0:5;
end;
hence thesis by TARSKI:def 3;
end;
end;

definition
let S be Language;
func S-termsOfMaxDepth -> Function means :Def30: 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
proof
deffunc F(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)=F(n,f.n) from NAT_1:sch 11;
hence thesis;
end;
uniqueness
proof
deffunc F(set,set)=(union {Compound(s,$2) where s is ofAtomicFormula
Element of S: s is operational}) \/ $2;
let IT1,IT2 be Function;
assume A1: dom IT1=NAT & IT1.0=(AtomicTermsOf S) &
for n being Nat holds IT1.(n+1)=F(n,IT1.n);
A2: dom IT1=NAT by A1; A3: IT1.0=(AtomicTermsOf S) by A1;
A4: for n being Nat holds IT1.(n+1)=F(n,IT1.n) by A1;
assume A5: dom IT2=NAT & IT2.0=(AtomicTermsOf S) &
for n being Nat holds IT2.(n+1)=F(n,IT2.n);
A6: dom IT2=NAT by A5; A7: IT2.0=(AtomicTermsOf S) by A5;
A8: for n being Nat holds IT2.(n+1)=F(n,IT2.n) by A5;
thus IT1=IT2 from NAT_1:sch 15(A2,A3,A4,A6,A7,A8);
end;
end;

definition
let S;
redefine func AtomicTermsOf S -> Subset of (AllSymbolsOf S)*;  :: redefines AtomicTermsOf (FOMODEL1, definition)
coherence
proof
set SS=AllSymbolsOf S, A=AtomicTermsOf S;
reconsider L=LettersOf S as Subset of SS;
A c= L* by FINSEQ_2:134;
hence thesis by XBOOLE_1:1;
end;
end;

Lm4: S-termsOfMaxDepth.m c= (AllSymbolsOf S)*\{{}}
proof
set T=S-termsOfMaxDepth, SS=AllSymbolsOf S, L=LettersOf S;
defpred P[Nat] means T.$1 c= SS*\{{}};
A1: P[0]
proof
T.0=AtomicTermsOf S by Def30
.= (0+1)-tuples_on L; then A2: T.0 c= L*\{{}} by FOMODEL0:9;
 L*\{{}} c= SS*\{{}} by XBOOLE_1:33;
hence thesis by A2, XBOOLE_1:1;
end;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume A4: P[n];
set TM1 =
{Compound(s,T.n) where s is ofAtomicFormula Element of S:s is operational};
now
let X be set; assume X in TM1; then
consider s being ofAtomicFormula Element of S such that A5:
X=Compound(s,T.n) & s is operational; thus X c= SS*\{{}} by A5;
end;
then union TM1 c= SS*\{{}} & T.(n+1)= union TM1 \/ T.n
by Def30, ZFMISC_1:76; hence thesis by A4, XBOOLE_1:8;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A3); hence thesis;
end;

Lm5: S-termsOfMaxDepth.m c= S-termsOfMaxDepth.(m+n)
proof
set T=S-termsOfMaxDepth;
defpred P[Nat] means T.(m) c= T.(m+$1);
A1: P[0];
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
A3: P[n];
T.(m+n+1)=T.(m+n) \/
(union {Compound(s,T.(m+n)) where s is ofAtomicFormula Element of S:
s is operational}) by Def30; then T.(m+n) c= T.(m+n+1) by XBOOLE_1:7;
hence thesis by A3, XBOOLE_1:1;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1, A2);
hence thesis;
end;

definition
let S be Language;
func AllTermsOf S -> set equals union rng (S-termsOfMaxDepth);
coherence;
end;

theorem Th2: S-termsOfMaxDepth.mm c= AllTermsOf S
proof
set T=S-termsOfMaxDepth; dom T=NAT by Def30;
hence thesis by ZFMISC_1:74, FUNCT_1:3;
end;

Lm6: x in AllTermsOf S implies ex nn st x in S-termsOfMaxDepth.nn
proof
set T=S-termsOfMaxDepth;
assume x in AllTermsOf S; then consider Y being set such that A1:
x in Y & Y in rng T by TARSKI:def 4;
consider mmm being object such that
A2: mmm in dom T & Y=T.mmm by A1, FUNCT_1:def 3;
reconsider mm=mmm as Element of NAT by A2, Def30;
take nn=mm; thus thesis by A1,A2;
end;

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

definition
let m be Nat;
let S be Language;
let w be string of S;
attr w is m-termal means :Def33: w in S-termsOfMaxDepth.m;
end;

registration
let m be Nat;
let S be Language;
cluster m-termal -> termal for string of S;
coherence
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
let w be string of S; assume w is m-termal; then w in S-termsOfMaxDepth.m
& S-termsOfMaxDepth.mm c= AllTermsOf S by Th2;
hence thesis;
end;
end;

definition
let S;
redefine func S-termsOfMaxDepth -> sequence of bool((AllSymbolsOf S)*);  :: redefines -termsOfMaxDepth (FOMODEL1, definition)
coherence
proof
set SS=AllSymbolsOf S, T=S-termsOfMaxDepth;
A1: dom T=NAT by Def30;
now
let y be object;
 reconsider yy=y as set by TARSKI:1;
assume y in rng T; then consider x being object such that A2:
x in dom T & y=T.x by FUNCT_1:def 3;
reconsider m=x as Element of NAT by Def30, A2; y=T.m by A2; then
yy c= SS*\{{}} & SS*\{{}} c= SS* by Lm4;
then yy c= SS* by XBOOLE_1:1; hence y in bool (SS*);
end;
then rng T c= bool (SS*) by TARSKI:def 3;
hence thesis by A1, RELSET_1:4, FUNCT_2:67;
end;
end;

definition
let S;
redefine func AllTermsOf S -> non empty Subset of (AllSymbolsOf S)*;  :: redefines AllTermsOf (FOMODEL1, definition)
coherence
proof
set A=AllTermsOf S, T=S-termsOfMaxDepth, SS=AllSymbolsOf S;
A1: now
let x be object; assume x in A; then consider mm being Element of NAT
such that A2: x in T.mm by Lm6;
thus x in SS* by A2;
end;
A=T.0 \/ A by Th2, XBOOLE_1:12 .= (AtomicTermsOf S) \/ A by Def30;
hence thesis by A1, TARSKI:def 3;
end;
end;

registration
let S;
cluster AllTermsOf S -> non empty for set;
coherence;
end;

registration
let S,m;
cluster S-termsOfMaxDepth.m -> non empty;
coherence
proof
set T=S-termsOfMaxDepth, Z=AtomicTermsOf S, SS=AllSymbolsOf S,
x = the Element of Z; x in Z & Z=T.0 by Def30; then x in T.0 &
T.0 c= T.(0+m) by Lm5; hence T.m is non empty;
end;
end;

registration
let S,m;
cluster -> non empty for Element of S-termsOfMaxDepth.m;
coherence
proof
set T=S-termsOfMaxDepth, SS=AllSymbolsOf S, A=AtomicTermsOf S;
let w be Element of T.m;
w in SS*\{{}} by Lm4, TARSKI:def 3;
hence thesis;
end;
end;

registration
let S;
cluster -> non empty for Element of AllTermsOf S;
coherence
proof
set T=S-termsOfMaxDepth, SS=AllSymbolsOf S,
A=AtomicTermsOf S, AA=AllTermsOf S; let t be Element of AA;
consider mm such that A1: t in T.mm by Lm6; reconsider
tt=t as Element of T.mm by A1; tt is non empty; hence thesis;
end;
end;

registration
let m be Nat, S be Language;
cluster m-termal for string of S;
existence
proof
set T=S-termsOfMaxDepth, SS=AllSymbolsOf S, A=AtomicTermsOf S,
w = the Element of A;
A1: w in A; then w in T.0 & T.0 c= SS*\{{}} by Lm4, Def30;
then reconsider ww=w as string of S; take ww; ww in T.0 & T.0 c= T.(0+m)
by Lm5, A1, Def30; hence thesis;
end;
end;

registration
let S;
cluster 0-termal -> 1-element for string of S;
coherence
proof
set A=AtomicTermsOf S, L=LettersOf S, T=S-termsOfMaxDepth;
let w be string of S; assume w is 0-termal; then w in T.0;
then w in A by Def30;
then reconsider ww=w as Element of 1-tuples_on L;
ww is 1-element; hence thesis;
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
proof
set A=AllTermsOf S, T=S-termsOfMaxDepth, Z=AtomicTermsOf S,
SS=AllSymbolsOf S, s=S-firstChar.w, ss=SS-firstChar.w, L=LettersOf S;
reconsider ww=w as non empty FinSequence of SS by FOMODEL0:5;
A1: ss=ww.1 by FOMODEL0:6;
w in T.0 by Def33; then w in Z by Def30;
then consider x such that A2: x in L & w=<*x*> by FINSEQ_2:135;
ss in L by A2,A1;
hence thesis;
end;
end;

Lm7: for w being (mm+1)-termal string of S st w is not mm-termal holds ex
s being termal Element of S, T being Element of ((S-termsOfMaxDepth).mm)*
st T is (|.ar s.|)-element & w=<*s*>^((S-multiCat).T)
proof
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; assume w is not mm-termal; then
w in (S-termsOfMaxDepth).(mm+1) & not w in (S-termsOfMaxDepth).mm
by Def33; then w in (union fam)\/(S-termsOfMaxDepth).mm & not w in
(S-termsOfMaxDepth).mm by Def30; then w in union fam by XBOOLE_0:def 3;
then consider C being set such that A1: w in C & C in fam  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;
consider StringTuple being Element of
(AllSymbolsOf S)**
such that A3:
w=<*s*>^((S-multiCat).StringTuple) & rng StringTuple c=
(S-termsOfMaxDepth).mm & StringTuple is (|.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)*;
take T=TTT; thus T is (|.ar s.|)-element by A3;
thus thesis by A3;
end;

Lm8: for w being (mm+1)-termal string of S ex s being
termal Element of S, T being Element of ((S-termsOfMaxDepth).mm)*
st T is (|.ar s.|)-element & w=<*s*>^((S-multiCat).T)
proof
set TS=TermSymbolsOf S, T=S-termsOfMaxDepth, C=S-multiCat,
L=LettersOf S;
defpred P[Element of omega] means
for w being ($1+1)-termal string of S ex s being termal Element of S,
T being Element of ((S-termsOfMaxDepth).$1)* st T is
(|.ar s.|)-element & w=<*s*>^((S-multiCat).T);
defpred Q[Nat] means ex mm being Element of NAT st mm=$1 & P[mm];
A1: Q[0]
proof
take 0; thus 0=0;
thus P[0]
proof
let w be (0+1)-termal string of S;
per cases;
suppose w is 0-termal; then w in S-termsOfMaxDepth.0; then
w in AtomicTermsOf S by Def30; then
w in the set of all <*ss*> where ss is Element of (LettersOf S)
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
reconsider TTT=TT as FinSequence of S-termsOfMaxDepth.0
by XBOOLE_1:2, FINSEQ_1:def 4;
reconsider TTTT=TTT as Element of (S-termsOfMaxDepth.0)*;
take s=sss; take T=TTTT;
thus T is (|.ar s.|)-element;
reconsider s=sss as Element of TS by Def18;
S-multiCat.{}={} & <*sss*>^{} = <*sss*>;
hence thesis by A2;
end;
suppose w is non 0-termal; hence thesis by Lm7;end;
end;
end;
A3: for m being Nat st Q[m] holds Q[m+1]
proof
let m be Nat; reconsider mm=m, mmm=m+1 as Element of NAT by ORDINAL1:def 12;
assume
A4: Q[m]; take mmm; thus mmm=m+1;
let w be (mmm+1)-termal (string of S);
per cases;
suppose w is not mmm-termal; hence thesis by Lm7; end;
suppose w is mmm-termal; then
consider s being termal Element of S,
T being Element of ((S-termsOfMaxDepth).mm)* such that
A5: T is (|.ar s.|)-element & w=<*s*>^((S-multiCat).T) by A4;
set high=(S-termsOfMaxDepth.mmm);
reconsider low=(S-termsOfMaxDepth.mm) as Subset of high by Lm5;
T in low* & low* is Subset of high*; then
reconsider TT=T as Element of high*;
take s,TT; thus thesis by A5;
end;
end;
A6: for m being Nat holds Q[m] from NAT_1:sch 2(A1, A3);
now
let mm be Element of NAT;
reconsider m=mm as Nat;
consider nn being Element of NAT such that
A7: nn=m & P[nn] by A6; thus P[mm] by A7;
end;
hence thesis;
end;

registration
let S;
let w be termal (string of S);
cluster S-firstChar.w -> termal for Element of S;
coherence
proof
set A=AllTermsOf S, T=S-termsOfMaxDepth, Z=AtomicTermsOf S,
SS=AllSymbolsOf S, s=S-firstChar.w, ss=SS-firstChar.w, L=LettersOf S;
w in A by Def32; then consider mm such that A1: w in T.mm by Lm6;
reconsider ww=w as non empty FinSequence of SS by FOMODEL0:5;
A2: ss=ww.1 by FOMODEL0:6;
per cases;
suppose mm=0; then
reconsider www=w as 0-termal string of S by Def33, A1;
S-firstChar.www is literal; hence thesis;
end;
suppose mm<>0; 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 (T.nn)* such that
A4: T1 is (|.ar s1.|)-element & www=<*s1*>^((S-multiCat).T1) by Lm8;
thus thesis by FINSEQ_1:41, A4, A2;
end;
end;
end;

definition
let S; let t be termal string of S;
func ar(t) -> Element of INT equals ar(S-firstChar.t);
coherence;
end;

theorem Th3: for w being (mm+1)-termal string of S ex T being Element of
((S-termsOfMaxDepth).mm)* st T is |.(ar(S-firstChar.w)).|-element
& w=<*S-firstChar.w*>^((S-multiCat).T)
proof
let w be (mm+1)-termal string of S; consider s being termal Element of S,
T being Element of ((S-termsOfMaxDepth).mm)* such that A1:
T is (|.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 thesis by A1;
end;

Lm9: S-termsOfMaxDepth.m is S-prefix
proof
set T=S-termsOfMaxDepth, SS=AllSymbolsOf S, L=LettersOf S, S1=1-tuples_on SS,
f=S-cons, F=S-multiCat, ff=SS-concatenation, FF=SS-multiCat;
A1: dom FF=SS** by FUNCT_2:def 1;
reconsider LS=L as non empty Subset of SS;
set L1=1-tuples_on LS;
defpred P[Nat] means T.$1 is S-prefix;
A2: P[0]
proof
L1 /\ S1 = 1-tuples_on (LS /\ SS) by FOMODEL0:3
.= 1-tuples_on LS by XBOOLE_1:28;
then reconsider L11=1-tuples_on LS as Subset of S1;
T.0 = (AtomicTermsOf S) by Def30 .= L11; hence thesis;
end;
A3: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume
A4: P[m];
reconsider mm=m, mm1=m+1 as Element of NAT by ORDINAL1:def 12;
now
let t1,t2,w1,w2 be set; assume
A5: t1 in (T.(m+1))/\(SS*) &
t2 in T.(m+1)/\ (SS*) & w1 in SS* & w2 in SS*;
t1 in T.mm1 & not t1 in {{}} & t2 in T.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 SS by FINSEQ_1:def 11;
consider T1 being Element of (T.mm)* such that A6: T1 is
|.ar(S-firstChar.t11).|-element & t11=<*S-firstChar.t11*>^(F.T1) by Th3;
consider T2 being Element of (T.mm)* such that A7: T2 is
|.ar(S-firstChar.t22).|-element & t22=<*S-firstChar.t22*>^(F.T2) by Th3;
reconsider T11=T1, T22=T2 as FinSequence of T.mm by FINSEQ_1:def 11;
reconsider w11=w1, w22=w2 as Element of SS* by A5;
reconsider head1=F.T1, head2=F.T2, tail1=w11, tail2=w22 as
FinSequence of SS by FINSEQ_1:def 11;
assume f.(t1,w1)=f.(t2,w2);
then t111^w11=f.(t222,w22) by FOMODEL0:4; then
(<*S-firstChar.t11*>^(F.T1))^w11=t222^w22 by FOMODEL0:4, A6; then
<*S-firstChar.t11*>^((F.T1)^w11)=(<*S-firstChar.t22*>^(F.T2))^w22
by A7, FINSEQ_1:32; then
<*S-firstChar.t11*>^(head1^tail1)=<*S-firstChar.t22*>^(head2^tail2)
by FINSEQ_1:32; then
A8: f.(<*S-firstChar.t11*>,head1^tail1)=<*S-firstChar.t22*>^(head2^tail2)
by FOMODEL0:4;
1-tuples_on SS c= 1-tuples_on SS;then reconsider
S1=1-tuples_on SS as Subset of 1-tuples_on SS;
A9: S1 is f-unambiguous by FOMODEL0:def 3;
 S1 /\ (SS*) = S1 by FINSEQ_2:134, XBOOLE_1:28;
then
<*S-firstChar.t11*> in S1 /\ (SS*) & <*S-firstChar.t22*> in S1 /\ (SS*) &
head1^tail1 in SS* & head2^tail2 in SS* &
f.(<*S-firstChar.t11*>, head1^tail1) =
f.(<*S-firstChar.t22*>,head2^tail2) by A8, FOMODEL0:4,FINSEQ_2:98; then
A10: <*S-firstChar.t11*>=<*S-firstChar.t22*> & head1^tail1=head2^tail2 &
head1^tail1=ff.(head1, tail1) by A9, FOMODEL0:4;
A11: S-firstChar.t11=S-firstChar.t22 by FINSEQ_1:76, A10;
set n=|.ar(S-firstChar.t11).|;
len T11=n & len T22=n by A6, CARD_1:def 7,A11,A7; then
T11 in n-tuples_on (T.m) & T22 in n-tuples_on (T.m) &
T11 in dom FF & T22 in dom FF by FINSEQ_2:133, A1;
then FF.T11 in FF.:(n-tuples_on (T.m)) & FF.T22 in FF.:(n-tuples_on (T.m))
& FF.T1 in SS* & FF.T2 in SS* by FUNCT_1:def 6; then
A12: FF.T1 in (FF.:(n-tuples_on (T.m))) /\ (SS*) &
FF.T2 in (FF.:(n-tuples_on (T.m))) /\ (SS*) & w11 in SS* & w22 in SS*
& ff.(FF.T1, w11)=ff.(FF.T2, w22) by FOMODEL0:4, A10, XBOOLE_0:def 4;
T.m is SS-prefix & (T.m is SS-prefix implies
(SS-multiCat).:(n-tuples_on (T.m)) is SS-prefix) by A4, Def28;
then (SS-multiCat).:(n-tuples_on (T.m)) is ff-unambiguous;
hence t1=t2 & w1=w2 by A6, A7, A10, A12;
end; then
T.(m+1) is SS-prefix by FOMODEL0:def 10; hence thesis;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A2, A3); hence thesis;
end;

registration
let S,m;
cluster S-termsOfMaxDepth.m -> S-prefix for set;
coherence by Lm9;
end;

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

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

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

registration
let S;
cluster 0wff for string of S;
existence
proof
set SS=AllSymbolsOf S, s = the relational Element of S, V =
the |.ar s.|-element Element of (AllTermsOf S)*; reconsider
ss=s as Element of SS; reconsider tail=S-multiCat.V as FinSequence of SS
by FINSEQ_1:def 11; reconsider IT=<*ss*>^tail as Element of SS*\{{}}
by FOMODEL0:5; take IT; thus thesis;
end;
end;

registration
let S; let phi be 0wff string of S;
cluster S-firstChar.phi -> relational for Element of S;
coherence
proof
set SS=AllSymbolsOf S, A=AllTermsOf S, C=S-multiCat, F=S-firstChar;
consider s be relational Element of S,
V being |.ar s.|-element Element of A* such that A1:
phi=<*s*>^(C.V) by Def35;
reconsider ss=s as Element of SS;
reconsider head=<*ss*> as FinSequence of SS;
reconsider tail=C.V as FinSequence of SS by FINSEQ_1:def 11; F.phi =
(head^tail).1 by A1, FOMODEL0:6 .= s by FINSEQ_1:41; hence thesis;
end;
end;

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

definition
let S;
redefine func AtomicFormulasOf S -> Subset of (AllSymbolsOf S)*\{{}};  :: redefines AtomicFormulasOf (FOMODEL1, definition)
coherence
proof
set SS=AllSymbolsOf S, AF=AtomicFormulasOf S;
defpred P[Element of SS*\{{}}] means $1 is 0wff;
{phi where phi is Element of SS*\{{}}: P[phi]} is Subset of SS*\{{}} from
DOMAIN_1:sch 7; hence thesis;
end;
end;

registration
let S;
cluster AtomicFormulasOf S -> non empty for set;
coherence
proof
set AF=AtomicFormulasOf S, phi = the 0wff string of S;
phi in AF; hence thesis;
end;
end;

registration
let S;
cluster -> 0wff for Element of AtomicFormulasOf S;
coherence
proof
set AF=AtomicFormulasOf S;
let phi be Element of AF; phi in AF; then consider x being string of S
such that A1: phi=x & x is 0wff; thus thesis by A1;
end;
end;

Lm10: AllTermsOf S is S-prefix
proof
set SS=AllSymbolsOf S, f=SS-concatenation, F=SS-multiCat, TT=AllTermsOf S,
T=S-termsOfMaxDepth;
now
let t1,t2,w1,w2 be set; assume
A1: t1 in TT/\(SS*) & t2 in TT/\(SS*) &
w1 in SS* & w2 in SS* & f.(t1,w1)=f.(t2,w2);
consider mm being Element of NAT such that A2: t1 in T.mm by Lm6, A1;
consider nn being Element of NAT such that A3: t2 in T.nn by Lm6, A1;
set p=mm+nn;
A4: T.p is f-unambiguous by FOMODEL0:def 3;
T.mm c= T.p & T.nn c= T.p by Lm5;
then t1 in T.p /\ (SS*) & t2 in T.p /\ (SS*) &
w1 in SS* & w2 in SS* & f.(t1,w1)=f.(t2,w2) by A1,XBOOLE_0:def 4, A2, A3;
hence t1=t2 & w1=w2 by A4;
end;
then TT is SS-prefix by FOMODEL0:def 10;
hence thesis;
end;

registration
let S;
cluster AllTermsOf S -> S-prefix for set;
coherence by Lm10;
end;

definition
let S; let t be termal string of S;
func SubTerms(t) -> Element of (AllTermsOf S)* means :Def37:
it is (|.ar(S-firstChar.t).|)-element &
t=<*S-firstChar.t*>^(S-multiCat.it);
::# this yields the subterms of a non0wff term;
::# for an 0wff terms it returns the empty finsequence;
existence
proof
set SS=AllSymbolsOf S, T=S-termsOfMaxDepth,
TT=AllTermsOf S, s=S-firstChar.t,n=|.ar s.|;
t in TT by Def32; then
consider mmm being Element of NAT such that A1: t in T.mmm by Lm6;
reconsider tt=t as mmm-termal string of S by A1, Def33;
reconsider tttt=t as non empty FinSequence of SS by FOMODEL0:5;
per cases;
suppose mmm=0; then reconsider ttt=tt as 0-termal string of S;
reconsider e={} as Element of (AllTermsOf S)* by FINSEQ_1:49; take e;
|.ar(S-firstChar.ttt).| is zero;
hence e is n-element; len ttt=1 by CARD_1:def 7; then
tttt=<*tttt.1*> by FINSEQ_5:14
.= <*SS-firstChar.t*> ^ {} by FOMODEL0:6
.= <*SS-firstChar.t*>^(S-multiCat.e); hence thesis;
end;
suppose mmm<>0; 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 (T.mm)* such that A4:
ST is n-element & ttt=<*S-firstChar.ttt*>^((S-multiCat).ST) by Th3;
reconsider TM=T.mm as Subset of TT by Th2; ST in TM* & TM* c= TT*; then
reconsider STT=ST as Element of TT*;
take STT; thus thesis by A4;
end;
end;
uniqueness
proof
set SS=AllSymbolsOf S, T=S-termsOfMaxDepth, TT=AllTermsOf S,
s=S-firstChar.t, n=|.ar s.|;
A5: SS-multiCat is (n-tuples_on TT)-one-to-one by FOMODEL0:8;
A6: dom (SS-multiCat) = SS** by FUNCT_2:def 1;
let IT1,IT2 be Element of TT*;
reconsider IT11=IT1, IT22=IT2 as FinSequence of TT by FINSEQ_1:def 11;
assume A7: IT1 is n-element & t=<*s*>^((S-multiCat).IT1);
then len IT11=n by CARD_1:def 7; then
reconsider IT111=IT11 as Element of n-tuples_on TT by FINSEQ_2:133;
assume A8: IT2 is n-element & t=<*s*>^((S-multiCat).IT2);
then len IT22=n by CARD_1:def 7; then
reconsider IT222=IT22 as Element of n-tuples_on TT by FINSEQ_2:133;
A9: (SS-multiCat).IT111=(SS-multiCat).IT222 by FINSEQ_1:33, A7, A8;
IT111 in (n-tuples_on TT) /\ dom (SS-multiCat) &
IT222 in (n-tuples_on TT) /\ dom (SS-multiCat) by XBOOLE_0:def 4, A6;
hence thesis by A9, A5;
end;
end;

registration
let S; let t be termal string of S;
cluster SubTerms(t) -> (|.ar(t).|)-element for Element of (AllTermsOf S)*;
coherence by Def37;
end;

registration
let S; let t0 be 0-termal string of S;
cluster SubTerms(t0) -> empty for Element of (AllTermsOf S)*;
coherence
proof |.ar(t0).|=0; hence thesis; end;
end;

registration
let mm,S; let t be (mm+1)-termal string of S;
cluster SubTerms(t) ->
(S-termsOfMaxDepth.mm)-valued for Element of (AllTermsOf S)*;
coherence
proof
set T=S-termsOfMaxDepth, F=S-firstChar, C=S-multiCat, A=AllTermsOf S,
SS=AllSymbolsOf S; consider TT being Element of (T.mm)*
such that A1: TT is |.ar(t).|-element & t=<*F.t*> ^ (C.TT) by Th3;
reconsider X=T.mm as Subset of A by Th2; reconsider
Y=X* as non empty Subset of A*; reconsider TTTT=TT as Element of Y;
reconsider TTT=TTTT as Element of A*;
TTT=SubTerms(t) by Def37, A1;
hence thesis;
end;
end;

definition
let S; let phi be 0wff string of S;
func SubTerms(phi) -> |.ar(S-firstChar.phi).|-element
Element of (AllTermsOf S)* means :Def38:
phi=<*S-firstChar.phi*>^(S-multiCat.it);
existence
proof
set SS=AllSymbolsOf S, A=AllTermsOf S, C=S-multiCat, F=S-firstChar;
consider s be relational Element of S,
V being |.ar s.|-element Element of A* such that A1:
phi=<*s*>^(C.V) by Def35;
reconsider ss=s as Element of SS;
reconsider head=<*ss*> as FinSequence of SS;
reconsider tail=C.V as FinSequence of SS by FINSEQ_1:def 11;
A2: F.phi = (head^tail).1 by A1, FOMODEL0:6 .= s by FINSEQ_1:41;
reconsider VV=V as |.ar(F.phi).|-element Element of A* by A2;
take VV;
thus thesis by A2, A1;
end;
uniqueness
proof
set SS=AllSymbolsOf S, A=AllTermsOf S, C=S-multiCat, F=S-firstChar; set
n=|.ar(S-firstChar.phi).|;
A3: dom C = SS** & A* c= SS** by FUNCT_2:def 1;
reconsider s=F.phi as Element of SS; reconsider head=<*s*> as FinSequence of
SS;
let IT1, IT2 be n-element Element of A*;
reconsider I1=IT1, I2=IT2 as FinSequence of A by FINSEQ_1:def 11;
len IT1=n & len IT2=n by CARD_1:def 7; then reconsider
I11=I1, I22=I2 as Element of n-tuples_on A by FINSEQ_2:133;
reconsider tail1=C.IT1, tail2=C.IT2 as FinSequence of SS by FINSEQ_1:def 11;
assume
A4: phi=<*F.phi*>^(C.IT1) & phi=<*F.phi*>^(C.IT2);
IT1 in dom C & I11 in n-tuples_on A & IT2 in dom C & I22 in n-tuples_on A
by A3; then A5: IT1 in (n-tuples_on A) /\ dom C &
IT2 in (n-tuples_on A) /\ dom C & C.IT1=C.IT2
by A4, FINSEQ_1:33, XBOOLE_0:def 4;
C is (n-tuples_on A)-one-to-one by FOMODEL0:8;
hence thesis by A5;
end;
end;

registration
let S; let phi be 0wff string of S;
cluster SubTerms phi -> |.ar(S-firstChar.phi).|-element for FinSequence;
coherence;
end;

definition
let S;
redefine func AllTermsOf S -> Element of  :: redefines AllTermsOf (FOMODEL1, definition)
bool ((AllSymbolsOf S)*\{{}});
coherence
proof
set SS=AllSymbolsOf S, A=AllTermsOf S;
now
let x be object; assume A1: x in A; then reconsider t=x as Element of A;
not x in {{}} & x in SS* by A1; hence
x in SS*\{{}} by XBOOLE_0:def 5;
end;
hence thesis by TARSKI:def 3;
end;
end;

registration
let S;
cluster -> termal for Element of AllTermsOf S;
coherence;
end;

definition
let S;
func S-subTerms -> Function of (AllTermsOf S), (AllTermsOf S)* means
for t being Element of AllTermsOf S holds it.t=SubTerms(t);
existence
proof
set SS=AllSymbolsOf S, A=AllTermsOf S;
deffunc F(Element of A)=SubTerms($1);
consider f being Function of A,A* such that A1:
for t being Element of A holds f.t=F(t) from FUNCT_2:sch 4; take f;
thus thesis by A1;
end;
uniqueness
proof
set A=AllTermsOf S;
let IT1,IT2 be Function of A,A*;
assume A2: for t being Element of A holds IT1.t=SubTerms(t);
assume A3: for t being Element of A holds IT2.t=SubTerms(t);
now
let t be Element of A; thus IT1.t=SubTerms(t) by A2 .= IT2.t by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;

theorem S-termsOfMaxDepth.m c= S-termsOfMaxDepth.(m+n) by Lm5;

theorem
x in AllTermsOf S implies ex nn st x in S-termsOfMaxDepth.nn by Lm6;

theorem AllTermsOf S c= (AllSymbolsOf S)*\{{}};

theorem AllTermsOf S is S-prefix;

theorem x in AllTermsOf S implies x is string of S;

theorem (AtomicFormulaSymbolsOf S) \ OwnSymbolsOf S={TheEqSymbOf S}
proof
set o=the OneF of S, z=the ZeroF of S, f=the adicity of S, R=RelSymbolsOf S,
O=OwnSymbolsOf S, SS=AllSymbolsOf S, e=TheEqSymbOf S, n=TheNorSymbOf S,
A=AtomicFormulaSymbolsOf S, D = (the carrier of S) \ {o};
A1: e in A by Lm3;
A\O =
A \ (A \ {z})
by XBOOLE_1:41 .= (A \ A) \/ (A /\ {z}) by XBOOLE_1:52
.= {z} by ZFMISC_1:46, A1; hence thesis;
end;

theorem TermSymbolsOf S\(LettersOf S) = OpSymbolsOf S by FUNCT_1:69;

theorem Th11: (AtomicFormulaSymbolsOf S) \ (RelSymbolsOf S)=TermSymbolsOf S
proof
set R=RelSymbolsOf S, SSS=AtomicFormulaSymbolsOf S, f=the adicity of S;
f"INT=SSS by FUNCT_2:40; hence SSS\R =
f"(INT\(INT\NAT)) by FUNCT_1:69.=
f"(INT\INT \/ (INT /\ NAT)) by XBOOLE_1:52
.= TermSymbolsOf S by XBOOLE_1:7, XBOOLE_1:28;
end;

registration
let S;
cluster non relational -> termal for ofAtomicFormula Element of S;
coherence
proof
set R=RelSymbolsOf S, SSS=AtomicFormulaSymbolsOf S, T=TermSymbolsOf S;
let s be ofAtomicFormula Element of S; assume s is non relational;
then s in SSS & not s in R by Def20;
then s in SSS\R by XBOOLE_0:def 5; then s in T by Th11;
hence thesis;
end;
end;

definition
let S;
redefine func OwnSymbolsOf S -> Subset of AllSymbolsOf S;  :: redefines OwnSymbolsOf (FOMODEL1, definition)
coherence;
end;

registration
let S;
cluster non literal -> operational for termal Element of S;
coherence
proof
set L=LettersOf S, P=OpSymbolsOf S, T=TermSymbolsOf S, f=the adicity of S;
let s be termal Element of S; A1: s in T by Def18;
assume not s is literal; then not s in L; then
s in T\L & T\L=P by FUNCT_1:69, A1, XBOOLE_0:def 5;
hence thesis;
end;
end;

theorem Th12:
x is string of S iff x is non empty Element of ((AllSymbolsOf S)*)
proof
set SS=AllSymbolsOf S;
x is string of S iff (x in SS* & not x in {{}}) by XBOOLE_0:def 5;
hence thesis;
end;

theorem
x is string of S iff x is non empty FinSequence of (AllSymbolsOf S) by Th12;

theorem S-termsOfMaxDepth is sequence of bool((AllSymbolsOf S)*);

registration
let S;
cluster -> literal for Element of (LettersOf S);
coherence;
end;

registration
let S;
cluster TheNorSymbOf S -> non low-compounding for Element of S;
coherence
proof
set N=TheNorSymbOf S, f=the adicity of S, Low=LowerCompoundersOf S, SS
=AllSymbolsOf S;
A1: dom f = SS\{N} & N in {N} by FUNCT_2:def 1, TARSKI:def 1;
not N in Low by XBOOLE_0:def 5, A1;
hence thesis;
end;
end;

registration
let S;
cluster TheNorSymbOf S -> non own for Element of S;
coherence
proof
set N=TheNorSymbOf S,f=the adicity of S,O=OwnSymbolsOf S,SS=AllSymbolsOf S;
N in {the ZeroF of S,N} by TARSKI:def 2; then not N in O by XBOOLE_0:def 5;
hence thesis;
end;
end;

theorem
s<>TheNorSymbOf S & s<>TheEqSymbOf S implies s in OwnSymbolsOf S
proof
set O=OwnSymbolsOf S, R=RelSymbolsOf S, E=TheEqSymbOf S, X=R\O,
N=TheNorSymbOf S, SS=AllSymbolsOf S; assume s<>N & s<>E;then
not s in {N} & not s in {E} by TARSKI:def 1; then not s in {N}\/{E}
by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 5;
end;

reserve l,l1,l2 for literal Element of S, a for ofAtomicFormula Element of S,
r for relational Element of S, w,w1,w2 for string of S,
t,t1,t2 for termal string of S, tt,tt1, tt2 for Element of AllTermsOf S;

definition
let S, t;
func Depth t -> Nat means :Def40:
t is it-termal & for n st t is n-termal holds it <= n;
existence
proof
defpred P[Nat] means t is $1-termal;
set TT=AllTermsOf S, T=S-termsOfMaxDepth; reconsider TF=T as Function;
t in TT by Def32; then consider mm such that
A1: t in TF.mm by Lm6; t is mm-termal by A1; then
A2: ex n being Nat st P[n];
consider IT being Nat such that
A3: P[IT] & for n st P[n] holds IT <= n from NAT_1:sch 5(A2); take IT;
thus thesis by A3;
end;
uniqueness
proof
let IT1, IT2 be Nat; set phi=t; assume
A4: phi is IT1-termal & for n st phi is n-termal holds IT1 <= n; assume
A5: phi is IT2-termal & for n st phi is n-termal holds IT2 <= n;
A6: IT2 <= IT1 by A5, A4;
IT1 <= IT2 by A4, A5; hence thesis by A6, XXREAL_0:1;
end;
end;

registration
let S; let m0 be zero number; let t be m0-termal string of S;
cluster Depth t -> zero for number;
coherence by Def40;
end;

registration
let S; let s be low-compounding Element of S;
cluster ar(s) -> non zero for number;
coherence
proof
set f=the adicity of S, SS=AllSymbolsOf S, N=TheNorSymbOf S;
s in LowerCompoundersOf S by Def15;
then s in dom f & f.s in INT\{0} by FUNCT_1:def 7; then not f.s in {0};
hence thesis by TARSKI:def 1;
end;
end;

registration
  let S; let s be termal Element of S;
  cluster ar s -> non negative for ExtReal;
  coherence
  proof
    set f=the adicity of S, T=TermSymbolsOf S; s in T by Def18; then
    reconsider nn=ar s as Element of NAT by FUNCT_1:def 7;
    nn is non negative; hence thesis;
  end;
end;

registration
  let S; let s be relational Element of S;
  cluster ar s -> negative ext-real;
coherence
proof
set f=the adicity of S, R=RelSymbolsOf S; s in R by Def17; then
s in dom f & f.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 thesis by A1, INT_1:3;
end;
end;

theorem Th16:
  t is non 0-termal implies S-firstChar.t is operational & SubTerms t <> {}
proof
set T=S-termsOfMaxDepth, m=Depth t, ST=SubTerms t, TT=AllTermsOf S;
assume t is non 0-termal; then
m <> 0 by Def40; then
consider n such that
A1: m=n+1 by NAT_1:6;
set F=S-firstChar, C=S-multiCat,
Fam={Compound(s,T.n) where s is ofAtomicFormula Element of S:
  s is operational};
n < m by A1, NAT_1:16; then not t is n-termal & t is m-termal by Def40;
then not t in T.n & t in T.(n+1) by A1; then
(t in (union Fam) \/ T.n) & not t in T.n by Def30;
then t in union Fam by XBOOLE_0:def 3; then
consider x being set such that
A2: t in x & x in Fam by TARSKI:def 4;
consider s being ofAtomicFormula Element of S such that
A3: x=Compound(s,T.n) & s is operational by A2; set k=|.ar s.|;
consider StringTuple being Element of (AllSymbolsOf S)** such that
A4: t=<*s*>^(C.StringTuple) & rng StringTuple c= T.n
& StringTuple is (|.ar s.|)-element by A2, A3;
A5: F.t = (<*s*>^(C.StringTuple)).1 by FOMODEL0:6, A4 .=
<*s*>.1 by FOMODEL0:28 .= s; hence F.t is operational by A3;
reconsider k1=k as non zero Nat by A3; reconsider STT=ST as (k1+0)-element
Element of TT* by A5; STT <>{}; hence thesis;
end;

registration
  let S;
  cluster S-multiCat -> FinSequence-yielding for Function;
  coherence;
end;

registration
  let S; let W be non empty ((AllSymbolsOf S)*\{{}})-valued FinSequence;
  cluster S-multiCat.W -> non empty for set;
  coherence
proof
set C=S-multiCat, SS=AllSymbolsOf S, g=SS-concatenation, G=MultPlace g;
consider m 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)} \ (SS*\{{}})={}; then
A3: WW.(m+1) in SS*\{{}} 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 SS* by A3;
set VV=WW|Seg m;
reconsider VVV=VV as SS*-valued FinSequence;
VV ^ <*WW.(m+1)*> \+\ WW ={}; then
A4: G.W = G.(VVV^<*lastt*>) by FOMODEL0:29;
per cases;
suppose VVV is empty; then G.W=G.(<*lastt*>) by A4, FINSEQ_1:34
.= last by FOMODEL0:31; hence thesis by FOMODEL0:32;
end;
suppose A5: VVV is non empty; then reconsider
VVVV=VVV as Element of SS**\{{}} by FOMODEL0:30;
G.W = g.(G.VVV, lastt) by A5, A4, FOMODEL0:31 .= (G.VVVV)^last by FOMODEL0:4;
hence thesis by FOMODEL0:32;
end;
end;
end;

registration
let S, l;
cluster <*l*> -> 0-termal for string of S;
coherence
proof
set w=<*l*>, L=LettersOf S, AT=AtomicTermsOf S, T=S-termsOfMaxDepth;
reconsider ll=l as Element of L by Def14;
w=<*ll*>; then w in AT by FINSEQ_2:98; then w in T.0 by Def30;
hence thesis;
end;
end;

registration
let S, m, n;
cluster (m+0*n)-termal -> (m+n)-termal for string of S;
coherence
proof
set T=S-termsOfMaxDepth; let t be string of S; assume t is (m+0*n)-termal;
then t in T.m & T.m c= T.(m+n) by Lm5;
hence thesis;
end;
end;

registration
let S;
cluster non low-compounding -> literal for own Element of S;
coherence
proof
set L=LettersOf S, P=OpSymbolsOf S, O=OwnSymbolsOf S, T=TermSymbolsOf S;
A1: T\L=P by FUNCT_1:69; let s be own Element of S; reconsider ss=s as
ofAtomicFormula Element of S; assume
A2: s is non low-compounding; then not ss is relational; then
reconsider sss=ss as termal ofAtomicFormula Element of S; assume
not s is literal; then sss in T & not s in L by Def18;
then s in T\L by XBOOLE_0:def 5; then s is operational & not s is operational
by A2, A1; hence contradiction;
end;
end;

registration
let S, t;
cluster SubTerms t -> (rng t)*-valued for Relation;
coherence
proof
set SS=AllSymbolsOf S, C=S-multiCat, F=S-firstChar, ST=SubTerms t,
T=S-termsOfMaxDepth, TT=AllTermsOf S; reconsider TTT=TT as Subset of SS*
by XBOOLE_1:1;
t=<*F.t*>^(C.ST) by Def37; then rng (C.ST) c= rng t by FINSEQ_1:30;
then C.ST is (rng t)-valued by RELAT_1:def 19;
hence thesis by FOMODEL0:42;
end;
end;

registration
let S; let phi0 be 0wff string of S;
cluster SubTerms phi0 -> (rng phi0)*-valued for Relation;
coherence
proof
set SS=AllSymbolsOf S, C=S-multiCat, F=S-firstChar, ST=SubTerms phi0,
T=S-termsOfMaxDepth, TT=AllTermsOf S; reconsider TTT=TT as non empty
Subset of SS* by XBOOLE_1:1;
phi0=<*F.phi0*>^(C.ST) by Def38; then rng (C.ST) c= rng phi0
by FINSEQ_1:30; then C.ST is (rng phi0)-valued by RELAT_1:def 19;
hence thesis by FOMODEL0:42;
end;
end;

definition
let S;
redefine func S-termsOfMaxDepth ->  :: redefines -termsOfMaxDepth (FOMODEL1, definition)
sequence of bool((AllSymbolsOf S)*\{{}});
coherence
proof
set T=S-termsOfMaxDepth, SS=AllSymbolsOf S;
now
let y be object; assume y in rng T; then consider x being object such that
A1: x in dom T & T.x=y by FUNCT_1:def 3;
reconsider mm=x as Element of NAT by A1;
(T.mm) misses {{}}
proof
assume (T.mm) meets {{}}; then T.mm /\ {{}} <> {}; then
consider z being object such that
A2: z in T.mm /\ {{}} by XBOOLE_0:def 1;
thus contradiction by A2;
end;
then T.mm c= SS*\{{}} by XBOOLE_1:86; hence y in bool(SS*\{{}}) by A1;
end;
then rng T c= bool(SS*\{{}}) by TARSKI:def 3; hence thesis by FUNCT_2:6;
end;
end;

registration
let S,mm;
cluster S-termsOfMaxDepth.mm -> with_non-empty_elements for set;
coherence;
end;

Lm11: S-termsOfMaxDepth.m c= (TermSymbolsOf S)*
proof
set TS=TermSymbolsOf S, F=S-firstChar, C=S-multiCat,
P=OpSymbolsOf S, T=S-termsOfMaxDepth, SS=AllSymbolsOf S,
CC=TS-multiCat;
defpred P[Nat] means T.$1 c= TS*;
A1: P[0]
proof
now
let x be object; assume x in T.0; then reconsider t=x as 0-termal string of S
by Def33; reconsider s=F.t as termal Element of S;
set sub=SubTerms t; reconsider ss=s as Element of TS by Def18;
t=<*s*>^(C.sub) by Def37 .= <*s*>^{} .= <*ss*>;
then t is FinSequence of TS; hence x in TS*;
end; hence thesis by TARSKI:def 3;
end;
A2: for n st P[n] holds P[n+1]
proof
let n; reconsider nn=n, NN=n+1 as Element of NAT by ORDINAL1:def 12; assume
P[n]; then reconsider Tn=T.nn as non empty Subset of TS*;
now
let x be object; assume x in T.(n+1); then x in T.NN; then reconsider t=x as
(n+1)-termal string of S by Def33;
set s=F.t, m=|.ar s.|; reconsider tt=t as (nn+1)-termal string of S;
per cases;
suppose
A3: not t is 0-termal; then
A4: s is operational by Th16;
s in P & P c= TS by Def16, Th1, Th16, A3;
then reconsider ss=s as Element of TS;
reconsider m1=m as non zero Nat by A4; SubTerms tt is (T.nn)-valued; then
reconsider sub=SubTerms t as (m1+0)-element FinSequence of Tn by FOMODEL0:26;
sub in Tn* & Tn* c= TS**; then reconsider subb=sub as
(m1+0)-element Element of TS**;
sub is Tn-valued & Tn c= TS* & TS c= SS by XBOOLE_1:1; then
<*ss*>^(CC.subb) = <*F.t*>^(C.(SubTerms t))
by FOMODEL0:53 .= t by Def37;
then reconsider tt=t as FinSequence of TS by FOMODEL0:26;
tt in TS*; hence x in TS*;
end;
suppose
t is 0-termal; then x in T.0; hence x in TS* by A1;
end;
end;
hence thesis by TARSKI:def 3;
end;
for n holds P[n] from NAT_1:sch 2(A1, A2); hence thesis;
end;

registration
let S,m; let t be termal string of S;
cluster t null m -> (Depth t+m)-termal for string of S;
coherence
proof set d=Depth t; t is (d+0*m)-termal by Def40; hence thesis; end;
end;

registration
let S;
cluster termal -> (TermSymbolsOf S)-valued for string of S;
coherence
proof
set T=S-termsOfMaxDepth, TS=TermSymbolsOf S; let w; assume w is termal;
then reconsider tt=w as termal string of S; set d=Depth tt; reconsider
t=tt null 0 as (d+0)-termal string of S;
t in T.d & T.d c= TS* by Lm11, Def33; hence thesis;
end;
end;

registration
let S;
cluster AllTermsOf S\((TermSymbolsOf S)*) -> empty for set;
coherence
proof
set TT=AllTermsOf S, TS=TermSymbolsOf S;
now
let x be object; assume x in TT; then reconsider t=x as termal string of S;
t is FinSequence of TS by FOMODEL0:26; hence x in TS*;
end; then TT c= TS* by TARSKI:def 3; hence thesis;
end;
end;

registration
let S; let phi0 be 0wff string of S;
cluster SubTerms phi0 -> (TermSymbolsOf S)*-valued;
coherence
proof
set sub=SubTerms phi0, TS=TermSymbolsOf S, TT=AllTermsOf S;
TT\(TS*)={}; then reconsider TTT=TT as non empty Subset of TS*
by XBOOLE_1:37; sub is TTT-valued; hence thesis;
end;
end;

registration
let S;
cluster 0wff -> (AtomicFormulaSymbolsOf S)-valued for string of S;
coherence
proof
set TS=TermSymbolsOf S, AS=AtomicFormulaSymbolsOf S, F=S-firstChar,
C=S-multiCat, TT=AllTermsOf S, CC=TS-multiCat, SS=AllSymbolsOf S;
let w; assume w is 0wff; then reconsider phi=w as 0wff string of S;
reconsider r=F.phi as relational Element of S; set m=|.ar r.|;
reconsider rr=r as Element of AS by Def20;
reconsider sub=SubTerms phi as (m+0)-element Element of TT*;
TT\TS*={}; then
TS c= SS & TT c= TS* & sub is TT-valued by XBOOLE_1:1, 37; then
<*rr*>^(CC.sub) = <*r*>^(C.sub) by FOMODEL0:53 .= phi by Def38;
hence thesis;
end;
end;

registration
let S;
cluster OwnSymbolsOf S -> non empty for set;
coherence;
end;

reserve phi0 for 0wff string of S;

theorem S-firstChar.phi0<>TheEqSymbOf S implies
phi0 is (OwnSymbolsOf S)-valued
proof
set O=OwnSymbolsOf S, F=S-firstChar, r=F.phi0, C=S-multiCat, sub=
SubTerms phi0, E=TheEqSymbOf S, R=RelSymbolsOf S; reconsider
TS=TermSymbolsOf S as non empty Subset of O by Th1; assume r<>E; then
not r in {E} by TARSKI:def 1; then not r in R\O by Th1; then
r in O or not r in R by XBOOLE_0:def 5; then
reconsider rr=r as Element of O by Def17;
C.sub is TS-valued by FOMODEL0:54; then
reconsider tail=C.sub as O-valued FinSequence;
phi0=<*rr*>^tail by Def38; hence thesis;
end;

registration
cluster strict non empty for Language-like;
existence
proof
set a=the Function of NAT\{0}, INT;
take IT=Language-like(#NAT,0,0,a#); thus thesis;
end;
end;

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

registration
let S;
cluster S null -> S-extending for Language-like;
coherence;
end;

registration
let S;
cluster S-extending for Language;
existence
proof
reconsider SS=S null as Language; take SS; thus thesis;
end;
end;

registration
let S1; let S2 be S1-extending Language;
cluster OwnSymbolsOf S1 \ OwnSymbolsOf S2 -> empty for set;
coherence
proof
set O1=OwnSymbolsOf S1, O2=OwnSymbolsOf S2, f1=the adicity of S1,
f2=the adicity of S2, A1=AtomicFormulaSymbolsOf S1, SS1=AllSymbolsOf S1,
SS2=AllSymbolsOf S2, z1=the ZeroF of S1, o1=the OneF of S1,
z2=the ZeroF of S2, o2=the OneF of S2,
E1=TheEqSymbOf S1, E2=TheEqSymbOf S2, N1=TheNorSymbOf S1,
N2=TheNorSymbOf S2;
A1: dom f1=SS1\{o1} & dom f2=SS2\{o2} by FUNCT_2:def 1;
f1 c= f2 by Def41; then
(SS1\{N1}) \ {E1} c= SS2\{N2} \ {E1} by XBOOLE_1:33, GRFUNC_1:2, A1;
then SS1\({N1, E1}) c= (SS2\{N2})\{E1} by XBOOLE_1:41;
then SS1\({N1, E1}) c= SS2\({N2}\/{E1}) by XBOOLE_1:41;
then SS1\({N1, E1}) c= SS2\({N2}\/{E2}) by Def41;
hence thesis;
end;
end;

definition
let f be (INT)-valued Function; let L be non empty Language-like;
set C=the carrier of L, z=the ZeroF of L, o=the OneF of L,
a=the adicity of L, X=dom f, g=f|(X\{o}), a1=g +* a, C1=(C\/X);
func L extendWith f -> strict non empty Language-like means :Def42:
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
proof
z is Element of C null X; then
reconsider z1=z as Element of C1 by TARSKI:def 3;
o is Element of C null X; then
reconsider o1=o as Element of C1 by TARSKI:def 3;
A1: dom a=C\{o} by FUNCT_2:def 1;
dom a1 = X\{o} \/ (C\{o}) by FUNCT_4:def 1, A1 .= (X\/C)\{o}
by XBOOLE_1:42; then
dom a1 = C1\{o1} & rng a1 c= INT; then
a1 is Element of Funcs(C1\{o1}, INT) by FUNCT_2:def 2; then
reconsider a11=a1 as Function of C1\{o1}, INT;
set new=Language-like(# C1, z1, o1, a11 #);
reconsider new as strict non empty Language-like; take new; thus thesis;
end;
uniqueness
proof
let IT1, IT2 be strict non empty Language-like;
set c1=the carrier of IT1, z1=the ZeroF of IT1, o1=the OneF of IT1,
a1=the adicity of IT1;
set c2=the carrier of IT2, z2=the ZeroF of IT2, o2=the OneF of IT2,
a2=the adicity of IT2;
set ITT1=Language-like(#c1,z1,o1,a1#), ITT2=Language-like(#c2,z2,o2,a2#);
reconsider ITT1, ITT2 as non empty Language-like;
defpred P[Language-like] means the adicity of $1 = f|(dom f \ {o}) +* a
& the ZeroF of $1 = z & the OneF of $1 = o;
assume
A2: P[IT1] & P[IT2];
dom a1 = c2\{o1} by FUNCT_2:def 1, A2;
then c1\{o1}\/({o1} null c1) = c2\{o2}\/({o2} null c2) by A2, FUNCT_2:def 1
.= c2;
hence thesis by A2;
end;
end;

registration
let S be non empty Language-like; let f be (INT)-valued Function;
cluster S extendWith f -> S-extending for strict non empty Language-like;
coherence
proof
set S1=S, S2=S1 extendWith f, a1=the adicity of S1, a2=the adicity of S2,
o1=the OneF of S1;
A1: TheEqSymbOf S1=TheEqSymbOf S2 & TheNorSymbOf S1=TheNorSymbOf S2
by Def42; a2=f|(dom f\{o1}) +* a1 by Def42;
hence thesis by A1, FUNCT_4:25;
end;
end;

registration
let S be non degenerated Language-like;
cluster S-extending -> non degenerated for Language-like;
coherence
proof
set S1=S; let S2 be Language-like; assume S2 is S-extending; then
TheEqSymbOf S1=TheEqSymbOf S2 & TheNorSymbOf S1=TheNorSymbOf S2;
then 0.S1=0.S2 & 1.S1=1.S2;
hence thesis;
end;
end;

registration
let S be eligible Language-like;
cluster S-extending -> eligible for Language-like;
coherence
proof
set S1=S; let S2 be Language-like; set L1=LettersOf S1, L2=LettersOf S2,
AS1=AtomicFormulaSymbolsOf S1, AS2=AtomicFormulaSymbolsOf S2,
a1=the adicity of S1, a2=the adicity of S2, E1=TheEqSymbOf S1,
E2=TheEqSymbOf S2; assume
A1: S2 is S1-extending; then
A2: dom a1=AS1 & dom a2=AS2 & E1=E2 & a1 c= a2 by FUNCT_2:def 1;
reconsider a11=a1 as Subset of a2 by A1;
a11"{0} c= a2"{0} by RELAT_1:144; then
reconsider L11=L1 as Subset of L2; L2 null L11 is infinite;
hence L2 is infinite;
a1.E1=-2 by Def23; then E1 in dom a1 by FUNCT_1:def 2; then
a1.E1=(a2 +* a11).E1 by FUNCT_4:13 .= a2.E2 by FUNCT_4:98, A2;
hence a2.E2=-2 by Def23;
end;
end;

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

Lm12: for S1 being non empty Language-like, 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; let f be (INT)-valued Function;
set S2=S1 extendWith f, L1=LettersOf S1, a1=the adicity of S1, a2=
the adicity of S2, z1=the ZeroF of S1, o1=the OneF of S1, X=dom f\{o1},
C1=the carrier of S1, O1=OwnSymbolsOf S1, L2=LettersOf S2,
f1=f|(X\dom a1), SS1=AllSymbolsOf S1;
C1=C1\{o1}\/({o1} null C1)
.= dom a1\/{o1} by FUNCT_2:def 1; then
f1=f|(dom f \ C1) by XBOOLE_1:41; then
A1: f|(dom f \ C1) \/ a1 = f|X +* a1 by FOMODEL0:57 .= a2 by Def42;
hence L2=(f|(dom f \ SS1))"{0} \/ L1 by FOMODEL0:23;
reconsider Y=O1/\dom f as Subset of C1 by XBOOLE_1:1;
thus a2|O1 = a1|O1 \/ (f|(dom f \ C1)|O1) by A1, FOMODEL0:56 .=
a1|O1 \/ (f|(O1/\(dom f\C1))) by RELAT_1:71 .=
a1|O1 \/ (f|(Y\C1)) .= a1|O1;
end;

registration
let X; let m be Integer;
cluster X --> m -> (INT)-valued for Function;
coherence
proof
reconsider mm=m as Element of INT by INT_1:def 2;
X-->m is {mm}-valued; hence thesis;
end;
end;

definition
let S; let X be functional set;
func S addLettersNotIn X -> S-extending Language equals S extendWith (
(((AllSymbolsOf S)\/(SymbolsOf X))-freeCountableSet --> 0)
 qua (INT)-valued Function);
coherence;
end;

registration
let S1; let X be functional set;
cluster (LettersOf (S1 addLettersNotIn X)) \ SymbolsOf X -> infinite for set;
coherence
proof
set L1=LettersOf S1, S2=S1 addLettersNotIn X, no=SymbolsOf X,
L2=LettersOf S2, IT=L2\no, a1=the adicity of S1, a2=the adicity of S2,
 SS1=AllSymbolsOf S1, fresh = (SS1\/no)-freeCountableSet;
reconsider f=fresh --> 0 as (INT)-valued Function;
A1: 0 in {0} & dom (fresh-->0)=fresh by  TARSKI:def 1;
fresh /\ (SS1\/no)={}; then
fresh misses (SS1 null no)
& fresh misses (no null SS1) by XBOOLE_1:63, XBOOLE_0:def 7; then
A2: fresh\SS1=fresh & fresh\no=fresh by XBOOLE_1:83;
L2=(f|(dom f\SS1))"{0} \/ L1 by Lm12; then
IT = ((f null {})|({}\/dom f))"{0}\no \/ (L1\no)
by  XBOOLE_1:42, A2 .=
fresh \/ (L1\no) by FUNCOP_1:14, A1, A2; hence thesis;
end;
end;

registration
cluster countable for Language;
existence
proof
reconsider z=0, o=1 as Element of NAT;
set D=NAT\{o}; z in NAT & not z in {o}; then
reconsider zz=z as Element of D by XBOOLE_0:def 5;
reconsider f=D-->0, g=zz.-->(-2) as (INT)-valued Function;
set a= f+*g;
A1: zz in {zz} & dom g={zz} & dom f = D by  TARSKI:def 1;
dom a = D null {zz} by FUNCT_4:def 1; then
rng a c= INT & dom a=D; then a is Element of
Funcs(D, INT) by FUNCT_2:def 2; then
reconsider aa=a as Function of D, INT;
set IT=Language-like(#NAT, z, o, aa#);
A2: 0.IT<>1.IT;
aa.z = g.zz by A1, FUNCT_4:13 .= -2 by A1, FUNCOP_1:7; then
A3: aa.(TheEqSymbOf IT)=-2;
now
let x be object; assume
x in D\{z}; then
A4: x in D & not x in {zz}; 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; then
x in dom aa & aa.x in {0} by TARSKI:def 1, A4, FUNCT_2:def 1;
hence x in aa"{0} by FUNCT_1:def 7;
end;
then reconsider E=D\{z} as Subset of aa"{0} by TARSKI:def 3;
E is infinite & aa"{0}\/E=aa"{0} null E;
then LettersOf IT is infinite;
then reconsider IT as Language by A2, STRUCT_0:def 8, A3, Def23;
take IT;
thus thesis by ORDERS_4:def 2;
end;
end;

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

registration
let S be countable Language;
cluster (AllSymbolsOf S)*\{{}} -> countable for set;
coherence
proof
set SS=AllSymbolsOf S; reconsider C=SS* as countable set by CARD_4:13;
reconsider IT=C\{{}} as Subset of C; IT is countable; hence thesis;
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
proof
set L1=L, a1=the adicity of L1, SS1=AllSymbolsOf L1, L2=L extendWith f,
SS2=AllSymbolsOf L2, a2=the adicity of L2, X=dom f, E1=TheEqSymbOf L1,
N1=TheNorSymbOf L1, E2=TheEqSymbOf L2, N2=TheNorSymbOf L2;
reconsider Y=X\{N1} as Subset of X;
a2=f|(X\{N1}) +* a1 by Def42; then dom a2=dom (f|Y) \/ dom a1 by
FUNCT_4:def 1; then
A1: SS2\{N2}=Y\/(dom a1) by FUNCT_2:def 1 .= Y\/(SS1\{N1})
by FUNCT_2:def 1;
reconsider NN1={N1} as non empty Subset of SS1 by ZFMISC_1:31;
reconsider NN2={N2} as non empty Subset of SS2 by ZFMISC_1:31;
NN1 c= SS1 & SS1 null X c= SS1\/X; then
reconsider NN11=NN1 as non empty Subset of SS1\/X by XBOOLE_1:1;
SS2=NN2 \/ (SS2\NN2) & SS1=NN1\/(SS1\NN1) by XBOOLE_1:45; then
SS2 = NN2\/(SS1\NN1)\/Y by XBOOLE_1:4, A1 .=
NN1\/(SS1\NN1)\/Y by Def41 .= NN1\/((SS1\NN1)\/Y) by XBOOLE_1:4 .=
NN11\/((SS1\/X)\NN11) by XBOOLE_1:42 .= SS1\/X by XBOOLE_1:45;
hence thesis;
end;
end;

registration
let S be countable Language; let X be functional set;
cluster S addLettersNotIn X -> countable for 1-sorted;
coherence
proof
set S1=S,SS1=AllSymbolsOf S1,SX=SymbolsOf X, add=(SS1\/SX)-freeCountableSet,
f=add --> 0, S2=S1 extendWith f, SS2=AllSymbolsOf S2;
SS2 \+\ (dom f \/ SS1) = {}; then SS2=dom f \/ SS1 by FOMODEL0:29 .=
add \/ SS1;
hence thesis by ORDERS_4:def 2;
end;
end;

definition
let S be ZeroOneStr;
redefine attr S is degenerated means :Def44: the ZeroF of S = the OneF of S;  :: redefines degenerated (STRUCT_0, definition)
compatibility;
end;

registration
let S;
cluster AtomicTermsOf S -> infinite for set;
coherence
proof
set L=LettersOf S; card (1-tuples_on L)=card L by CARD_4:8;
hence thesis;
end;
end;

theorem X/\LettersOf S2 is infinite implies ex S1 st
(OwnSymbolsOf S1 = X/\OwnSymbolsOf S2 & S2 is S1-extending)
proof
set L2=LettersOf S2, O2=OwnSymbolsOf S2, a2=the adicity of S2, E2=TheEqSymbOf
S2, N2=TheNorSymbOf S2, SS2=AllSymbolsOf S2;
reconsider X1=SS2/\X as Subset of SS2; reconsider
N22=N2, E22=E2 as Element of SS2; {E22,N22} is Subset of SS2; then
reconsider X2={E2,N2} as non empty Subset of SS2; set SS1=X1\/X2;
assume X/\L2 is infinite; then reconsider L11=X/\L2 as infinite set;
L11 c= X/\SS2 null {E2,N2} by XBOOLE_1:26;
then reconsider SS11=SS1 as infinite Subset of SS2;
reconsider AS11=SS11\{N2} as infinite Subset of SS11;
E2 in X2 null X1 & not E2 in {N2} by TARSKI:def 1, def 2; then
reconsider E1=E2 as Element of AS11 by XBOOLE_0:def 5;
N2 in X2 null X1 by TARSKI:def 2;
then reconsider N1=N2 as Element of SS11;
reconsider D1=SS11\{N1} as infinite Subset of SS2\{N2} by XBOOLE_1:33;
rng (a2|D1) c= INT & dom (a2|D1)=D1 by PARTFUN1:def 2; then
reconsider a1=a2|D1 as Function of SS11\{N1}, INT by FUNCT_2:2;
reconsider a11=a2|D1 as Subset of a2;
set S1=Language-like (# SS11, E1 qua Element of SS11, N1, a1 #),
O1=OwnSymbolsOf S1, L1=LettersOf S1;
reconsider IT=S1 as non degenerated Language-like by Def44;
A1: L1 = a2"{0} /\ D1 by FUNCT_1:70 .=
L2 /\ SS11 \ {N1} by XBOOLE_1:49 .=
L2 /\ (SS2/\X) \/ L2/\{E2,N2} \ {N2} by XBOOLE_1:23 .=
L2 null SS2 /\ X\/L2/\{E2,N2}\{N2} by XBOOLE_1:16
.= L11\/(L2/\{E2,N2})\{N2};
a1.E1 \+\ a2.E1 = {}; then a1.E1=a2.E2 &
a2.E2=-2 by Def23, FOMODEL0:29; then
(the adicity of IT).(TheEqSymbOf IT)=-2 &
LettersOf IT is infinite by A1; then reconsider IT as Language
by Def23; take IT; SS1\X2=X1\X2 \/ (X2\X2) by XBOOLE_1:42 .=
O2/\X by XBOOLE_1:49;
hence OwnSymbolsOf IT = X/\O2; thus thesis;
end;

definition
let S; let w1,w2 be string of S;
redefine func w1^w2 -> string of S;  :: redefines ^ (FINSEQ_1, definition)
coherence
proof
set SS=AllSymbolsOf S;
reconsider w11=w1, w22=w2 as non empty FinSequence of SS by FOMODEL0:5;
w11^w22 is non empty FinSequence of SS; hence thesis by FOMODEL0:5;
end;
end;

definition
let S,s;
redefine func <*s*> -> string of S;  :: redefines <* (FINSEQ_1, definition)
coherence
proof
set SS=AllSymbolsOf S; <*s*> is non empty FinSequence of SS;
hence thesis by FOMODEL0:5;
end;
end;

Lm13: <*TheEqSymbOf S*>^t1^t2 is 0wff string of S
proof
set E=TheEqSymbOf S, AT=AllTermsOf S, C=S-multiCat, SS=AllSymbolsOf S;
reconsider tt1=t1,tt2=t2 as Element of AT by Def32; reconsider
T=<*tt1*>^<*tt2*> as 2-element Element of (AT*);
reconsider ATT=AT as Subset of SS* by XBOOLE_1:1; reconsider
TT=T as Element of ATT*;
reconsider TTT=TT as Element of SS**;
reconsider EE=E as ofAtomicFormula Element of S;
A1: |.-2.|=-(-2) by ABSVALUE:def 1 .= 2;
A2: |.ar(EE).|=2 by A1, Def23; C.TT is Element of SS*;
then reconsider tailer=C.T as FinSequence of SS;
reconsider SSS=SS as non empty set;
reconsider EEE=EE as Element of SSS;
reconsider header=<*EEE*> as FinSequence of SS;
reconsider IT=header^tailer as non empty FinSequence of SS;
reconsider phi=IT as string of S by Th12;
tailer = (SS-multiCat.<*tt1,tt2*>) .= tt1^tt2 by FOMODEL0:15;
then phi=<*E*>^tt1^tt2 &
phi is 0wff string of S by A2, Def35, FINSEQ_1:32;
hence thesis;
end;

registration
let S; let t1,t2 be termal string of S;
cluster <*TheEqSymbOf S*>^t1^t2 -> 0wff for string of S;
coherence by Lm13;
end;