:: Free interpretation, quotient interpretation and substitution of a letter with a term for first order languages.
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users


begin

definition
let S be Language;
let s be Element of S;
let V be Element of (((AllSymbolsOf S) *) \ {{}}) * ;
func s -compound V -> string of S equals :: FOMODEL3:def 1
<*s*> ^ ((S -multiCat) . V);
coherence
<*s*> ^ ((S -multiCat) . V) is string of S
proof end;
end;

:: deftheorem defines -compound FOMODEL3:def 1 :
for S being Language
for s being Element of S
for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds s -compound V = <*s*> ^ ((S -multiCat) . V);

registration
let S be Language;
let mm be Element of NAT ;
let s be termal Element of S;
let V be abs (ar s) -element Element of ((S -termsOfMaxDepth) . mm) * ;
cluster s -compound V -> mm + 1 -termal string of S;
coherence
for b1 being string of S st b1 = s -compound V holds
b1 is mm + 1 -termal
proof end;
end;

Lm2: for x being set
for m, n being Nat
for S being Language st not x in (S -termsOfMaxDepth) . (m + n) holds
not x in (S -termsOfMaxDepth) . m
proof end;

Lm5: for x being set
for n being Nat
for S being Language st x in (S -termsOfMaxDepth) . n holds
{ mm where mm is Element of NAT : not x in (S -termsOfMaxDepth) . mm } c= n
proof end;

Lm1: for S being Language
for V being Element of (AllTermsOf S) * ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) *
proof end;

registration
let S be Language;
let s be termal Element of S;
let V be abs (ar s) -element Element of (AllTermsOf S) * ;
cluster s -compound V -> termal string of S;
coherence
for b1 being string of S st b1 = s -compound V holds
b1 is termal
proof end;
end;

registration
let S be Language;
let s be relational Element of S;
let V be abs (ar s) -element Element of (AllTermsOf S) * ;
cluster s -compound V -> 0wff string of S;
coherence
for b1 being string of S st b1 = s -compound V holds
b1 is 0wff
by FOMODEL1:def 35;
end;

definition
let S be Language;
let s be Element of S;
func s -compound -> Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) means :DefCompound1: :: FOMODEL3:def 2
for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds it . V = s -compound V;
existence
ex b1 being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) st
for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b1 . V = s -compound V
proof end;
uniqueness
for b1, b2 being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) st ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b1 . V = s -compound V ) & ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b2 . V = s -compound V ) holds
b1 = b2
proof end;
end;

:: deftheorem DefCompound1 defines -compound FOMODEL3:def 2 :
for S being Language
for s being Element of S
for b3 being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) holds
( b3 = s -compound iff for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b3 . V = s -compound V );

registration
let S be Language;
let s be termal Element of S;
cluster (s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) -> AllTermsOf S -valued ;
coherence
(s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) is AllTermsOf S -valued
proof end;
end;

registration
let S be Language;
let s be relational Element of S;
cluster (s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) -> AtomicFormulasOf S -valued ;
coherence
(s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) is AtomicFormulasOf S -valued
proof end;
end;

definition
let S be Language;
let s be ofAtomicFormula Element of S;
let X be set ;
func X -freeInterpreter s -> set equals :DefFreeInt1: :: FOMODEL3:def 3
(s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) if not s is relational
otherwise ((s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S)));
coherence
( ( not s is relational implies (s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) is set ) & ( s is relational implies ((s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S))) is set ) )
;
consistency
for b1 being set holds verum
;
end;

:: deftheorem DefFreeInt1 defines -freeInterpreter FOMODEL3:def 3 :
for S being Language
for s being ofAtomicFormula Element of S
for X being set holds
( ( not s is relational implies X -freeInterpreter s = (s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) ) & ( s is relational implies X -freeInterpreter s = ((s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S))) ) );

definition
let S be Language;
let s be ofAtomicFormula Element of S;
let X be set ;
:: original: -freeInterpreter
redefine func X -freeInterpreter s -> Interpreter of s, AllTermsOf S;
coherence
X -freeInterpreter s is Interpreter of s, AllTermsOf S
proof end;
end;

definition
let S be Language;
let X be set ;
func (S,X) -freeInterpreter -> Function means :DefFree1: :: FOMODEL3:def 4
( dom it = OwnSymbolsOf S & ( for s being own Element of S holds it . s = X -freeInterpreter s ) );
existence
ex b1 being Function st
( dom b1 = OwnSymbolsOf S & ( for s being own Element of S holds b1 . s = X -freeInterpreter s ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = OwnSymbolsOf S & ( for s being own Element of S holds b1 . s = X -freeInterpreter s ) & dom b2 = OwnSymbolsOf S & ( for s being own Element of S holds b2 . s = X -freeInterpreter s ) holds
b1 = b2
proof end;
end;

:: deftheorem DefFree1 defines -freeInterpreter FOMODEL3:def 4 :
for S being Language
for X being set
for b3 being Function holds
( b3 = (S,X) -freeInterpreter iff ( dom b3 = OwnSymbolsOf S & ( for s being own Element of S holds b3 . s = X -freeInterpreter s ) ) );

registration
let S be Language;
let X be set ;
cluster (S,X) -freeInterpreter -> Function-yielding Function;
coherence
for b1 being Function st b1 = (S,X) -freeInterpreter holds
b1 is Function-yielding
proof end;
end;

definition
let S be Language;
let X be set ;
:: original: -freeInterpreter
redefine func (S,X) -freeInterpreter -> Interpreter of S, AllTermsOf S;
coherence
(S,X) -freeInterpreter is Interpreter of S, AllTermsOf S
proof end;
end;

registration
let S be Language;
let X be set ;
cluster (S,X) -freeInterpreter -> S, AllTermsOf S -interpreter-like Function;
coherence
for b1 being Function st b1 = (S,X) -freeInterpreter holds
b1 is S, AllTermsOf S -interpreter-like
by FOMODEL2:def 4;
end;

definition
let S be Language;
let X be set ;
:: original: -freeInterpreter
redefine func (S,X) -freeInterpreter -> Element of (AllTermsOf S) -InterpretersOf S;
coherence
(S,X) -freeInterpreter is Element of (AllTermsOf S) -InterpretersOf S
proof end;
end;

definition
let X, Y be non empty set ;
let R be Relation of X,Y;
let n be Nat;
func n -placesOf R -> Relation of (n -tuples_on X),(n -tuples_on Y) equals :: FOMODEL3:def 5
{ [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R
}
;
coherence
{ [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R
}
is Relation of (n -tuples_on X),(n -tuples_on Y)
proof end;
end;

:: deftheorem defines -placesOf FOMODEL3:def 5 :
for X, Y being non empty set
for R being Relation of X,Y
for n being Nat holds n -placesOf R = { [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R
}
;

Lm7: for n being zero Nat
for X, Y being non empty set
for R being Relation of X,Y holds n -placesOf R = {[{},{}]}
proof end;

registration
let X, Y be non empty set ;
let R be total Relation of X,Y;
let n be non zero Nat;
cluster n -placesOf R -> total Relation of (n -tuples_on X),(n -tuples_on Y);
coherence
for b1 being Relation of (n -tuples_on X),(n -tuples_on Y) st b1 = n -placesOf R holds
b1 is total
proof end;
end;

registration
let X, Y be non empty set ;
let R be total Relation of X,Y;
let n be Nat;
cluster n -placesOf R -> total Relation of (n -tuples_on X),(n -tuples_on Y);
coherence
for b1 being Relation of (n -tuples_on X),(n -tuples_on Y) st b1 = n -placesOf R holds
b1 is total
proof end;
end;

registration
let X, Y be non empty set ;
let R be Relation of X,Y;
let n be zero Nat;
cluster n -placesOf R -> Function-like Relation of (n -tuples_on X),(n -tuples_on Y);
coherence
for b1 being Relation of (n -tuples_on X),(n -tuples_on Y) st b1 = n -placesOf R holds
b1 is Function-like
proof end;
end;

definition
let X be non empty set ;
let R be Relation of X;
let n be Nat;
func n -placesOf R -> Relation of (n -tuples_on X) equals :: FOMODEL3:def 6
n -placesOf R;
coherence
n -placesOf R is Relation of (n -tuples_on X)
;
end;

:: deftheorem defines -placesOf FOMODEL3:def 6 :
for X being non empty set
for R being Relation of X
for n being Nat holds n -placesOf R = n -placesOf R;

definition
let X be non empty set ;
let R be Relation of X;
let n be zero Nat;
:: original: -placesOf
redefine func n -placesOf R -> Relation of (n -tuples_on X) equals :: FOMODEL3:def 7
{[{},{}]};
coherence
n -placesOf R is Relation of (n -tuples_on X)
;
compatibility
for b1 being Relation of (n -tuples_on X) holds
( b1 = n -placesOf R iff b1 = {[{},{}]} )
by Lm7;
end;

:: deftheorem defines -placesOf FOMODEL3:def 7 :
for X being non empty set
for R being Relation of X
for n being zero Nat holds n -placesOf R = {[{},{}]};

Lm9: for n being non zero Nat
for X being non empty set
for x, y being Element of Funcs ((Seg n),X)
for R being Relation of X holds
( [x,y] in n -placesOf R iff for j being Element of Seg n holds [(x . j),(y . j)] in R )
proof end;

Lm16: for n being non zero Nat
for X being non empty set
for r being total symmetric Relation of X holds n -placesOf r is total symmetric Relation of (n -tuples_on X)
proof end;

Lm17: for n being non zero Nat
for X being non empty set
for r being total transitive Relation of X holds n -placesOf r is total transitive Relation of (n -tuples_on X)
proof end;

Lm13: for n being zero Nat
for X being non empty set
for r being Relation of X holds n -placesOf r is total symmetric transitive Relation of (n -tuples_on X)
proof end;

registration
let X be non empty set ;
let R be total symmetric Relation of X;
let n be Nat;
cluster n -placesOf R -> total Relation of (n -tuples_on X);
coherence
for b1 being Relation of (n -tuples_on X) st b1 = n -placesOf R holds
b1 is total
;
end;

registration
let X be non empty set ;
let R be total symmetric Relation of X;
let n be Nat;
cluster n -placesOf R -> symmetric Relation of (n -tuples_on X);
coherence
for b1 being Relation of (n -tuples_on X) st b1 = n -placesOf R holds
b1 is symmetric
proof end;
end;

registration
let X be non empty set ;
let R be total symmetric Relation of X;
let n be Nat;
cluster n -placesOf R -> total symmetric Relation of (n -tuples_on X);
coherence
for b1 being Relation of (n -tuples_on X) st b1 = n -placesOf R holds
( b1 is symmetric & b1 is total )
;
end;

registration
let X be non empty set ;
let R be total transitive Relation of X;
let n be Nat;
cluster n -placesOf R -> total transitive Relation of (n -tuples_on X);
coherence
for b1 being Relation of (n -tuples_on X) st b1 = n -placesOf R holds
( b1 is transitive & b1 is total )
proof end;
end;

registration
let X be non empty set ;
let R be Equivalence_Relation of X;
let n be Nat;
cluster n -placesOf R -> total symmetric transitive Relation of (n -tuples_on X);
coherence
for b1 being Relation of (n -tuples_on X) st b1 = n -placesOf R holds
( b1 is total & b1 is symmetric & b1 is transitive )
;
end;

definition
let X, Y be non empty set ;
let E be Equivalence_Relation of X;
let F be Equivalence_Relation of Y;
let R be Relation;
func R quotient (E,F) -> set equals :: FOMODEL3:def 8
{ [e,f] where e is Element of Class E, f is Element of Class F : ex x, y being set st
( x in e & y in f & [x,y] in R )
}
;
coherence
{ [e,f] where e is Element of Class E, f is Element of Class F : ex x, y being set st
( x in e & y in f & [x,y] in R )
}
is set
;
end;

:: deftheorem defines quotient FOMODEL3:def 8 :
for X, Y being non empty set
for E being Equivalence_Relation of X
for F being Equivalence_Relation of Y
for R being Relation holds R quotient (E,F) = { [e,f] where e is Element of Class E, f is Element of Class F : ex x, y being set st
( x in e & y in f & [x,y] in R )
}
;

definition
let X, Y be non empty set ;
let E be Equivalence_Relation of X;
let F be Equivalence_Relation of Y;
let R be Relation;
:: original: quotient
redefine func R quotient (E,F) -> Relation of (Class E),(Class F);
coherence
R quotient (E,F) is Relation of (Class E),(Class F)
proof end;
end;

definition
let E, F be Relation;
let f be Function;
attr f is E,F -respecting means :DefCompatible: :: FOMODEL3:def 9
for x1, x2 being set st [x1,x2] in E holds
[(f . x1),(f . x2)] in F;
end;

:: deftheorem DefCompatible defines -respecting FOMODEL3:def 9 :
for E, F being Relation
for f being Function holds
( f is E,F -respecting iff for x1, x2 being set st [x1,x2] in E holds
[(f . x1),(f . x2)] in F );

definition
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
let E be Relation of U;
let f be Interpreter of s,U;
attr f is E -respecting means :DefCompatible2: :: FOMODEL3:def 10
f is (abs (ar s)) -placesOf E,E -respecting if not s is relational
otherwise f is (abs (ar s)) -placesOf E, id BOOLEAN -respecting ;
consistency
verum
;
end;

:: deftheorem DefCompatible2 defines -respecting FOMODEL3:def 10 :
for S being Language
for U being non empty set
for s being ofAtomicFormula Element of S
for E being Relation of U
for f being Interpreter of s,U holds
( ( not s is relational implies ( f is E -respecting iff f is (abs (ar s)) -placesOf E,E -respecting ) ) & ( s is relational implies ( f is E -respecting iff f is (abs (ar s)) -placesOf E, id BOOLEAN -respecting ) ) );

registration
let X, Y be non empty set ;
let E be Equivalence_Relation of X;
let F be Equivalence_Relation of Y;
cluster non empty Relation-like X -defined Y -valued Function-like total quasi_total E,F -respecting Element of bool [:X,Y:];
existence
ex b1 being Function of X,Y st b1 is E,F -respecting
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
let E be Equivalence_Relation of U;
cluster non empty Relation-like (abs (ar s)) -tuples_on U -defined U \/ BOOLEAN -valued Function-like total quasi_total E -respecting Interpreter of s,U;
existence
ex b1 being Interpreter of s,U st b1 is E -respecting
proof end;
end;

registration
let X, Y be non empty set ;
let E be Equivalence_Relation of X;
let F be Equivalence_Relation of Y;
cluster Relation-like Function-like E,F -respecting set ;
existence
ex b1 being Function st b1 is E,F -respecting
proof end;
end;

definition
let X be non empty set ;
let E be Equivalence_Relation of X;
let n be Nat;
:: original: -placesOf
redefine func n -placesOf E -> Equivalence_Relation of (n -tuples_on X);
coherence
n -placesOf E is Equivalence_Relation of (n -tuples_on X)
;
end;

definition
let X be non empty set ;
let x be Element of SmallestPartition X;
func DeTrivial x -> Element of X means :DefDetriv: :: FOMODEL3:def 11
x = {it};
existence
ex b1 being Element of X st x = {b1}
proof end;
uniqueness
for b1, b2 being Element of X st x = {b1} & x = {b2} holds
b1 = b2
by ZFMISC_1:6;
end;

:: deftheorem DefDetriv defines DeTrivial FOMODEL3:def 11 :
for X being non empty set
for x being Element of SmallestPartition X
for b3 being Element of X holds
( b3 = DeTrivial x iff x = {b3} );

definition
let X be non empty set ;
func peeler X -> Function of {_{X}_},X means :DefPeel: :: FOMODEL3:def 12
for x being Element of {_{X}_} holds it . x = DeTrivial x;
existence
ex b1 being Function of {_{X}_},X st
for x being Element of {_{X}_} holds b1 . x = DeTrivial x
proof end;
uniqueness
for b1, b2 being Function of {_{X}_},X st ( for x being Element of {_{X}_} holds b1 . x = DeTrivial x ) & ( for x being Element of {_{X}_} holds b2 . x = DeTrivial x ) holds
b1 = b2
proof end;
end;

:: deftheorem DefPeel defines peeler FOMODEL3:def 12 :
for X being non empty set
for b2 being Function of {_{X}_},X holds
( b2 = peeler X iff for x being Element of {_{X}_} holds b2 . x = DeTrivial x );

registration
let X be non empty set ;
let EqR be Equivalence_Relation of X;
cluster -> non empty Element of Class EqR;
coherence
for b1 being Element of Class EqR holds not b1 is empty
;
end;

Lm3: for X being non empty set
for E being Equivalence_Relation of X
for x, y being set
for C being Element of Class E st x in C & y in C holds
[x,y] in E
proof end;

Lm10: for X being non empty set
for E being Equivalence_Relation of X
for C1, C2 being Element of Class E
for x1, x2 being set st x1 in C1 & x2 in C2 & [x1,x2] in E holds
C1 = C2
proof end;

registration
let X, Y be non empty set ;
let E be Equivalence_Relation of X;
let F be Equivalence_Relation of Y;
let f be E,F -respecting Function;
cluster f quotient (E,F) -> Function-like Relation;
coherence
for b1 being Relation st b1 = f quotient (E,F) holds
b1 is Function-like
proof end;
end;

registration
let X, Y be non empty set ;
let E be Equivalence_Relation of X;
let F be Equivalence_Relation of Y;
let R be total Relation of X,Y;
cluster R quotient (E,F) -> total Relation of (Class E),(Class F);
coherence
for b1 being Relation of (Class E),(Class F) st b1 = R quotient (E,F) holds
b1 is total
proof end;
end;

definition
let X, Y be non empty set ;
let E be Equivalence_Relation of X;
let F be Equivalence_Relation of Y;
let f be E,F -respecting Function of X,Y;
:: original: quotient
redefine func f quotient (E,F) -> Function of (Class E),(Class F);
coherence
f quotient (E,F) is Function of (Class E),(Class F)
proof end;
end;

definition
let X be non empty set ;
let E be Equivalence_Relation of X;
func E -class -> Function of X,(Class E) means :DefClass: :: FOMODEL3:def 13
for x being Element of X holds it . x = EqClass (E,x);
existence
ex b1 being Function of X,(Class E) st
for x being Element of X holds b1 . x = EqClass (E,x)
proof end;
uniqueness
for b1, b2 being Function of X,(Class E) st ( for x being Element of X holds b1 . x = EqClass (E,x) ) & ( for x being Element of X holds b2 . x = EqClass (E,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefClass defines -class FOMODEL3:def 13 :
for X being non empty set
for E being Equivalence_Relation of X
for b3 being Function of X,(Class E) holds
( b3 = E -class iff for x being Element of X holds b3 . x = EqClass (E,x) );

registration
let X be non empty set ;
let E be Equivalence_Relation of X;
cluster E -class -> onto Function of X,(Class E);
coherence
for b1 being Function of X,(Class E) st b1 = E -class holds
b1 is onto
proof end;
end;

registration
let X, Y be non empty set ;
cluster Relation-like X -defined Y -valued onto Element of bool [:X,Y:];
existence
ex b1 being Relation of X,Y st b1 is onto
proof end;
end;

registration
let Y be non empty set ;
cluster Relation-like Y -valued onto set ;
existence
ex b1 being Y -valued Relation st b1 is onto
proof end;
end;

registration
let Y be non empty set ;
let R be Y -valued Relation;
cluster R ~ -> Y -defined Relation;
coherence
for b1 being Relation st b1 = R ~ holds
b1 is Y -defined
proof end;
end;

registration
let Y be non empty set ;
let R be Y -valued onto Relation;
cluster R ~ -> Y -defined total Y -defined Relation;
coherence
for b1 being Y -defined Relation st b1 = R ~ holds
b1 is total
proof end;
end;

registration
let X, Y be non empty set ;
let R be onto Relation of X,Y;
cluster R ~ -> total Relation of Y,X;
coherence
for b1 being Relation of Y,X st b1 = R ~ holds
b1 is total
;
end;

registration
let Y be non empty set ;
let R be Y -valued onto Relation;
cluster R ~ -> Y -defined total Y -defined Relation;
coherence
for b1 being Y -defined Relation st b1 = R ~ holds
b1 is total
;
end;

Lm8: for U being non empty set
for E being Equivalence_Relation of U
for n being non zero Nat holds (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Function-like
proof end;

definition
let U be non empty set ;
let n be Nat;
let E be Equivalence_Relation of U;
func n -tuple2Class E -> Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) equals :: FOMODEL3:def 14
(n -placesOf ((E -class) ~)) * ((n -placesOf E) -class);
coherence
(n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Relation of (n -tuples_on (Class E)),(Class (n -placesOf E))
;
end;

:: deftheorem defines -tuple2Class FOMODEL3:def 14 :
for U being non empty set
for n being Nat
for E being Equivalence_Relation of U holds n -tuple2Class E = (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class);

registration
let U be non empty set ;
let n be Nat;
let E be Equivalence_Relation of U;
cluster n -tuple2Class E -> Function-like Relation of (n -tuples_on (Class E)),(Class (n -placesOf E));
coherence
for b1 being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b1 = n -tuple2Class E holds
b1 is Function-like
proof end;
end;

registration
let U be non empty set ;
let n be Nat;
let E be Equivalence_Relation of U;
cluster n -tuple2Class E -> total Relation of (n -tuples_on (Class E)),(Class (n -placesOf E));
coherence
for b1 being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b1 = n -tuple2Class E holds
b1 is total
;
end;

definition
let U be non empty set ;
let n be Nat;
let E be Equivalence_Relation of U;
:: original: -tuple2Class
redefine func n -tuple2Class E -> Function of (n -tuples_on (Class E)),(Class (n -placesOf E));
coherence
n -tuple2Class E is Function of (n -tuples_on (Class E)),(Class (n -placesOf E))
;
end;

definition
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
let E be Equivalence_Relation of U;
let f be Interpreter of s,U;
func f quotient E -> set equals :DefQuot2: :: FOMODEL3:def 15
((abs (ar s)) -tuple2Class E) * (f quotient (((abs (ar s)) -placesOf E),E)) if not s is relational
otherwise (((abs (ar s)) -tuple2Class E) * (f quotient (((abs (ar s)) -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN);
coherence
( ( not s is relational implies ((abs (ar s)) -tuple2Class E) * (f quotient (((abs (ar s)) -placesOf E),E)) is set ) & ( s is relational implies (((abs (ar s)) -tuple2Class E) * (f quotient (((abs (ar s)) -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN) is set ) )
;
consistency
for b1 being set holds verum
;
end;

:: deftheorem DefQuot2 defines quotient FOMODEL3:def 15 :
for S being Language
for U being non empty set
for s being ofAtomicFormula Element of S
for E being Equivalence_Relation of U
for f being Interpreter of s,U holds
( ( not s is relational implies f quotient E = ((abs (ar s)) -tuple2Class E) * (f quotient (((abs (ar s)) -placesOf E),E)) ) & ( s is relational implies f quotient E = (((abs (ar s)) -tuple2Class E) * (f quotient (((abs (ar s)) -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN) ) );

definition
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
let E be Equivalence_Relation of U;
let f be E -respecting Interpreter of s,U;
:: original: quotient
redefine func f quotient E -> Interpreter of s, Class E;
coherence
f quotient E is Interpreter of s, Class E
proof end;
end;

theorem :: FOMODEL3:1
for X being non empty set
for E being Equivalence_Relation of X
for C1, C2 being Element of Class E st C1 meets C2 holds
C1 = C2 by EQREL_1:def 6;

registration
let S be Language;
cluster -> own Element of OwnSymbolsOf S;
coherence
for b1 being Element of OwnSymbolsOf S holds b1 is own
by FOMODEL1:def 19;
cluster -> ofAtomicFormula Element of OwnSymbolsOf S;
coherence
for b1 being Element of OwnSymbolsOf S holds b1 is ofAtomicFormula
;
end;

registration
let S be Language;
let U be non empty set ;
let o be non relational ofAtomicFormula Element of S;
let E be Relation of U;
cluster E -respecting -> (abs (ar o)) -placesOf E,E -respecting Interpreter of o,U;
coherence
for b1 being Interpreter of o,U st b1 is E -respecting holds
b1 is (abs (ar o)) -placesOf E,E -respecting
by DefCompatible2;
end;

registration
let S be Language;
let U be non empty set ;
let r be relational Element of S;
let E be Relation of U;
cluster E -respecting -> (abs (ar r)) -placesOf E, id BOOLEAN -respecting Interpreter of r,U;
coherence
for b1 being Interpreter of r,U st b1 is E -respecting holds
b1 is (abs (ar r)) -placesOf E, id BOOLEAN -respecting
by DefCompatible2;
end;

registration
let n be Nat;
let U1, U2 be non empty set ;
let f be Function-like Relation of U1,U2;
cluster n -placesOf f -> Function-like Relation;
coherence
for b1 being Relation st b1 = n -placesOf f holds
b1 is Function-like
proof end;
end;

registration
let U1, U2 be non empty set ;
let n be zero Nat;
let R be Relation of U1,U2;
cluster (n -placesOf R) \+\ (id {{}}) -> empty ;
coherence
(n -placesOf R) \+\ (id {{}}) is empty
proof end;
end;

registration
let X be set ;
let Y be functional set ;
cluster X /\ Y -> functional ;
coherence
X /\ Y is functional
;
end;

theorem :: FOMODEL3:2
for S being Language
for V being Element of (AllTermsOf S) * ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) * by Lm1;

definition
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
let I be S,U -interpreter-like Function;
attr I is E -respecting means :DefCompatible3: :: FOMODEL3:def 16
for s being own Element of S holds I . s is E -respecting ;
end;

:: deftheorem DefCompatible3 defines -respecting FOMODEL3:def 16 :
for S being Language
for U being non empty set
for E being Equivalence_Relation of U
for I being b1,b2 -interpreter-like Function holds
( I is E -respecting iff for s being own Element of S holds I . s is E -respecting );

definition
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
let I be S,U -interpreter-like Function;
func I quotient E -> Function means :DefQuot3: :: FOMODEL3:def 17
( dom it = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds it . o = (I . o) quotient E ) );
existence
ex b1 being Function st
( dom b1 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b1 . o = (I . o) quotient E ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b1 . o = (I . o) quotient E ) & dom b2 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b2 . o = (I . o) quotient E ) holds
b1 = b2
proof end;
end;

:: deftheorem DefQuot3 defines quotient FOMODEL3:def 17 :
for S being Language
for U being non empty set
for E being Equivalence_Relation of U
for I being b1,b2 -interpreter-like Function
for b5 being Function holds
( b5 = I quotient E iff ( dom b5 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b5 . o = (I . o) quotient E ) ) );

definition
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
let I be S,U -interpreter-like Function;
redefine func I quotient E means :DefQuot3b: :: FOMODEL3:def 18
( dom it = OwnSymbolsOf S & ( for o being own Element of S holds it . o = (I . o) quotient E ) );
compatibility
for b1 being Function holds
( b1 = I quotient E iff ( dom b1 = OwnSymbolsOf S & ( for o being own Element of S holds b1 . o = (I . o) quotient E ) ) )
proof end;
end;

:: deftheorem DefQuot3b defines quotient FOMODEL3:def 18 :
for S being Language
for U being non empty set
for E being Equivalence_Relation of U
for I being b1,b2 -interpreter-like Function
for b5 being Function holds
( b5 = I quotient E iff ( dom b5 = OwnSymbolsOf S & ( for o being own Element of S holds b5 . o = (I . o) quotient E ) ) );

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let E be Equivalence_Relation of U;
cluster I quotient E -> OwnSymbolsOf S -defined ;
coherence
I quotient E is OwnSymbolsOf S -defined
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
cluster Relation-like OwnSymbolsOf S -defined Function-like total Function-yielding S,U -interpreter-like E -respecting Element of U -InterpretersOf S;
existence
ex b1 being Element of U -InterpretersOf S st b1 is E -respecting
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
cluster Relation-like Function-like Function-yielding S,U -interpreter-like E -respecting set ;
existence
ex b1 being S,U -interpreter-like Function st b1 is E -respecting
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
let o be own Element of S;
let I be S,U -interpreter-like E -respecting Function;
cluster I . o -> E -respecting Interpreter of o,U;
coherence
for b1 being Interpreter of o,U st b1 = I . o holds
b1 is E -respecting
by DefCompatible3;
end;

registration
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
let I be S,U -interpreter-like E -respecting Function;
cluster I quotient E -> S, Class E -interpreter-like Function;
coherence
for b1 being Function st b1 = I quotient E holds
b1 is S, Class E -interpreter-like
proof end;
end;

definition
let S be Language;
let U be non empty set ;
let E be Equivalence_Relation of U;
let I be S,U -interpreter-like E -respecting Function;
:: original: quotient
redefine func I quotient E -> Element of (Class E) -InterpretersOf S;
coherence
I quotient E is Element of (Class E) -InterpretersOf S
proof end;
end;

Lm6: for U1, U2 being non empty set
for n being Nat
for R being Relation of U1,U2 holds n -placesOf R = { [p,q] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : q c= p * R }
proof end;

Lm12: for U2, U1, U3 being non empty set
for n being Nat
for U being non empty Subset of U2
for P being Relation of U1,U
for Q being Relation of U2,U3 holds (n -placesOf P) * (n -placesOf Q) c= n -placesOf (P * Q)
proof end;

Lm18: for U2, U1, U3 being non empty set
for n being Nat
for U being non empty Subset of U2
for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) c= (n -placesOf P) * (n -placesOf Q)
proof end;

Lm14: for U2, U1, U3 being non empty set
for n being Nat
for U being non empty Subset of U2
for P being Relation of U1,U
for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
proof end;

Lm20: for U1, U2, U3 being non empty set
for n being Nat
for P being Relation of U1,U2
for Q being Relation of U2,U3 holds n -placesOf (P * Q) = (n -placesOf P) * (n -placesOf Q)
proof end;

Lm19: for U1, U2 being non empty set
for n being Nat
for R being Relation of U1,U2 holds n -placesOf (R ~) = (n -placesOf R) ~
proof end;

Lm27: for X, Y being non empty set
for E being Equivalence_Relation of X
for F being Equivalence_Relation of Y
for g being b3,b4 -respecting Function of X,Y holds (F -class) * g = (g quotient (E,F)) * (E -class)
proof end;

Lm22: for U1, U2 being non empty set
for m being Nat
for p being b1 -valued b3 -element FinSequence
for f being Function of U1,U2 holds f * p = (m -placesOf f) . p
proof end;

Lm23: for U being non empty set
for n being Nat
for E being Equivalence_Relation of U holds (n -placesOf E) -class = (n -tuple2Class E) * (n -placesOf (E -class))
proof end;

Lm24: for U1, U2 being non empty set
for n being Nat
for E being Equivalence_Relation of U1
for F being Equivalence_Relation of U2
for g being b3 -placesOf b4,b5 -respecting Function of (n -tuples_on U1),U2 holds (g quotient ((n -placesOf E),F)) * (n -tuple2Class E) = (n -placesOf ((E -class) ~)) * ((F -class) * g)
proof end;

Lm25: for x being set
for U being non empty set
for f being Function
for R being total reflexive Relation of U st x in dom f & f is U -valued holds
f is id {x},R -respecting
proof end;

Lm26: for U being non empty set holds (peeler U) * ((id U) -class) = id U
proof end;

Lm21: for U being non empty set
for u being Element of U
for k being Nat
for S being Language
for E being Equivalence_Relation of U
for I being b4,b1 -interpreter-like b5 -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
proof end;

Lm32: for U being non empty set
for S being Language
for E being Equivalence_Relation of U
for I being b2,b1 -interpreter-like b3 -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval)
proof end;

Lm28: for U1 being non empty set
for S being Language
for R being Equivalence_Relation of U1
for phi being 0wff string of S
for i being b2,b1 -interpreter-like b3 -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi
proof end;

Lm31: for X being set
for m being Nat
for S being Language
for tt being Element of AllTermsOf S
for t being 0 -termal string of S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t = t
proof end;

Lm30: for X being set
for m being Nat
for S being Language
for tt being Element of AllTermsOf S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = id ((S -termsOfMaxDepth) . m)
proof end;

Lm29: for X being set
for S being Language holds ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)
proof end;

Lm33: for U1, U2 being non empty set
for R being Relation of U1,U2 holds 0 -placesOf R = id {{}}
proof end;

theorem :: FOMODEL3:3
for U being non empty set
for S being Language
for E being Equivalence_Relation of U
for I being b2,b1 -interpreter-like b3 -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval) by Lm32;

theorem :: FOMODEL3:4
for X being set
for S being Language holds ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S) by Lm29;

theorem :: FOMODEL3:5
for U1 being non empty set
for S being Language
for R being Equivalence_Relation of U1
for phi being 0wff string of S
for i being b2,b1 -interpreter-like b3 -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi by Lm28;

Lm35: for m being Nat
for S being Language
for l1, l2 being literal Element of S holds (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) is Function of ((S -termsOfMaxDepth) . m),((S -termsOfMaxDepth) . m)
proof end;

definition
let S be Language;
let x be set ;
let s be Element of S;
let w be string of S;
:: original: -SymbolSubstIn
redefine func (x,s) -SymbolSubstIn w -> string of S;
coherence
(x,s) -SymbolSubstIn w is string of S
proof end;
end;

registration
let S be Language;
let l1, l2 be literal Element of S;
let m be Nat;
let t be m -termal string of S;
cluster (l1,l2) -SymbolSubstIn t -> m -termal string of S;
coherence
for b1 being string of S st b1 = (l1,l2) -SymbolSubstIn t holds
b1 is m -termal
proof end;
end;

registration
let S be Language;
let t be termal string of S;
let l1, l2 be literal Element of S;
cluster (l1,l2) -SymbolSubstIn t -> termal string of S;
coherence
for b1 being string of S st b1 = (l1,l2) -SymbolSubstIn t holds
b1 is termal
proof end;
end;

Lm36: for S being Language
for l1, l2 being literal Element of S holds (l1 SubstWith l2) | (AllTermsOf S) is Function of (AllTermsOf S),(AllTermsOf S)
proof end;

registration
let S be Language;
let l1, l2 be literal Element of S;
let phi be 0wff string of S;
cluster (l1,l2) -SymbolSubstIn phi -> 0wff string of S;
coherence
for b1 being string of S st b1 = (l1,l2) -SymbolSubstIn phi holds
b1 is 0wff
proof end;
end;

registration
let S be Language;
let m0 be zero number ;
let phi be m0 -wff string of S;
cluster Depth phi -> zero number ;
coherence
for b1 being number st b1 = Depth phi holds
b1 is empty
by FOMODEL2:def 31;
end;

Lm37: for S being Language
for l1, l2 being literal Element of S
for psi1 being wff string of S ex psi2 being wff string of S st
( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )
proof end;

definition
let S be Language;
let m be Nat;
let w be string of S;
:: original: null
redefine func w null m -> string of S;
coherence
w null m is string of S
;
end;

registration
let S be Language;
let phi be wff string of S;
let m be Nat;
cluster phi null m -> (Depth phi) + m -wff string of S;
coherence
for b1 being string of S st b1 = phi null m holds
b1 is (Depth phi) + m -wff
proof end;
end;

registration
let S be Language;
let m be Nat;
let phi be m -wff string of S;
cluster m - (Depth phi) -> ext-real non negative ext-real number ;
coherence
for b1 being ext-real number st b1 = m - (Depth phi) holds
not b1 is negative
proof end;
end;

registration
let S be Language;
let l1, l2 be literal Element of S;
let m be Nat;
let phi be m -wff string of S;
cluster (l1,l2) -SymbolSubstIn phi -> m -wff string of S;
coherence
for b1 being string of S st b1 = (l1,l2) -SymbolSubstIn phi holds
b1 is m -wff
proof end;
end;

registration
let S be Language;
let l1, l2 be literal Element of S;
let phi be wff string of S;
cluster (l1,l2) -SymbolSubstIn phi -> wff string of S;
coherence
for b1 being string of S st b1 = (l1,l2) -SymbolSubstIn phi holds
b1 is wff
proof end;
end;

Lm39: for S being Language
for l1, l2 being literal Element of S
for psi1 being wff string of S holds Depth psi1 = Depth ((l1,l2) -SymbolSubstIn psi1)
proof end;

registration
let S be Language;
let l1, l2 be literal Element of S;
let phi be wff string of S;
cluster (Depth ((l1,l2) -SymbolSubstIn phi)) \+\ (Depth phi) -> empty set ;
coherence
for b1 being set st b1 = (Depth ((l1,l2) -SymbolSubstIn phi)) \+\ (Depth phi) holds
b1 is empty
proof end;
end;

theorem :: FOMODEL3:6
for X being set
for S being Language
for a being ofAtomicFormula Element of S
for T being abs (ar b3) -element Element of (AllTermsOf S) * holds
( ( not a is relational implies (X -freeInterpreter a) . T = a -compound T ) & ( a is relational implies (X -freeInterpreter a) . T = (chi (X,(AtomicFormulasOf S))) . (a -compound T) ) )
proof end;

registration
let S be Language;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like finite-support termal Element of ((AllSymbolsOf S) *) \ {{}};
existence
ex b1 being string of S st b1 is termal
proof end;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like finite-support 0wff Element of ((AllSymbolsOf S) *) \ {{}};
existence
ex b1 being string of S st b1 is 0wff
proof end;
end;

theorem Th7: :: FOMODEL3:7
for X being set
for U being non empty set
for n being Nat
for S being Language
for l being literal Element of S
for I being b4,b2 -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
proof end;

definition
let S be Language;
let l be literal Element of S;
let tt be Element of AllTermsOf S;
let phi0 be 0wff string of S;
func (l,tt) AtomicSubst phi0 -> FinSequence equals :: FOMODEL3:def 19
<*((S -firstChar) . phi0)*> ^ ((S -multiCat) . ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0)));
coherence
<*((S -firstChar) . phi0)*> ^ ((S -multiCat) . ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0))) is FinSequence
;
end;

:: deftheorem defines AtomicSubst FOMODEL3:def 19 :
for S being Language
for l being literal Element of S
for tt being Element of AllTermsOf S
for phi0 being 0wff string of S holds (l,tt) AtomicSubst phi0 = <*((S -firstChar) . phi0)*> ^ ((S -multiCat) . ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0)));

Lm38: for S being Language
for l being literal Element of S
for phi0 being 0wff string of S
for tt being Element of AllTermsOf S holds (l,tt) AtomicSubst phi0 is 0wff string of S
proof end;

definition
let S be Language;
let l be literal Element of S;
let tt be Element of AllTermsOf S;
let phi0 be 0wff string of S;
:: original: AtomicSubst
redefine func (l,tt) AtomicSubst phi0 -> string of S;
coherence
(l,tt) AtomicSubst phi0 is string of S
by Lm38;
end;

registration
let S be Language;
let l be literal Element of S;
let tt be Element of AllTermsOf S;
let phi0 be 0wff string of S;
cluster (l,tt) AtomicSubst phi0 -> 0wff string of S;
coherence
for b1 being string of S st b1 = (l,tt) AtomicSubst phi0 holds
b1 is 0wff
by Lm38;
end;

Lm42: for S being Language
for l being literal Element of S
for phi0 being 0wff string of S
for tt being Element of AllTermsOf S holds
( (S -firstChar) . ((l,tt) AtomicSubst phi0) = (S -firstChar) . phi0 & SubTerms ((l,tt) AtomicSubst phi0) = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0) )
proof end;

Lm43: for X being set
for U being non empty set
for S being Language
for l being literal Element of S
for I being b3,b2 -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
proof end;

theorem Th8: :: FOMODEL3:8
for U being non empty set
for S being Language
for l being literal Element of S
for phi0 being 0wff string of S
for I being b2,b1 -interpreter-like Function
for tt being Element of AllTermsOf S holds I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0
proof end;

registration
let S be Language;
let l1, l2 be literal Element of S;
let m be Nat;
cluster (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) -> (S -termsOfMaxDepth) . m -valued Relation;
coherence
for b1 being Relation st b1 = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) holds
b1 is (S -termsOfMaxDepth) . m -valued
proof end;
end;

registration
let S be Language;
let l1, l2 be literal Element of S;
cluster (l1 SubstWith l2) | (AllTermsOf S) -> AllTermsOf S -valued Relation;
coherence
for b1 being Relation st b1 = (l1 SubstWith l2) | (AllTermsOf S) holds
b1 is AllTermsOf S -valued
proof end;
end;

Lm40: for S being Language
for l1, l2 being literal Element of S
for t being termal string of S holds SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t)
proof end;

Lm41: for S being Language
for l1, l2 being literal Element of S
for phi0 being 0wff string of S holds SubTerms ((l1,l2) -SymbolSubstIn phi0) = (l1 SubstWith l2) * (SubTerms phi0)
proof end;

Lm44: for U being non empty set
for u being Element of U
for m being Nat
for S being Language
for l1, l2 being literal Element of S
for I being b4,b1 -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
proof end;

Lm45: for U being non empty set
for u being Element of U
for S being Language
for l2, l1 being literal Element of S
for phi0 being 0wff string of S
for I being b3,b1 -interpreter-like Function st phi0 is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
proof end;

theorem Th9: :: FOMODEL3:9
for U being non empty set
for u1 being Element of U
for S being Language
for l2, l1 being literal Element of S
for psi being wff string of S st not l2 in rng psi holds
for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
proof end;

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let n be Nat;
let f be FinSequence-yielding Function;
let phi be wff string of S;
func (l,t,n,f) Subst2 phi -> FinSequence equals :DefSubst2: :: FOMODEL3:def 20
(<*(TheNorSymbOf S)*> ^ (f . (head phi))) ^ (f . (tail phi)) if ( Depth phi = n + 1 & not phi is exal )
<* the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})*> ^ (f . ((((S -firstChar) . phi), the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})) -SymbolSubstIn (head phi))) if ( Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l )
otherwise f . phi;
coherence
( ( Depth phi = n + 1 & not phi is exal implies (<*(TheNorSymbOf S)*> ^ (f . (head phi))) ^ (f . (tail phi)) is FinSequence ) & ( Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l implies <* the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})*> ^ (f . ((((S -firstChar) . phi), the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})) -SymbolSubstIn (head phi))) is FinSequence ) & ( ( not Depth phi = n + 1 or phi is exal ) & ( not Depth phi = n + 1 or not phi is exal or not (S -firstChar) . phi <> l ) implies f . phi is FinSequence ) )
;
consistency
for b1 being FinSequence st Depth phi = n + 1 & not phi is exal & Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l holds
( b1 = (<*(TheNorSymbOf S)*> ^ (f . (head phi))) ^ (f . (tail phi)) iff b1 = <* the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})*> ^ (f . ((((S -firstChar) . phi), the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})) -SymbolSubstIn (head phi))) )
;
end;

:: deftheorem DefSubst2 defines Subst2 FOMODEL3:def 20 :
for S being Language
for l being literal Element of S
for t being termal string of S
for n being Nat
for f being FinSequence-yielding Function
for phi being wff string of S holds
( ( Depth phi = n + 1 & not phi is exal implies (l,t,n,f) Subst2 phi = (<*(TheNorSymbOf S)*> ^ (f . (head phi))) ^ (f . (tail phi)) ) & ( Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l implies (l,t,n,f) Subst2 phi = <* the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})*> ^ (f . ((((S -firstChar) . phi), the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})) -SymbolSubstIn (head phi))) ) & ( ( not Depth phi = n + 1 or phi is exal ) & ( not Depth phi = n + 1 or not phi is exal or not (S -firstChar) . phi <> l ) implies (l,t,n,f) Subst2 phi = f . phi ) );

registration
let S be Language;
cluster -> FinSequence-yielding Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));
coherence
for b1 being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds b1 is FinSequence-yielding
;
end;

Lm46: for n being Nat
for S being Language
for l being literal Element of S
for t being termal string of S
for phi being wff string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (l,t,n,f) Subst2 phi is wff string of S
proof end;

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let n be Nat;
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));
let phi be wff string of S;
:: original: Subst2
redefine func (l,t,n,f) Subst2 phi -> wff string of S;
coherence
(l,t,n,f) Subst2 phi is wff string of S
by Lm46;
end;

registration
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let n be Nat;
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));
let phi be wff string of S;
cluster (l,t,n,f) Subst2 phi -> wff string of S;
coherence
for b1 being string of S st b1 = (l,t,n,f) Subst2 phi holds
b1 is wff
;
end;

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let nn be Element of NAT ;
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));
let phi be wff string of S;
:: original: Subst2
redefine func (l,t,nn,f) Subst2 phi -> Element of AllFormulasOf S;
coherence
(l,t,nn,f) Subst2 phi is Element of AllFormulasOf S
proof end;
end;

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let n be Nat;
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));
set FF = AllFormulasOf S;
set D = Funcs ((AllFormulasOf S),(AllFormulasOf S));
func (l,t,n,f) Subst3 -> Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) means :DefSubst3: :: FOMODEL3:def 21
for phi being wff string of S holds it . phi = (l,t,n,f) Subst2 phi;
existence
ex b1 being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) st
for phi being wff string of S holds b1 . phi = (l,t,n,f) Subst2 phi
proof end;
uniqueness
for b1, b2 being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) st ( for phi being wff string of S holds b1 . phi = (l,t,n,f) Subst2 phi ) & ( for phi being wff string of S holds b2 . phi = (l,t,n,f) Subst2 phi ) holds
b1 = b2
proof end;
end;

:: deftheorem DefSubst3 defines Subst3 FOMODEL3:def 21 :
for S being Language
for l being literal Element of S
for t being termal string of S
for n being Nat
for f, b6 being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds
( b6 = (l,t,n,f) Subst3 iff for phi being wff string of S holds b6 . phi = (l,t,n,f) Subst2 phi );

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));
set FF = AllFormulasOf S;
set D = Funcs ((AllFormulasOf S),(AllFormulasOf S));
deffunc H1( Nat, Element of Funcs ((AllFormulasOf S),(AllFormulasOf S))) -> Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) = (l,t,$1,$2) Subst3 ;
func (l,t) Subst4 f -> Function of NAT,(Funcs ((AllFormulasOf S),(AllFormulasOf S))) means :DefSubst4: :: FOMODEL3:def 22
( it . 0 = f & ( for m being Nat holds it . (m + 1) = (l,t,m,(it . m)) Subst3 ) );
existence
ex b1 being Function of NAT,(Funcs ((AllFormulasOf S),(AllFormulasOf S))) st
( b1 . 0 = f & ( for m being Nat holds b1 . (m + 1) = (l,t,m,(b1 . m)) Subst3 ) )
proof end;
uniqueness
for b1, b2 being Function of NAT,(Funcs ((AllFormulasOf S),(AllFormulasOf S))) st b1 . 0 = f & ( for m being Nat holds b1 . (m + 1) = (l,t,m,(b1 . m)) Subst3 ) & b2 . 0 = f & ( for m being Nat holds b2 . (m + 1) = (l,t,m,(b2 . m)) Subst3 ) holds
b1 = b2
proof end;
end;

:: deftheorem DefSubst4 defines Subst4 FOMODEL3:def 22 :
for S being Language
for l being literal Element of S
for t being termal string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S))
for b5 being Function of NAT,(Funcs ((AllFormulasOf S),(AllFormulasOf S))) holds
( b5 = (l,t) Subst4 f iff ( b5 . 0 = f & ( for m being Nat holds b5 . (m + 1) = (l,t,m,(b5 . m)) Subst3 ) ) );

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
set AF = AtomicFormulasOf S;
set TT = AllTermsOf S;
func l AtomicSubst t -> Function of (AtomicFormulasOf S),(AtomicFormulasOf S) means :DefAtomSubst2: :: FOMODEL3:def 23
for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
it . phi0 = (l,tt) AtomicSubst phi0;
existence
ex b1 being Function of (AtomicFormulasOf S),(AtomicFormulasOf S) st
for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
b1 . phi0 = (l,tt) AtomicSubst phi0
proof end;
uniqueness
for b1, b2 being Function of (AtomicFormulasOf S),(AtomicFormulasOf S) st ( for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
b1 . phi0 = (l,tt) AtomicSubst phi0 ) & ( for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
b2 . phi0 = (l,tt) AtomicSubst phi0 ) holds
b1 = b2
proof end;
end;

:: deftheorem DefAtomSubst2 defines AtomicSubst FOMODEL3:def 23 :
for S being Language
for l being literal Element of S
for t being termal string of S
for b4 being Function of (AtomicFormulasOf S),(AtomicFormulasOf S) holds
( b4 = l AtomicSubst t iff for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
b4 . phi0 = (l,tt) AtomicSubst phi0 );

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
func l Subst1 t -> Function equals :: FOMODEL3:def 24
(id (AllFormulasOf S)) +* (l AtomicSubst t);
coherence
(id (AllFormulasOf S)) +* (l AtomicSubst t) is Function
;
end;

:: deftheorem defines Subst1 FOMODEL3:def 24 :
for S being Language
for l being literal Element of S
for t being termal string of S holds l Subst1 t = (id (AllFormulasOf S)) +* (l AtomicSubst t);

Lm47: for S being Language
for l being literal Element of S
for t being termal string of S holds l Subst1 t in Funcs ((AllFormulasOf S),(AllFormulasOf S))
proof end;

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
:: original: Subst1
redefine func l Subst1 t -> Element of Funcs ((AllFormulasOf S),((AllSymbolsOf S) *));
coherence
l Subst1 t is Element of Funcs ((AllFormulasOf S),((AllSymbolsOf S) *))
proof end;
end;

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
:: original: Subst1
redefine func l Subst1 t -> Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));
coherence
l Subst1 t is Element of Funcs ((AllFormulasOf S),(AllFormulasOf S))
by Lm47;
end;

definition
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let phi be wff string of S;
func (l,t) SubstIn phi -> wff string of S equals :: FOMODEL3:def 25
(((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi;
coherence
(((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi is wff string of S
proof end;
end;

:: deftheorem defines SubstIn FOMODEL3:def 25 :
for S being Language
for l being literal Element of S
for t being termal string of S
for phi being wff string of S holds (l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi;

registration
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let phi be wff string of S;
cluster (l,t) SubstIn phi -> wff string of S;
coherence
for b1 being string of S st b1 = (l,t) SubstIn phi holds
b1 is wff
;
end;

Lm48: for m being Nat
for S being Language
for l being literal Element of S
for t being termal string of S
for phi being wff string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (((l,t) Subst4 f) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 phi
proof end;

Lm49: for m being Nat
for S being Language
for l being literal Element of S
for t being termal string of S
for phi being wff string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds
( (((l,t) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) )
proof end;

Lm50: for m being Nat
for S being Language
for l being literal Element of S
for t being termal string of S
for phi being wff string of S st phi is m -wff holds
(l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi
proof end;

registration
let S be Language;
let l be literal Element of S;
let tt be Element of AllTermsOf S;
let phi0 be 0wff string of S;
identify (l,tt) SubstIn phi0 with (l,tt) AtomicSubst phi0;
compatibility
(l,tt) SubstIn phi0 = (l,tt) AtomicSubst phi0
proof end;
identify (l,tt) AtomicSubst phi0 with (l,tt) SubstIn phi0;
compatibility
(l,tt) AtomicSubst phi0 = (l,tt) SubstIn phi0
;
end;

theorem Th10: :: FOMODEL3:10
for U being non empty set
for S being Language
for l being literal Element of S
for psi being wff string of S
for tt being Element of AllTermsOf S holds
( Depth ((l,tt) SubstIn psi) = Depth psi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi ) )
proof end;

registration
let m be Nat;
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let phi be m -wff string of S;
cluster (l,t) SubstIn phi -> m -wff string of S;
coherence
for b1 being string of S st b1 = (l,t) SubstIn phi holds
b1 is m -wff
proof end;
end;

Lm51: for X being set
for U being non empty set
for S1, S2 being Language
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds
(I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *)
proof end;

theorem Th11: :: FOMODEL3:11
for X being set
for U being non empty set
for S1, S2 being Language
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds
(I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
proof end;

Lm52: for U being non empty set
for S1, S2 being Language
for phi1 being 0wff string of S1
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & TheEqSymbOf S1 = TheEqSymbOf S2 holds
ex phi2 being 0wff string of S2 st
( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 )
proof end;

theorem :: FOMODEL3:12
for U being non empty set
for S1, S2 being Language st TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) holds
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2
for phi1 being wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
ex phi2 being wff string of S2 st
( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )
proof end;

theorem Th13: :: FOMODEL3:13
for U being non empty set
for S being Language
for phi being wff string of S
for I1, I2 being Element of U -InterpretersOf S st I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) holds
I1 -TruthEval phi = I2 -TruthEval phi
proof end;

theorem :: FOMODEL3:14
for X being set
for U being non empty set
for u being Element of U
for S being Language
for l being literal Element of S
for I being Element of U -InterpretersOf S st not l is X -occurring & X is I -satisfied holds
X is (l,u) ReassignIn I -satisfied
proof end;

theorem :: FOMODEL3:15
for U being non empty set
for u being Element of U
for S being Language
for l being literal Element of S
for E being Equivalence_Relation of U
for i being b5 -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E
proof end;