:: 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 b₁ being string of S st b₁ = s -compound V holds
b₁ 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 b₁ being string of S st b₁ = s -compound V holds
b₁ 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 b₁ being string of S st b₁ = s -compound V holds
b₁ 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 b₁ being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) st
for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b₁ . V = s -compound V

proof end;

uniqueness
for b₁, b₂ being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) st ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b₁ . V = s -compound V ) & ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b₂ . V = s -compound V ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefCompound1 defines -compound FOMODEL3:def 2 :
for S being Language
for s being Element of S
for b₃ being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) holds
( b₃ = s -compound iff for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b₃ . 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 b₁ 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 b₁ being Function st
( dom b₁ = OwnSymbolsOf S & ( for s being own Element of S holds b₁ . s = X -freeInterpreter s ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = OwnSymbolsOf S & ( for s being own Element of S holds b₁ . s = X -freeInterpreter s ) & dom b₂ = OwnSymbolsOf S & ( for s being own Element of S holds b₂ . s = X -freeInterpreter s ) holds
b₁ = b₂

proof end;

end;

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

registration

let S be Language;
let X be set ;
cluster (S,X) -freeInterpreter -> Function-yielding Function;
coherence
for b₁ being Function st b₁ = (S,X) -freeInterpreter holds
b₁ 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 b₁ being Function st b₁ = (S,X) -freeInterpreter holds
b₁ 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 b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ 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 b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ 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 b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ 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 b₁ being Relation of (n -tuples_on X) holds
( b₁ = n -placesOf R iff b₁ = {[{},{}]} ) 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 b₁ being Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
b₁ 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 b₁ being Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
b₁ 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 b₁ being Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
( b₁ is symmetric & b₁ 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 b₁ being Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
( b₁ is transitive & b₁ 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 b₁ being Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
( b₁ is total & b₁ is symmetric & b₁ 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 b₁ being Function of X,Y st b₁ 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 b₁ being Interpreter of s,U st b₁ 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 b₁ being Function st b₁ 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 b₁ being Element of X st x = {b₁}

proof end;

uniqueness
for b₁, b₂ being Element of X st x = {b₁} & x = {b₂} holds
b₁ = b₂ 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 b₃ being Element of X holds
( b₃ = DeTrivial x iff x = {b₃} );

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 b₁ being Function of {_{X}_},X st
for x being Element of {_{X}_} holds b₁ . x = DeTrivial x

proof end;

uniqueness
for b₁, b₂ being Function of {_{X}_},X st ( for x being Element of {_{X}_} holds b₁ . x = DeTrivial x ) & ( for x being Element of {_{X}_} holds b₂ . x = DeTrivial x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefPeel defines peeler FOMODEL3:def 12 :
for X being non empty set
for b₂ being Function of {_{X}_},X holds
( b₂ = peeler X iff for x being Element of {_{X}_} holds b₂ . 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 b₁ being Element of Class EqR holds not b₁ 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 b₁ being Relation st b₁ = f quotient (E,F) holds
b₁ 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 b₁ being Relation of (Class E),(Class F) st b₁ = R quotient (E,F) holds
b₁ 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 b₁ being Function of X,(Class E) st
for x being Element of X holds b₁ . x = EqClass (E,x)

proof end;

uniqueness
for b₁, b₂ being Function of X,(Class E) st ( for x being Element of X holds b₁ . x = EqClass (E,x) ) & ( for x being Element of X holds b₂ . x = EqClass (E,x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefClass defines -class FOMODEL3:def 13 :
for X being non empty set
for E being Equivalence_Relation of X
for b₃ being Function of X,(Class E) holds
( b₃ = E -class iff for x being Element of X holds b₃ . 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 b₁ being Function of X,(Class E) st b₁ = E -class holds
b₁ 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 b₁ being Relation of X,Y st b₁ is onto

proof end;

end;

registration

let Y be non empty set ;
cluster Relation-like Y -valued onto set ;
existence
ex b₁ being Y -valued Relation st b₁ 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 b₁ being Relation st b₁ = R ~ holds
b₁ 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 b₁ being Y -defined Relation st b₁ = R ~ holds
b₁ 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 b₁ being Relation of Y,X st b₁ = R ~ holds
b₁ 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 b₁ being Y -defined Relation st b₁ = R ~ holds
b₁ 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 b₁ being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b₁ = n -tuple2Class E holds
b₁ 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 b₁ being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b₁ = n -tuple2Class E holds
b₁ 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 b₁ 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 b₁ being Element of OwnSymbolsOf S holds b₁ is own by FOMODEL1:def 19;
cluster -> ofAtomicFormula Element of OwnSymbolsOf S;
coherence
for b₁ being Element of OwnSymbolsOf S holds b₁ 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 b₁ being Interpreter of o,U st b₁ is E -respecting holds
b₁ 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 b₁ being Interpreter of r,U st b₁ is E -respecting holds
b₁ 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 b₁ being Relation st b₁ = n -placesOf f holds
b₁ 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 b₁,b₂ -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 b₁ being Function st
( dom b₁ = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b₁ . o = (I . o) quotient E ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b₁ . o = (I . o) quotient E ) & dom b₂ = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b₂ . o = (I . o) quotient E ) holds
b₁ = b₂

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 b₁,b₂ -interpreter-like Function
for b₅ being Function holds
( b₅ = I quotient E iff ( dom b₅ = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b₅ . 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 b₁ being Function holds
( b₁ = I quotient E iff ( dom b₁ = OwnSymbolsOf S & ( for o being own Element of S holds b₁ . 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 b₁,b₂ -interpreter-like Function
for b₅ being Function holds
( b₅ = I quotient E iff ( dom b₅ = OwnSymbolsOf S & ( for o being own Element of S holds b₅ . 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 b₁ being Element of U -InterpretersOf S st b₁ 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 b₁ being S,U -interpreter-like Function st b₁ 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 b₁ being Interpreter of o,U st b₁ = I . o holds
b₁ 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 b₁ being Function st b₁ = I quotient E holds
b₁ 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 b₃,b₄ -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 b₁ -valued b₃ -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 b₃ -placesOf b₄,b₅ -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 b₄,b₁ -interpreter-like b₅ -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 b₂,b₁ -interpreter-like b₃ -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 b₂,b₁ -interpreter-like b₃ -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 b₂,b₁ -interpreter-like b₃ -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 b₂,b₁ -interpreter-like b₃ -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 b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn t holds
b₁ 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 b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn t holds
b₁ 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 b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn phi holds
b₁ 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 b₁ being number st b₁ = Depth phi holds
b₁ 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 b₁ being string of S st b₁ = phi null m holds
b₁ 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 b₁ being ext-real number st b₁ = m - (Depth phi) holds
not b₁ 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 b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn phi holds
b₁ 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 b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn phi holds
b₁ 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 b₁ being set st b₁ = (Depth ((l1,l2) -SymbolSubstIn phi)) \+\ (Depth phi) holds
b₁ 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 b₃) -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 b₁ being string of S st b₁ 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 b₁ being string of S st b₁ 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 b₄,b₂ -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 b₁ being string of S st b₁ = (l,tt) AtomicSubst phi0 holds
b₁ 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 b₃,b₂ -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 b₂,b₁ -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 b₁ being Relation st b₁ = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) holds
b₁ 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 b₁ being Relation st b₁ = (l1 SubstWith l2) | (AllTermsOf S) holds
b₁ 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 b₄,b₁ -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 b₃,b₁ -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 b₁ being FinSequence st Depth phi = n + 1 & not phi is exal & Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l holds
( b₁ = (<*(TheNorSymbOf S)*> ^ (f . (head phi))) ^ (f . (tail phi)) iff b₁ = <* 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 b₁ being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds b₁ 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 b₁ being string of S st b₁ = (l,t,n,f) Subst2 phi holds
b₁ 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 b₁ being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) st
for phi being wff string of S holds b₁ . phi = (l,t,n,f) Subst2 phi

proof end;

uniqueness
for b₁, b₂ being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) st ( for phi being wff string of S holds b₁ . phi = (l,t,n,f) Subst2 phi ) & ( for phi being wff string of S holds b₂ . phi = (l,t,n,f) Subst2 phi ) holds
b₁ = b₂

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, b₆ being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds
( b₆ = (l,t,n,f) Subst3 iff for phi being wff string of S holds b₆ . 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 H₁( 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 b₁ being Function of NAT,(Funcs ((AllFormulasOf S),(AllFormulasOf S))) st
( b₁ . 0 = f & ( for m being Nat holds b₁ . (m + 1) = (l,t,m,(b₁ . m)) Subst3 ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT,(Funcs ((AllFormulasOf S),(AllFormulasOf S))) st b₁ . 0 = f & ( for m being Nat holds b₁ . (m + 1) = (l,t,m,(b₁ . m)) Subst3 ) & b₂ . 0 = f & ( for m being Nat holds b₂ . (m + 1) = (l,t,m,(b₂ . m)) Subst3 ) holds
b₁ = b₂

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 b₅ being Function of NAT,(Funcs ((AllFormulasOf S),(AllFormulasOf S))) holds
( b₅ = (l,t) Subst4 f iff ( b₅ . 0 = f & ( for m being Nat holds b₅ . (m + 1) = (l,t,m,(b₅ . 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 b₁ 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
b₁ . phi0 = (l,tt) AtomicSubst phi0

proof end;

uniqueness
for b₁, b₂ 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
b₁ . phi0 = (l,tt) AtomicSubst phi0 ) & ( for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
b₂ . phi0 = (l,tt) AtomicSubst phi0 ) holds
b₁ = b₂

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 b₄ being Function of (AtomicFormulasOf S),(AtomicFormulasOf S) holds
( b₄ = l AtomicSubst t iff for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
b₄ . 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 b₁ being string of S st b₁ = (l,t) SubstIn phi holds
b₁ 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 b₁ being string of S st b₁ = (l,t) SubstIn phi holds
b₁ 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 b₅ -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

proof end;