FOMODEL3: Free interpretation, quotient interpretation and substitution of a letter with a term for first order languages

proof end;

end;

:: deftheorem defines -compound FOMODEL3:def 1 :

registration

let S be Language;
let mm be Element of NAT ;
let s be termal Element of S;
let V be |.(ar s).| -element Element of ((S -termsOfMaxDepth) . mm) * ;

cluster s -compound V -> mm + 1 -termal for string of S;

proof end;

end;

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

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

Lm3: 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 |.(ar s).| -element Element of (AllTermsOf S) * ;

cluster s -compound V -> termal for string of S;

proof end;

end;

registration

let S be Language;
let s be relational Element of S;
let V be |.(ar s).| -element Element of (AllTermsOf S) * ;

cluster s -compound V -> 0wff for string of S;

end;

definition

let S be Language;
let s be Element of S;

func s -compound -> Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) means :Def2: :: FOMODEL3:def 2
for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds it . V = s -compound V;

proof end;

proof end;

end;

:: deftheorem Def2 defines -compound FOMODEL3:def 2 :

registration

let S be Language;
let s be termal Element of S;

cluster (s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) -> AllTermsOf S -valued ;

proof end;

end;

registration

let S be Language;
let s be relational Element of S;

cluster (s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) -> 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 :Def3: :: FOMODEL3:def 3
(s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) if not s is relational
otherwise ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S)));

coherence ;
consistency ;

end;

:: deftheorem Def3 defines -freeInterpreter FOMODEL3:def 3 :

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

proof end;

end;

definition

let S be Language;
let X be set ;

func (S,X) -freeInterpreter -> Function means :Def4: :: FOMODEL3:def 4
( dom it = OwnSymbolsOf S & ( for s being own Element of S holds it . s = X -freeInterpreter s ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines -freeInterpreter FOMODEL3:def 4 :

registration

let S be Language;
let X be set ;

cluster (S,X) -freeInterpreter -> Function-yielding for Function;

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

proof end;

end;

registration

let S be Language;
let X be set ;

cluster (S,X) -freeInterpreter -> S, AllTermsOf S -interpreter-like for Function;

end;

definition

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

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

proof end;

end;

:: deftheorem defines -placesOf FOMODEL3:def 5 :

Lm4: 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 for Relation of (n -tuples_on X),(n -tuples_on Y);

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 for Relation of (n -tuples_on X),(n -tuples_on Y);

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 for Relation of (n -tuples_on X),(n -tuples_on Y);

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;

end;

:: deftheorem defines -placesOf FOMODEL3:def 6 :

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 ;
compatibility by Lm4;

end;

:: deftheorem defines -placesOf FOMODEL3:def 7 :

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

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

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

Lm8: for n being zero Nat
for X being non empty set
for r being Relation of X holds
( n -placesOf r is total & n -placesOf r is symmetric & n -placesOf r is transitive )

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 for Relation of (n -tuples_on X);

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 for Relation of (n -tuples_on X);

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 for total Relation of (n -tuples_on X);

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 for total Relation of (n -tuples_on X);

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 for symmetric transitive Relation of (n -tuples_on X);

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

end;

:: deftheorem defines quotient FOMODEL3:def 8 :

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

proof end;

end;

definition

let E, F be Relation;
let f be Function;

attr f is E,F -respecting means :Def9: :: FOMODEL3:def 9
for x1, x2 being set st [x1,x2] in E holds
[(f . x1),(f . x2)] in F;

end;

:: deftheorem Def9 defines -respecting FOMODEL3:def 9 :

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 :Def10: :: FOMODEL3:def 10
f is |.(ar s).| -placesOf E,E -respecting if not s is relational
otherwise f is |.(ar s).| -placesOf E, id BOOLEAN -respecting ;

consistency ;

end;

:: deftheorem Def10 defines -respecting FOMODEL3:def 10 :

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 for Element of bool [:X,Y:];

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 |.(ar s).| -tuples_on U -defined U \/ BOOLEAN -valued Function-like total quasi_total E -respecting for Interpreter of s,U;

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

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 ;

end;

definition

let X be non empty set ;
let x be Element of SmallestPartition X;

func DeTrivial x -> Element of X means :Def11: :: FOMODEL3:def 11
x = {it};

proof end;

uniqueness by ZFMISC_1:3;

end;

:: deftheorem Def11 defines DeTrivial FOMODEL3:def 11 :

definition

let X be non empty set ;

func peeler X -> Function of (SmallestPartition X),X means :Def12: :: FOMODEL3:def 12
for x being Element of SmallestPartition X holds it . x = DeTrivial x;

proof end;

proof end;

end;

:: deftheorem Def12 defines peeler FOMODEL3:def 12 :

registration

let X be non empty set ;
let EqR be Equivalence_Relation of X;

cluster -> non empty for Element of Class EqR;

end;

Lm9: 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 for Relation;

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 for Relation of (Class E),(Class F);

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

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 :Def13: :: FOMODEL3:def 13
for x being Element of X holds it . x = EqClass (E,x);

proof end;

proof end;

end;

:: deftheorem Def13 defines -class FOMODEL3:def 13 :

registration

let X be non empty set ;
let E be Equivalence_Relation of X;

cluster E -class -> onto for Function of X,(Class E);

proof end;

end;

registration

let X, Y be non empty set ;

cluster Relation-like X -defined Y -valued onto for Element of bool [:X,Y:];

proof end;

end;

registration

let Y be non empty set ;

cluster Relation-like Y -valued onto for set ;

proof end;

end;

registration

let Y be non empty set ;
let R be Y -valued Relation;

cluster R ~ -> Y -defined for Relation;

proof end;

end;

registration

let Y be non empty set ;
let R be Y -valued onto Relation;

cluster R ~ -> Y -defined total for Y -defined Relation;

proof end;

end;

registration

let X, Y be non empty set ;
let R be onto Relation of X,Y;

cluster R ~ -> total for Relation of Y,X;

end;

registration

let Y be non empty set ;
let R be Y -valued onto Relation;

cluster R ~ -> Y -defined total for Y -defined Relation;

end;

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

end;

:: deftheorem defines -tuple2Class FOMODEL3:def 14 :

registration

let U be non empty set ;
let n be Nat;
let E be Equivalence_Relation of U;

cluster n -tuple2Class E -> Function-like for Relation of (n -tuples_on (Class E)),(Class (n -placesOf E));

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 for Relation of (n -tuples_on (Class E)),(Class (n -placesOf E));

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 ;

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 :Def15: :: FOMODEL3:def 15
(|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),E)) if not s is relational
otherwise ((|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN);

coherence ;
consistency ;

end;

:: deftheorem Def15 defines quotient FOMODEL3:def 15 :

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

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

registration

let S be Language;

cluster -> own for Element of OwnSymbolsOf S;

coherence ;

cluster -> ofAtomicFormula for Element of OwnSymbolsOf S;

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 -> |.(ar o).| -placesOf E,E -respecting for Interpreter of o,U;

coherence by Def10;

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 -> |.(ar r).| -placesOf E, id BOOLEAN -respecting for Interpreter of r,U;

coherence by Def10;

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

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

proof end;

end;

registration

let X be set ;
let Y be functional set ;

cluster X /\ Y -> functional for set ;

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

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 :Def16: :: FOMODEL3:def 16
for s being own Element of S holds I . s is E -respecting ;

end;

:: deftheorem Def16 defines -respecting FOMODEL3:def 16 :

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 :Def17: :: FOMODEL3:def 17
( dom it = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds it . o = (I . o) quotient E ) );

proof end;

proof end;

end;

:: deftheorem Def17 defines quotient FOMODEL3:def 17 :

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 :Def18: :: FOMODEL3:def 18
( dom it = OwnSymbolsOf S & ( for o being own Element of S holds it . o = (I . o) quotient E ) );

compatibility

proof end;

end;

:: deftheorem Def18 defines quotient FOMODEL3:def 18 :

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 ;

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 V171() S,U -interpreter-like E -respecting for Element of U -InterpretersOf S;

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 V171() S,U -interpreter-like E -respecting for set ;

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 for Interpreter of o,U;

coherence by Def16;

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

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

proof end;

end;

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

Lm13: for U1, U2, 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;

Lm14: for U1, U2, 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;

Lm15: for U1, U2, 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)
by Lm13, Lm14;

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

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

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

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

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

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

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

Lm23: for U being non empty set holds (peeler U) * ((id U) -class) = id U

proof end;

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

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

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

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

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

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

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

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

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 for string of S;

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 for string of S;

proof end;

end;

Lm32: 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 for string of S;

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

coherence by FOMODEL2:def 31;

end;

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

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 for string of S;

proof end;

end;

registration

let S be Language;
let m be Nat;
let phi be m -wff string of S;

cluster m - (Depth phi) -> non negative for ExtReal;

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 for string of S;

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 for string of S;

proof end;

end;

Lm34: 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 for set ;

proof end;

end;

theorem :: FOMODEL3:6

for X being set
for S being Language
for a being ofAtomicFormula Element of S
for T being |.(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 omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like finite-support termal for Element of ((AllSymbolsOf S) *) \ {{}};

proof end;

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

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

end;

:: deftheorem defines AtomicSubst FOMODEL3:def 19 :

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

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 for string of S;

coherence by Lm35;

end;

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

Lm37: 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 for Relation;

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

proof end;

end;

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

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

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

Lm41: for U being non empty set
for u being Element of U
for S being Language
for l1, l2 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 l1, l2 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 :Def20: :: 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 ;
consistency ;

end;

:: deftheorem Def20 defines Subst2 FOMODEL3:def 20 :

registration

let S be Language;

cluster -> FinSequence-yielding for Element of Funcs ((AllFormulasOf S),(AllFormulasOf S));

end;

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

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 for string of S;

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

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 :Def21: :: FOMODEL3:def 21
for phi being wff string of S holds it . phi = (l,t,n,f) Subst2 phi;

proof end;

proof end;

end;

:: deftheorem Def21 defines Subst3 FOMODEL3:def 21 :

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 -> sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))) means :Def22: :: FOMODEL3:def 22
( it . 0 = f & ( for m being Nat holds it . (m + 1) = (l,t,m,(it . m)) Subst3 ) );

proof end;

proof end;

end;

:: deftheorem Def22 defines Subst4 FOMODEL3:def 22 :

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

proof end;

proof end;

end;

:: deftheorem Def23 defines AtomicSubst FOMODEL3:def 23 :

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

end;

:: deftheorem defines Subst1 FOMODEL3:def 24 :

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

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

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;

proof end;

end;

:: deftheorem defines SubstIn FOMODEL3:def 25 :

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 for string of S;

end;

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

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

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

proof end;

identify (l,tt) AtomicSubst phi0 with (l,tt) SubstIn phi0;

compatibility ;

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 for string of S;