:: by Marco B. Caminati

::

:: Received December 29, 2010

:: Copyright (c) 2010-2013 Association of Mizar Users

registration

let z be zero Integer;

coherence

for b_{1} being Integer st b_{1} = |.z.| holds

b_{1} is zero
by COMPLEX1:47;

end;
coherence

for b

b

registration
end;

definition

attr c_{1} is strict ;

struct Language-like -> ZeroOneStr ;

aggr Language-like(# carrier, ZeroF, OneF, adicity #) -> Language-like ;

sel adicity c_{1} -> Function of ( the carrier of c_{1} \ { the OneF of c_{1}}),INT;

end;
struct Language-like -> ZeroOneStr ;

aggr Language-like(# carrier, ZeroF, OneF, adicity #) -> Language-like ;

sel adicity c

definition

let S be Language-like ;

coherence

the carrier of S is set ;

coherence

the adicity of S " {0} is set ;

coherence

the adicity of S " (NAT \ {0}) is set ;

coherence

the adicity of S " (INT \ NAT) is set ;

coherence

the adicity of S " NAT is set ;

coherence

the adicity of S " (INT \ {0}) is set ;

coherence

the ZeroF of S is set ;

coherence

the OneF of S is set ;

the carrier of S \ { the ZeroF of S, the OneF of S} is set ;

end;
coherence

the carrier of S is set ;

coherence

the adicity of S " {0} is set ;

coherence

the adicity of S " (NAT \ {0}) is set ;

coherence

the adicity of S " (INT \ NAT) is set ;

coherence

the adicity of S " NAT is set ;

coherence

the adicity of S " (INT \ {0}) is set ;

coherence

the ZeroF of S is set ;

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

the carrier of S \ { the ZeroF of S, the OneF of S} is set ;

:: deftheorem defines AllSymbolsOf FOMODEL1:def 1 :

for S being Language-like holds AllSymbolsOf S = the carrier of S;

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

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

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

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;

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

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;

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;

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

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;

(AllSymbolsOf S) \ {(TheNorSymbOf S)} is set ;

coherence

1 -tuples_on (LettersOf S) is set ;

end;
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)};

(AllSymbolsOf S) \ {(TheNorSymbOf S)} is set ;

coherence

1 -tuples_on (LettersOf S) is set ;

:: deftheorem defines AtomicFormulaSymbolsOf FOMODEL1:def 10 :

for S being Language-like holds AtomicFormulaSymbolsOf S = (AllSymbolsOf S) \ {(TheNorSymbOf S)};

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

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

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

for S being Language-like holds

( S is relational iff not (RelSymbolsOf S) \ {(TheEqSymbOf S)} is empty );

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

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

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

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

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

for S being Language-like

for s being Element of S holds

( s is termal iff s in TermSymbolsOf S );

:: deftheorem defines own FOMODEL1:def 19 :

for S being Language-like

for s being Element of S holds

( s is own iff s in OwnSymbolsOf S );

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

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

( ( s = the ZeroF of S implies - 2 is Integer ) & ( not s = the ZeroF of S implies 0 is Integer ) ) ;

consistency

for b_{1} being Integer holds verum
;

end;
let s be Element of the carrier of S \ { the OneF of S};

func TrivialArity s -> Integer equals :Def21: :: FOMODEL1:def 21

- 2 if s = the ZeroF of S

otherwise 0 ;

coherence - 2 if s = the ZeroF of S

otherwise 0 ;

( ( s = the ZeroF of S implies - 2 is Integer ) & ( not s = the ZeroF of S implies 0 is Integer ) ) ;

consistency

for b

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

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

definition

let S be non degenerated ZeroOneStr ;

ex b_{1} 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 b_{1} . s = TrivialArity s

for b_{1}, b_{2} 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 b_{1} . s = TrivialArity s ) & ( for s being Element of the carrier of S \ { the OneF of S} holds b_{2} . s = TrivialArity s ) holds

b_{1} = b_{2}

end;
func S TrivialArity -> Function of ( the carrier of S \ { the OneF of S}),INT means :Def22: :: FOMODEL1:def 22

for s being Element of the carrier of S \ { the OneF of S} holds it . s = TrivialArity s;

existence for s being Element of the carrier of S \ { the OneF of S} holds it . s = TrivialArity s;

ex b

for s being Element of the carrier of S \ { the OneF of S} holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 defines TrivialArity FOMODEL1:def 22 :

for S being non degenerated ZeroOneStr

for b_{2} being Function of ( the carrier of S \ { the OneF of S}),INT holds

( b_{2} = S TrivialArity iff for s being Element of the carrier of S \ { the OneF of S} holds b_{2} . s = TrivialArity s );

for S being non degenerated ZeroOneStr

for b

( b

registration
end;

registration

let S be non degenerated infinite ZeroOneStr ;

coherence

for b_{1} being set st b_{1} = (S TrivialArity) " {0} holds

not b_{1} is finite

end;
coherence

for b

not b

proof end;

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

proof end;

definition

let S be Language-like ;

end;
attr S is eligible means :Def23: :: FOMODEL1:def 23

( LettersOf S is infinite & the adicity of S . (TheEqSymbOf S) = - 2 );

( LettersOf S is infinite & the adicity of S . (TheEqSymbOf S) = - 2 );

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

for S being Language-like holds

( S is eligible iff ( LettersOf S is infinite & the adicity of S . (TheEqSymbOf S) = - 2 ) );

Lm2: ex S being Language-like st

( not S is degenerated & S is eligible )

proof end;

registration
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;
:: original: AllSymbolsOf

redefine func AllSymbolsOf S -> non empty set ;

coherence

AllSymbolsOf S is non empty set ;

registration

let S be eligible Language-like ;

coherence

for b_{1} being set st b_{1} = LettersOf S holds

not b_{1} is finite
by Def23;

end;
coherence

for b

not b

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

Lm3: for S being non degenerated Language-like holds TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)}

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of S st b_{1} = TheEqSymbOf S holds

b_{1} is relational

end;
coherence

for b

b

proof 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;
:: original: AtomicFormulaSymbolsOf

redefine func AtomicFormulaSymbolsOf S -> non empty Subset of (AllSymbolsOf S);

coherence

AtomicFormulaSymbolsOf S is non empty Subset of (AllSymbolsOf S) ;

definition

let S be Language;

:: original: TheEqSymbOf

redefine func TheEqSymbOf S -> Element of S;

coherence

TheEqSymbOf S is Element of S ;

end;
:: original: TheEqSymbOf

redefine func TheEqSymbOf S -> Element of S;

coherence

TheEqSymbOf S is Element of S ;

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 )

( (LettersOf S) /\ (OpSymbolsOf S) = {} & (TermSymbolsOf S) /\ (LowerCompoundersOf S) = OpSymbolsOf S & (RelSymbolsOf S) \ (OwnSymbolsOf S) = {(TheEqSymbOf S)} & OwnSymbolsOf S c= AtomicFormulaSymbolsOf S & RelSymbolsOf S c= LowerCompoundersOf S & OpSymbolsOf S c= TermSymbolsOf S & LettersOf S c= TermSymbolsOf S & TermSymbolsOf S c= OwnSymbolsOf S & OpSymbolsOf S c= LowerCompoundersOf S & LowerCompoundersOf S c= AtomicFormulaSymbolsOf S )

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = TermSymbolsOf S holds

not b_{1} is empty

for b_{1} being Element of S st b_{1} is own holds

b_{1} is ofAtomicFormula

for b_{1} being Element of S st b_{1} is relational holds

b_{1} is low-compounding

for b_{1} being Element of S st b_{1} is operational holds

b_{1} is termal

for b_{1} being Element of S st b_{1} is literal holds

b_{1} is termal

for b_{1} being Element of S st b_{1} is termal holds

b_{1} is own

for b_{1} being Element of S st b_{1} is operational holds

b_{1} is low-compounding

for b_{1} being Element of S st b_{1} is low-compounding holds

b_{1} is ofAtomicFormula
;

coherence

for b_{1} being Element of S st b_{1} is termal holds

not b_{1} is relational

for b_{1} being Element of S st b_{1} is literal holds

not b_{1} is relational
;

coherence

for b_{1} being Element of S st b_{1} is literal holds

not b_{1} is operational

end;
coherence

for b

not b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

coherence

for b

not b

proof end;

coherence for b

not b

coherence

for b

not b

proof end;

registration

let S be Language;

existence

ex b_{1} being Element of S st b_{1} is relational

ex b_{1} being Element of S st b_{1} is literal

end;
existence

ex b

proof end;

existence ex b

proof end;

registration

let S be Language;

coherence

for b_{1} being low-compounding Element of S st b_{1} is termal holds

b_{1} is operational

end;
coherence

for b

b

proof end;

registration
end;

definition

let S be Language;

let s be ofAtomicFormula Element of S;

coherence

the adicity of S . s is Element of INT

end;
let s be ofAtomicFormula Element of S;

coherence

the adicity of S . s is Element of INT

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

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;

coherence

for b_{1} being number st b_{1} = ar s holds

b_{1} is zero

end;
let s be literal Element of S;

coherence

for b

b

proof end;

definition

let S be Language;

(AllSymbolsOf S) -concatenation is BinOp of ((AllSymbolsOf S) *) ;

end;
func S -cons -> BinOp of ((AllSymbolsOf S) *) equals :: FOMODEL1:def 25

(AllSymbolsOf S) -concatenation ;

coherence (AllSymbolsOf S) -concatenation ;

(AllSymbolsOf S) -concatenation is BinOp of ((AllSymbolsOf S) *) ;

:: deftheorem defines -cons FOMODEL1:def 25 :

for S being Language holds S -cons = (AllSymbolsOf S) -concatenation ;

for S being Language holds S -cons = (AllSymbolsOf S) -concatenation ;

definition

let S be Language;

(AllSymbolsOf S) -multiCat is Function of (((AllSymbolsOf S) *) *),((AllSymbolsOf S) *) ;

end;
func S -multiCat -> Function of (((AllSymbolsOf S) *) *),((AllSymbolsOf S) *) equals :: FOMODEL1:def 26

(AllSymbolsOf S) -multiCat ;

coherence (AllSymbolsOf S) -multiCat ;

(AllSymbolsOf S) -multiCat is Function of (((AllSymbolsOf S) *) *),((AllSymbolsOf S) *) ;

:: deftheorem defines -multiCat FOMODEL1:def 26 :

for S being Language holds S -multiCat = (AllSymbolsOf S) -multiCat ;

for S being Language holds S -multiCat = (AllSymbolsOf S) -multiCat ;

definition

let S be Language;

(AllSymbolsOf S) -firstChar is Function of (((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S) ;

end;
func S -firstChar -> Function of (((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S) equals :: FOMODEL1:def 27

(AllSymbolsOf S) -firstChar ;

coherence (AllSymbolsOf S) -firstChar ;

(AllSymbolsOf S) -firstChar is Function of (((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S) ;

:: deftheorem defines -firstChar FOMODEL1:def 27 :

for S being Language holds S -firstChar = (AllSymbolsOf S) -firstChar ;

for S being Language holds S -firstChar = (AllSymbolsOf S) -firstChar ;

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

for S being Language

for X being set holds

( X is S -prefix iff X is AllSymbolsOf S -prefix );

registration

let S be Language;

coherence

for b_{1} being set st b_{1} is S -prefix holds

b_{1} is AllSymbolsOf S -prefix
;

coherence

for b_{1} being set st b_{1} is AllSymbolsOf S -prefix holds

b_{1} is S -prefix
;

end;
coherence

for b

b

coherence

for b

b

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = ((AllSymbolsOf S) *) \ {{}} holds

not b_{1} is empty
;

end;
coherence

for b

not b

registration
end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = AllSymbolsOf S holds

not b_{1} is finite
;

end;
coherence

for b

not b

definition

let S be Language;

let s be ofAtomicFormula Element of S;

let Strings be set ;

{ (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } is set ;

end;
let s be ofAtomicFormula Element of S;

let Strings be set ;

func Compound (s,Strings) -> set equals :: FOMODEL1:def 29

{ (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } ;

coherence { (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } ;

{ (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } is set ;

:: deftheorem defines Compound FOMODEL1:def 29 :

for S being Language

for s being ofAtomicFormula Element of S

for Strings being set holds Compound (s,Strings) = { (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } ;

for S being Language

for s being ofAtomicFormula Element of S

for Strings being set holds Compound (s,Strings) = { (<*s*> ^ ((S -multiCat) . StringTuple)) where StringTuple is Element of ((AllSymbolsOf S) *) * : ( rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) } ;

definition

let S be Language;

let s be ofAtomicFormula Element of S;

let Strings be set ;

:: original: Compound

redefine func Compound (s,Strings) -> Element of bool (((AllSymbolsOf S) *) \ {{}});

coherence

Compound (s,Strings) is Element of bool (((AllSymbolsOf S) *) \ {{}})

end;
let s be ofAtomicFormula Element of S;

let Strings be set ;

:: original: Compound

redefine func Compound (s,Strings) -> Element of bool (((AllSymbolsOf S) *) \ {{}});

coherence

Compound (s,Strings) is Element of bool (((AllSymbolsOf S) *) \ {{}})

proof end;

definition

let S be Language;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = AtomicTermsOf S & ( for n being Nat holds b_{1} . (n + 1) = (union { (Compound (s,(b_{1} . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b_{1} . n) ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & b_{1} . 0 = AtomicTermsOf S & ( for n being Nat holds b_{1} . (n + 1) = (union { (Compound (s,(b_{1} . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b_{1} . n) ) & dom b_{2} = NAT & b_{2} . 0 = AtomicTermsOf S & ( for n being Nat holds b_{2} . (n + 1) = (union { (Compound (s,(b_{2} . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b_{2} . n) ) holds

b_{1} = b_{2}

end;
func S -termsOfMaxDepth -> Function means :Def30: :: FOMODEL1:def 30

( dom it = NAT & it . 0 = AtomicTermsOf S & ( for n being Nat holds it . (n + 1) = (union { (Compound (s,(it . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (it . n) ) );

existence ( 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) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def30 defines -termsOfMaxDepth FOMODEL1:def 30 :

for S being Language

for b_{2} being Function holds

( b_{2} = S -termsOfMaxDepth iff ( dom b_{2} = NAT & b_{2} . 0 = AtomicTermsOf S & ( for n being Nat holds b_{2} . (n + 1) = (union { (Compound (s,(b_{2} . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b_{2} . n) ) ) );

for S being Language

for b

( b

definition

let S be Language;

:: original: AtomicTermsOf

redefine func AtomicTermsOf S -> Subset of ((AllSymbolsOf S) *);

coherence

AtomicTermsOf S is Subset of ((AllSymbolsOf S) *)

end;
:: original: AtomicTermsOf

redefine func AtomicTermsOf S -> Subset of ((AllSymbolsOf S) *);

coherence

AtomicTermsOf S is Subset of ((AllSymbolsOf S) *)

proof end;

Lm4: for m being Nat

for S being Language holds (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}

proof end;

Lm5: for m, n being Nat

for S being Language holds (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n)

proof end;

:: deftheorem defines AllTermsOf FOMODEL1:def 31 :

for S being Language holds AllTermsOf S = union (rng (S -termsOfMaxDepth));

for S being Language holds AllTermsOf S = union (rng (S -termsOfMaxDepth));

Lm6: for x being set

for S being Language st x in AllTermsOf S holds

ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn

proof end;

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

for S being Language

for w being string of S holds

( w is termal iff w in AllTermsOf S );

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

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;

coherence

for b_{1} being string of S st b_{1} is m -termal holds

b_{1} is termal

end;
let S be Language;

coherence

for b

b

proof end;

definition

let S be Language;

:: original: -termsOfMaxDepth

redefine func S -termsOfMaxDepth -> sequence of (bool ((AllSymbolsOf S) *));

coherence

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

end;
:: original: -termsOfMaxDepth

redefine func S -termsOfMaxDepth -> sequence of (bool ((AllSymbolsOf S) *));

coherence

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

proof 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) *)

end;
:: original: AllTermsOf

redefine func AllTermsOf S -> non empty Subset of ((AllSymbolsOf S) *);

coherence

AllTermsOf S is non empty Subset of ((AllSymbolsOf S) *)

proof end;

registration
end;

registration
end;

registration

let S be Language;

let m be Nat;

coherence

for b_{1} being Element of (S -termsOfMaxDepth) . m holds not b_{1} is empty

end;
let m be Nat;

coherence

for b

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of AllTermsOf S holds not b_{1} is empty

end;
coherence

for b

proof end;

registration

let m be Nat;

let S be Language;

ex b_{1} being string of S st b_{1} is m -termal

end;
let S be Language;

cluster Relation-like omega -defined non empty non zero Function-like finite FinSequence-like FinSubsequence-like countable finite-support m -termal for Element of ((AllSymbolsOf S) *) \ {{}};

existence ex b

proof end;

registration

let S be Language;

coherence

for b_{1} being string of S st b_{1} is 0 -termal holds

b_{1} is 1 -element

end;
coherence

for b

b

proof end;

registration

let S be Language;

let w be 0 -termal string of S;

coherence

for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

b_{1} is literal

end;
let w be 0 -termal string of S;

coherence

for b

b

proof end;

Lm7: for mm being Element of NAT

for S being Language

for w being b

ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mm) * st

( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

proof end;

Lm8: for mm being Element of NAT

for S being Language

for w being b

( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

proof end;

registration

let S be Language;

let w be termal string of S;

coherence

for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

b_{1} is termal

end;
let w be termal string of S;

coherence

for b

b

proof end;

definition

let S be Language;

let t be termal string of S;

coherence

ar ((S -firstChar) . t) is Element of INT ;

end;
let t be termal string of S;

coherence

ar ((S -firstChar) . t) is Element of INT ;

:: deftheorem defines ar FOMODEL1:def 34 :

for S being Language

for t being termal string of S holds ar t = ar ((S -firstChar) . t);

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 b_{1} + 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) )

for S being Language

for w being b

( T is |.(ar ((S -firstChar) . w)).| -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )

proof end;

Lm9: for m being Nat

for S being Language holds (S -termsOfMaxDepth) . m is S -prefix

proof end;

registration

let S be Language;

let m be Nat;

coherence

for b_{1} being set st b_{1} = (S -termsOfMaxDepth) . m holds

b_{1} is S -prefix
by Lm9;

end;
let m be Nat;

coherence

for b

b

registration

let S be Language;

let V be Element of (AllTermsOf S) * ;

coherence

for b_{1} being set st b_{1} = (S -multiCat) . V holds

b_{1} is Relation-like
;

end;
let V be Element of (AllTermsOf S) * ;

coherence

for b

b

registration

let S be Language;

let V be Element of (AllTermsOf S) * ;

coherence

for b_{1} being Relation st b_{1} = (S -multiCat) . V holds

b_{1} is Function-like
;

end;
let V be Element of (AllTermsOf S) * ;

coherence

for b

b

:: deftheorem Def35 defines 0wff FOMODEL1:def 35 :

for S being Language

for phi being string of S holds

( phi is 0wff iff ex s being relational Element of S ex V being |.(ar b_{3}).| -element Element of (AllTermsOf S) * st phi = <*s*> ^ ((S -multiCat) . V) );

for S being Language

for phi being string of S holds

( phi is 0wff iff ex s being relational Element of S ex V being |.(ar b

registration

let S be Language;

ex b_{1} being string of S st b_{1} is 0wff

end;
cluster Relation-like omega -defined non empty non zero Function-like finite FinSequence-like FinSubsequence-like countable finite-support 0wff for Element of ((AllSymbolsOf S) *) \ {{}};

existence ex b

proof end;

registration

let S be Language;

let phi be 0wff string of S;

coherence

for b_{1} being Element of S st b_{1} = (S -firstChar) . phi holds

b_{1} is relational

end;
let phi be 0wff string of S;

coherence

for b

b

proof end;

definition

let S be Language;

{ phi where phi is string of S : phi is 0wff } is set ;

end;
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 } ;

{ phi where phi is string of S : phi is 0wff } is set ;

:: deftheorem defines AtomicFormulasOf FOMODEL1:def 36 :

for S being Language holds AtomicFormulasOf S = { phi where phi is string of S : phi is 0wff } ;

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) *) \ {{}})

end;
:: original: AtomicFormulasOf

redefine func AtomicFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}});

coherence

AtomicFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = AtomicFormulasOf S holds

not b_{1} is empty

end;
coherence

for b

not b

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of AtomicFormulasOf S holds b_{1} is 0wff

end;
coherence

for b

proof end;

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

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = AllTermsOf S holds

b_{1} is S -prefix
by Lm10;

end;
coherence

for b

b

definition

let S be Language;

let t be termal string of S;

ex b_{1} being Element of (AllTermsOf S) * st

( b_{1} is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b_{1}) )

for b_{1}, b_{2} being Element of (AllTermsOf S) * st b_{1} is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b_{1}) & b_{2} is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b_{2}) holds

b_{1} = b_{2}

end;
let t be termal string of S;

func SubTerms t -> Element of (AllTermsOf S) * means :Def37: :: FOMODEL1:def 37

( it is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . it) );

existence ( it is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . it) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def37 defines SubTerms FOMODEL1:def 37 :

for S being Language

for t being termal string of S

for b_{3} being Element of (AllTermsOf S) * holds

( b_{3} = SubTerms t iff ( b_{3} is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b_{3}) ) );

for S being Language

for t being termal string of S

for b

( b

registration

let S be Language;

let t be termal string of S;

coherence

for b_{1} being Element of (AllTermsOf S) * st b_{1} = SubTerms t holds

b_{1} is |.(ar t).| -element
by Def37;

end;
let t be termal string of S;

coherence

for b

b

registration

let S be Language;

let t0 be 0 -termal string of S;

coherence

for b_{1} being Element of (AllTermsOf S) * st b_{1} = SubTerms t0 holds

b_{1} is empty

end;
let t0 be 0 -termal string of S;

coherence

for b

b

proof end;

registration

let mm be Element of NAT ;

let S be Language;

let t be mm + 1 -termal string of S;

coherence

for b_{1} being Element of (AllTermsOf S) * st b_{1} = SubTerms t holds

b_{1} is (S -termsOfMaxDepth) . mm -valued

end;
let S be Language;

let t be mm + 1 -termal string of S;

coherence

for b

b

proof end;

definition

let S be Language;

let phi be 0wff string of S;

ex b_{1} being |.(ar ((S -firstChar) . phi)).| -element Element of (AllTermsOf S) * st phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b_{1})

for b_{1}, b_{2} being |.(ar ((S -firstChar) . phi)).| -element Element of (AllTermsOf S) * st phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b_{1}) & phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b_{2}) holds

b_{1} = b_{2}

end;
let phi be 0wff string of S;

func SubTerms phi -> |.(ar ((S -firstChar) . phi)).| -element Element of (AllTermsOf S) * means :Def38: :: FOMODEL1:def 38

phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . it);

existence phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . it);

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def38 defines SubTerms FOMODEL1:def 38 :

for S being Language

for phi being 0wff string of S

for b_{3} being |.(ar ((b_{1} -firstChar) . b_{2})).| -element Element of (AllTermsOf S) * holds

( b_{3} = SubTerms phi iff phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . b_{3}) );

for S being Language

for phi being 0wff string of S

for b

( b

registration

let S be Language;

let phi be 0wff string of S;

coherence

for b_{1} being FinSequence st b_{1} = SubTerms phi holds

b_{1} is |.(ar ((S -firstChar) . phi)).| -element
;

end;
let phi be 0wff string of S;

coherence

for b

b

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) *) \ {{}})

end;
:: original: AllTermsOf

redefine func AllTermsOf S -> Element of bool (((AllSymbolsOf S) *) \ {{}});

coherence

AllTermsOf S is Element of bool (((AllSymbolsOf S) *) \ {{}})

proof end;

registration
end;

definition

let S be Language;

ex b_{1} being Function of (AllTermsOf S),((AllTermsOf S) *) st

for t being Element of AllTermsOf S holds b_{1} . t = SubTerms t

for b_{1}, b_{2} being Function of (AllTermsOf S),((AllTermsOf S) *) st ( for t being Element of AllTermsOf S holds b_{1} . t = SubTerms t ) & ( for t being Element of AllTermsOf S holds b_{2} . t = SubTerms t ) holds

b_{1} = b_{2}

end;
func S -subTerms -> Function of (AllTermsOf S),((AllTermsOf S) *) means :: FOMODEL1:def 39

for t being Element of AllTermsOf S holds it . t = SubTerms t;

existence for t being Element of AllTermsOf S holds it . t = SubTerms t;

ex b

for t being Element of AllTermsOf S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines -subTerms FOMODEL1:def 39 :

for S being Language

for b_{2} being Function of (AllTermsOf S),((AllTermsOf S) *) holds

( b_{2} = S -subTerms iff for t being Element of AllTermsOf S holds b_{2} . t = SubTerms t );

for S being Language

for b

( b

theorem :: FOMODEL1:4

for m, n being Nat

for S being Language holds (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n) by Lm5;

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;

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:8

theorem :: FOMODEL1:10

registration

let S be Language;

coherence

for b_{1} being ofAtomicFormula Element of S st not b_{1} is relational holds

b_{1} is termal

end;
coherence

for b

b

proof 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;
:: original: OwnSymbolsOf

redefine func OwnSymbolsOf S -> Subset of (AllSymbolsOf S);

coherence

OwnSymbolsOf S is Subset of (AllSymbolsOf S) ;

registration

let S be Language;

coherence

for b_{1} being termal Element of S st not b_{1} is literal holds

b_{1} is operational

end;
coherence

for b

b

proof 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) * )

for S being Language holds

( x is string of S iff x is non empty Element of (AllSymbolsOf S) * )

proof end;

theorem :: FOMODEL1:13

for x being set

for S being Language holds

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

for S being Language holds

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

theorem :: FOMODEL1:14

registration
end;

registration

let S be Language;

coherence

for b_{1} being Element of S st b_{1} = TheNorSymbOf S holds

not b_{1} is low-compounding

end;
coherence

for b

not b

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of S st b_{1} = TheNorSymbOf S holds

not b_{1} is own

end;
coherence

for b

not b

proof 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

for s being Element of S st s <> TheNorSymbOf S & s <> TheEqSymbOf S holds

s in OwnSymbolsOf S

proof end;

definition

let S be Language;

let t be termal string of S;

ex b_{1} being Nat st

( t is b_{1} -termal & ( for n being Nat st t is n -termal holds

b_{1} <= n ) )

for b_{1}, b_{2} being Nat st t is b_{1} -termal & ( for n being Nat st t is n -termal holds

b_{1} <= n ) & t is b_{2} -termal & ( for n being Nat st t is n -termal holds

b_{2} <= n ) holds

b_{1} = b_{2}

end;
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 ( t is it -termal & ( for n being Nat st t is n -termal holds

it <= n ) );

ex b

( t is b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def40 defines Depth FOMODEL1:def 40 :

for S being Language

for t being termal string of S

for b_{3} being Nat holds

( b_{3} = Depth t iff ( t is b_{3} -termal & ( for n being Nat st t is n -termal holds

b_{3} <= n ) ) );

for S being Language

for t being termal string of S

for b

( b

b

registration

let S be Language;

let m0 be zero number ;

let t be m0 -termal string of S;

coherence

for b_{1} being number st b_{1} = Depth t holds

b_{1} is zero
by Def40;

end;
let m0 be zero number ;

let t be m0 -termal string of S;

coherence

for b

b

registration

let S be Language;

let s be low-compounding Element of S;

coherence

for b_{1} being number st b_{1} = ar s holds

not b_{1} is zero

end;
let s be low-compounding Element of S;

coherence

for b

not b

proof end;

registration

let S be Language;

let s be termal Element of S;

coherence

for b_{1} being ExtReal st b_{1} = ar s holds

not b_{1} is negative

end;
let s be termal Element of S;

coherence

for b

not b

proof end;

registration

let S be Language;

let s be relational Element of S;

coherence

( ar s is negative & ar s is ext-real )

end;
let s be relational Element of S;

coherence

( ar s is negative & ar s is ext-real )

proof 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 <> {} )

for t being termal string of S st not t is 0 -termal holds

( (S -firstChar) . t is operational & SubTerms t <> {} )

proof end;

registration

let S be Language;

coherence

for b_{1} being Function st b_{1} = S -multiCat holds

b_{1} is FinSequence-yielding
;

end;
coherence

for b

b

registration

let S be Language;

let W be ((AllSymbolsOf S) *) \ {{}} -valued non empty FinSequence;

coherence

for b_{1} being set st b_{1} = (S -multiCat) . W holds

not b_{1} is empty

end;
let W be ((AllSymbolsOf S) *) \ {{}} -valued non empty FinSequence;

coherence

for b

not b

proof end;

registration

let S be Language;

let l be literal Element of S;

coherence

for b_{1} being string of S st b_{1} = <*l*> holds

b_{1} is 0 -termal

end;
let l be literal Element of S;

coherence

for b

b

proof end;

registration

let S be Language;

let m, n be Nat;

coherence

for b_{1} being string of S st b_{1} is m + (0 * n) -termal holds

b_{1} is m + n -termal

end;
let m, n be Nat;

coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being own Element of S st not b_{1} is low-compounding holds

b_{1} is literal

end;
coherence

for b

b

proof end;

registration

let S be Language;

let t be termal string of S;

coherence

for b_{1} being Relation st b_{1} = SubTerms t holds

b_{1} is (rng t) * -valued

end;
let t be termal string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let phi0 be 0wff string of S;

coherence

for b_{1} being Relation st b_{1} = SubTerms phi0 holds

b_{1} is (rng phi0) * -valued

end;
let phi0 be 0wff string of S;

coherence

for b

b

proof end;

definition

let S be Language;

:: original: -termsOfMaxDepth

redefine func S -termsOfMaxDepth -> sequence of (bool (((AllSymbolsOf S) *) \ {{}}));

coherence

S -termsOfMaxDepth is sequence of (bool (((AllSymbolsOf S) *) \ {{}}))

end;
:: original: -termsOfMaxDepth

redefine func S -termsOfMaxDepth -> sequence of (bool (((AllSymbolsOf S) *) \ {{}}));

coherence

S -termsOfMaxDepth is sequence of (bool (((AllSymbolsOf S) *) \ {{}}))

proof end;

registration

let S be Language;

let mm be Element of NAT ;

coherence

for b_{1} being set st b_{1} = (S -termsOfMaxDepth) . mm holds

b_{1} is with_non-empty_elements
;

end;
let mm be Element of NAT ;

coherence

for b

b

Lm11: for m being Nat

for S being Language holds (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) *

proof end;

registration

let S be Language;

let m be Nat;

let t be termal string of S;

coherence

for b_{1} being string of S st b_{1} = t null m holds

b_{1} is (Depth t) + m -termal

end;
let m be Nat;

let t be termal string of S;

coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being string of S st b_{1} is termal holds

b_{1} is TermSymbolsOf S -valued

end;
coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = (AllTermsOf S) \ ((TermSymbolsOf S) *) holds

b_{1} is empty

end;
coherence

for b

b

proof end;

registration

let S be Language;

let phi0 be 0wff string of S;

coherence

SubTerms phi0 is (TermSymbolsOf S) * -valued

end;
let phi0 be 0wff string of S;

coherence

SubTerms phi0 is (TermSymbolsOf S) * -valued

proof end;

registration

let S be Language;

coherence

for b_{1} being string of S st b_{1} is 0wff holds

b_{1} is AtomicFormulaSymbolsOf S -valued

end;
coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = OwnSymbolsOf S holds

not b_{1} is empty
;

end;
coherence

for b

not b

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

for phi0 being 0wff string of S st (S -firstChar) . phi0 <> TheEqSymbOf S holds

phi0 is OwnSymbolsOf S -valued

proof end;

registration
end;

definition

let S1, S2 be Language-like ;

end;
attr S2 is S1 -extending means :Def41: :: FOMODEL1:def 41

( the adicity of S1 c= the adicity of S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 );

( the adicity of S1 c= the adicity of S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 );

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

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;

coherence

for b_{1} being Language-like st b_{1} = S null holds

b_{1} is S -extending
;

end;
coherence

for b

b

registration
end;

registration

let S1 be Language;

let S2 be S1 -extending Language;

coherence

for b_{1} being set st b_{1} = (OwnSymbolsOf S1) \ (OwnSymbolsOf S2) holds

b_{1} is empty

end;
let S2 be S1 -extending Language;

coherence

for b

b

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

ex b_{1} being non empty strict Language-like st

( the adicity of b_{1} = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b_{1} = the ZeroF of L & the OneF of b_{1} = the OneF of L )

for b_{1}, b_{2} being non empty strict Language-like st the adicity of b_{1} = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b_{1} = the ZeroF of L & the OneF of b_{1} = the OneF of L & the adicity of b_{2} = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b_{2} = the ZeroF of L & the OneF of b_{2} = the OneF of L holds

b_{1} = b_{2}

end;
let L be non empty Language-like ;

set C = the carrier of L;

set z = the ZeroF of L;

set o = the OneF of L;

set a = the adicity of L;

set X = dom f;

set g = f | ((dom f) \ { the OneF of L});

set a1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L;

set C1 = the carrier of L \/ (dom f);

func L extendWith f -> non empty strict Language-like means :Def42: :: FOMODEL1:def 42

( the adicity of it = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of it = the ZeroF of L & the OneF of it = the OneF of L );

existence ( 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 );

ex b

( the adicity of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def42 defines extendWith FOMODEL1:def 42 :

for f being INT -valued Function

for L being non empty Language-like

for b_{3} being non empty strict Language-like holds

( b_{3} = L extendWith f iff ( the adicity of b_{3} = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b_{3} = the ZeroF of L & the OneF of b_{3} = the OneF of L ) );

for f being INT -valued Function

for L being non empty Language-like

for b

( b

registration

let S be non empty Language-like ;

let f be INT -valued Function;

coherence

for b_{1} being non empty strict Language-like st b_{1} = S extendWith f holds

b_{1} is S -extending

end;
let f be INT -valued Function;

coherence

for b

b

proof end;

registration

let S be non degenerated Language-like ;

coherence

for b_{1} being Language-like st b_{1} is S -extending holds

not b_{1} is degenerated

end;
coherence

for b

not b

proof end;

registration

let S be eligible Language-like ;

coherence

for b_{1} being Language-like st b_{1} is S -extending holds

b_{1} is eligible

end;
coherence

for b

b

proof end;

Lm12: for S1 being non empty Language-like

for f being INT -valued Function holds

( LettersOf (S1 extendWith f) = ((f | ((dom f) \ (AllSymbolsOf S1))) " {0}) \/ (LettersOf S1) & the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = the adicity of S1 | (OwnSymbolsOf S1) )

proof end;

registration

let X be set ;

let m be Integer;

coherence

for b_{1} being Function st b_{1} = X --> m holds

b_{1} is INT -valued

end;
let m be Integer;

coherence

for b

b

proof end;

definition

let S be Language;

let X be functional set ;

S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0) is S -extending Language ;

end;
let X be functional set ;

func S addLettersNotIn X -> S -extending Language equals :: FOMODEL1:def 43

S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0);

coherence S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0);

S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0) is S -extending Language ;

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

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 ;

coherence

for b_{1} being set st b_{1} = (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X) holds

not b_{1} is finite

end;
let X be functional set ;

coherence

for b

not b

proof end;

registration

let S be countable Language;

coherence

for b_{1} being set st b_{1} = AllSymbolsOf S holds

b_{1} is countable
by ORDERS_4:def 2;

end;
coherence

for b

b

registration

let S be countable Language;

coherence

for b_{1} being set st b_{1} = ((AllSymbolsOf S) *) \ {{}} holds

b_{1} is countable

end;
coherence

for b

b

proof end;

registration

let L be non empty Language-like ;

let f be INT -valued Function;

coherence

for b_{1} being set st b_{1} = (AllSymbolsOf (L extendWith f)) \+\ ((dom f) \/ (AllSymbolsOf L)) holds

b_{1} is empty

end;
let f be INT -valued Function;

coherence

for b

b

proof end;

registration

let S be countable Language;

let X be functional set ;

coherence

for b_{1} being 1-sorted st b_{1} = S addLettersNotIn X holds

b_{1} is countable

end;
let X be functional set ;

coherence

for b

b

proof end;

definition
end;

:: deftheorem Def44 defines degenerated FOMODEL1:def 44 :

for S being ZeroOneStr holds

( S is degenerated iff the ZeroF of S = the OneF of S );

for S being ZeroOneStr holds

( S is degenerated iff the ZeroF of S = the OneF of S );

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = AtomicTermsOf S holds

not b_{1} is finite

end;
coherence

for b

not b

proof end;

theorem :: FOMODEL1:18

for X being set

for S2 being Language st X /\ (LettersOf S2) is infinite holds

ex S1 being Language st

( OwnSymbolsOf S1 = X /\ (OwnSymbolsOf S2) & S2 is S1 -extending )

for S2 being Language st X /\ (LettersOf S2) is infinite holds

ex S1 being Language st

( OwnSymbolsOf S1 = X /\ (OwnSymbolsOf S2) & S2 is S1 -extending )

proof end;

definition

let S be Language;

let w1, w2 be string of S;

:: original: ^

redefine func w1 ^ w2 -> string of S;

coherence

w1 ^ w2 is string of S

end;
let w1, w2 be string of S;

:: original: ^

redefine func w1 ^ w2 -> string of S;

coherence

w1 ^ w2 is string of S

proof end;

definition

let S be Language;

let s be Element of S;

:: original: <*

redefine func <*s*> -> string of S;

coherence

<*s*> is string of S

end;
let s be Element of S;

:: original: <*

redefine func <*s*> -> string of S;

coherence

<*s*> is string of S

proof end;

Lm13: for S being Language

for t1, t2 being termal string of S holds (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S

proof end;

registration

let S be Language;

let t1, t2 be termal string of S;

coherence

for b_{1} being string of S st b_{1} = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 holds

b_{1} is 0wff
by Lm13;

end;
let t1, t2 be termal string of S;

coherence

for b

b

::###################### basic definitions ##########################

::#####################################################################

::#####################################################################