:: by Marco B. Caminati

::

:: Received December 29, 2010

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

definition

let S be Language;

let s be Element of S;

let V be Element of (((AllSymbolsOf S) *) \ {{}}) * ;

coherence

<*s*> ^ ((S -multiCat) . V) is string of S

end;
let s be Element of S;

let V be Element of (((AllSymbolsOf S) *) \ {{}}) * ;

coherence

<*s*> ^ ((S -multiCat) . V) is string of S

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

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 |.(ar s).| -element Element of ((S -termsOfMaxDepth) . mm) * ;

coherence

for b_{1} being string of S st b_{1} = s -compound V holds

b_{1} is mm + 1 -termal

end;
let mm be Element of NAT ;

let s be termal Element of S;

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

coherence

for b

b

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

coherence

for b_{1} being string of S st b_{1} = s -compound V holds

b_{1} is termal

end;
let s be termal Element of S;

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

coherence

for b

b

proof end;

registration

let S be Language;

let s be relational Element of S;

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

coherence

for b_{1} being string of S st b_{1} = s -compound V holds

b_{1} is 0wff
;

end;
let s be relational Element of S;

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

coherence

for b

b

definition

let S be Language;

let s be Element of S;

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

for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b_{1} . V = s -compound V

for b_{1}, b_{2} being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) st ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b_{1} . V = s -compound V ) & ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b_{2} . V = s -compound V ) holds

b_{1} = b_{2}

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

existence for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds it . V = s -compound V;

ex b

for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b

proof end;

uniqueness for b

b

proof end;

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

for S being Language

for s being Element of S

for b_{3} being Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}) holds

( b_{3} = s -compound iff for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds b_{3} . V = s -compound V );

for S being Language

for s being Element of S

for b

( b

registration

let S be Language;

let s be termal Element of S;

coherence

(s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is AllTermsOf S -valued

end;
let s be termal Element of S;

coherence

(s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is AllTermsOf S -valued

proof end;

registration

let S be Language;

let s be relational Element of S;

coherence

(s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is AtomicFormulasOf S -valued

end;
let s be relational Element of S;

coherence

(s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is AtomicFormulasOf S -valued

proof end;

definition

let S be Language;

let s be ofAtomicFormula Element of S;

let X be set ;

( ( not s is relational implies (s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is set ) & ( s is relational implies ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S))) is set ) ) ;

consistency

for b_{1} being set holds verum
;

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

( ( not s is relational implies (s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S)) is set ) & ( s is relational implies ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S))) is set ) ) ;

consistency

for b

:: deftheorem Def3 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) | (|.(ar s).| -tuples_on (AllTermsOf S)) ) & ( s is relational implies X -freeInterpreter s = ((s -compound) | (|.(ar s).| -tuples_on (AllTermsOf S))) * (chi (X,(AtomicFormulasOf S))) ) );

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) | (|.(ar s).| -tuples_on (AllTermsOf S)) ) & ( s is relational implies X -freeInterpreter s = ((s -compound) | (|.(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

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

definition

let S be Language;

let X be set ;

ex b_{1} being Function st

( dom b_{1} = OwnSymbolsOf S & ( for s being own Element of S holds b_{1} . s = X -freeInterpreter s ) )

for b_{1}, b_{2} being Function st dom b_{1} = OwnSymbolsOf S & ( for s being own Element of S holds b_{1} . s = X -freeInterpreter s ) & dom b_{2} = OwnSymbolsOf S & ( for s being own Element of S holds b_{2} . s = X -freeInterpreter s ) holds

b_{1} = b_{2}

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

existence ( dom it = OwnSymbolsOf S & ( for s being own Element of S holds it . s = X -freeInterpreter s ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

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

for S being Language

for X being set

for b_{3} being Function holds

( b_{3} = (S,X) -freeInterpreter iff ( dom b_{3} = OwnSymbolsOf S & ( for s being own Element of S holds b_{3} . s = X -freeInterpreter s ) ) );

for S being Language

for X being set

for b

( b

registration

let S be Language;

let X be set ;

coherence

for b_{1} being Function st b_{1} = (S,X) -freeInterpreter holds

b_{1} is Function-yielding

end;
let X be set ;

coherence

for b

b

proof 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

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

registration

let S be Language;

let X be set ;

coherence

for b_{1} being Function st b_{1} = (S,X) -freeInterpreter holds

b_{1} is S, AllTermsOf S -interpreter-like
;

end;
let X be set ;

coherence

for b

b

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

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

definition

let X, Y be non empty set ;

let R be Relation of X,Y;

let n be Nat;

{ [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)

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

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

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

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

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;

coherence

for b_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is total

end;
let R be total Relation of X,Y;

let n be non zero Nat;

coherence

for b

b

proof end;

registration

let X, Y be non empty set ;

let R be total Relation of X,Y;

let n be Nat;

coherence

for b_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is total

end;
let R be total Relation of X,Y;

let n be Nat;

coherence

for b

b

proof end;

registration

let X, Y be non empty set ;

let R be Relation of X,Y;

let n be zero Nat;

coherence

for b_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is Function-like

end;
let R be Relation of X,Y;

let n be zero Nat;

coherence

for b

b

proof end;

definition

let X be non empty set ;

let R be Relation of X;

let n be Nat;

coherence

n -placesOf R is Relation of (n -tuples_on X) ;

end;
let R be Relation of X;

let n be Nat;

coherence

n -placesOf R is Relation of (n -tuples_on X) ;

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

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;

n -placesOf R is Relation of (n -tuples_on X) ;

compatibility

for b_{1} being Relation of (n -tuples_on X) holds

( b_{1} = n -placesOf R iff b_{1} = {[{},{}]} )
by Lm4;

end;
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 redefine func n -placesOf R -> Relation of (n -tuples_on X) equals :: FOMODEL3:def 7

{[{},{}]};

n -placesOf R is Relation of (n -tuples_on X) ;

compatibility

for b

( b

:: 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 = {[{},{}]};

for X being non empty set

for R being Relation of X

for n being zero Nat holds n -placesOf R = {[{},{}]};

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;

coherence

for b_{1} being Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is total
;

end;
let R be total symmetric Relation of X;

let n be Nat;

coherence

for b

b

registration

let X be non empty set ;

let R be total symmetric Relation of X;

let n be Nat;

coherence

for b_{1} being Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is symmetric

end;
let R be total symmetric Relation of X;

let n be Nat;

coherence

for b

b

proof end;

registration

let X be non empty set ;

let R be total symmetric Relation of X;

let n be Nat;

coherence

for b_{1} being total Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is symmetric
;

end;
let R be total symmetric Relation of X;

let n be Nat;

coherence

for b

b

registration

let X be non empty set ;

let R be total transitive Relation of X;

let n be Nat;

coherence

for b_{1} being total Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is transitive

end;
let R be total transitive Relation of X;

let n be Nat;

coherence

for b

b

proof end;

registration

let X be non empty set ;

let R be Equivalence_Relation of X;

let n be Nat;

for b_{1} being symmetric transitive Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is total
;

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

coherence for b

b

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;

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

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

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

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)

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

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

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;

verum ;

end;
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 f is |.(ar s).| -placesOf E,E -respecting if not s is relational

otherwise f is |.(ar s).| -placesOf E, id BOOLEAN -respecting ;

verum ;

:: deftheorem Def10 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 |.(ar s).| -placesOf E,E -respecting ) ) & ( s is relational implies ( f is E -respecting iff f is |.(ar s).| -placesOf E, id BOOLEAN -respecting ) ) );

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 |.(ar s).| -placesOf E,E -respecting ) ) & ( s is relational implies ( f is E -respecting iff f is |.(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;

ex b_{1} being Function of X,Y st b_{1} is E,F -respecting

end;
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 Function of ,;

existence ex b

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

ex b_{1} being Interpreter of s,U st b_{1} is E -respecting

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

existence ex b

proof end;

registration

let X, Y be non empty set ;

let E be Equivalence_Relation of X;

let F be Equivalence_Relation of Y;

existence

ex b_{1} being Function st b_{1} is E,F -respecting

end;
let E be Equivalence_Relation of X;

let F be Equivalence_Relation of Y;

existence

ex b

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

definition

let X be non empty set ;

let x be Element of SmallestPartition X;

existence

ex b_{1} being Element of X st x = {b_{1}}

for b_{1}, b_{2} being Element of X st x = {b_{1}} & x = {b_{2}} holds

b_{1} = b_{2}
by ZFMISC_1:3;

end;
let x be Element of SmallestPartition X;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def11 defines DeTrivial FOMODEL3:def 11 :

for X being non empty set

for x being Element of SmallestPartition X

for b_{3} being Element of X holds

( b_{3} = DeTrivial x iff x = {b_{3}} );

for X being non empty set

for x being Element of SmallestPartition X

for b

( b

definition

let X be non empty set ;

ex b_{1} being Function of {_{X}_},X st

for x being Element of {_{X}_} holds b_{1} . x = DeTrivial x

for b_{1}, b_{2} being Function of {_{X}_},X st ( for x being Element of {_{X}_} holds b_{1} . x = DeTrivial x ) & ( for x being Element of {_{X}_} holds b_{2} . x = DeTrivial x ) holds

b_{1} = b_{2}

end;
func peeler X -> Function of {_{X}_},X means :Def12: :: FOMODEL3:def 12

for x being Element of {_{X}_} holds it . x = DeTrivial x;

existence for x being Element of {_{X}_} holds it . x = DeTrivial x;

ex b

for x being Element of {_{X}_} holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines peeler FOMODEL3:def 12 :

for X being non empty set

for b_{2} being Function of {_{X}_},X holds

( b_{2} = peeler X iff for x being Element of {_{X}_} holds b_{2} . x = DeTrivial x );

for X being non empty set

for b

( b

registration

let X be non empty set ;

let EqR be Equivalence_Relation of X;

coherence

for b_{1} being Element of Class EqR holds not b_{1} is empty
;

end;
let EqR be Equivalence_Relation of X;

coherence

for b

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;

coherence

for b_{1} being Relation st b_{1} = f quotient (E,F) holds

b_{1} is Function-like

end;
let E be Equivalence_Relation of X;

let F be Equivalence_Relation of Y;

let f be E,F -respecting Function;

coherence

for b

b

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 R be total Relation of X,Y;

coherence

for b_{1} being Relation of (Class E),(Class F) st b_{1} = R quotient (E,F) holds

b_{1} is total

end;
let E be Equivalence_Relation of X;

let F be Equivalence_Relation of Y;

let R be total Relation of X,Y;

coherence

for b

b

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

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

definition

let X be non empty set ;

let E be Equivalence_Relation of X;

ex b_{1} being Function of X,(Class E) st

for x being Element of X holds b_{1} . x = EqClass (E,x)

for b_{1}, b_{2} being Function of X,(Class E) st ( for x being Element of X holds b_{1} . x = EqClass (E,x) ) & ( for x being Element of X holds b_{2} . x = EqClass (E,x) ) holds

b_{1} = b_{2}

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

existence for x being Element of X holds it . x = EqClass (E,x);

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof end;

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

for X being non empty set

for E being Equivalence_Relation of X

for b_{3} being Function of X,(Class E) holds

( b_{3} = E -class iff for x being Element of X holds b_{3} . x = EqClass (E,x) );

for X being non empty set

for E being Equivalence_Relation of X

for b

( b

registration

let X be non empty set ;

let E be Equivalence_Relation of X;

coherence

for b_{1} being Function of X,(Class E) st b_{1} = E -class holds

b_{1} is onto

end;
let E be Equivalence_Relation of X;

coherence

for b

b

proof end;

registration
end;

registration
end;

registration

let Y be non empty set ;

let R be Y -valued Relation;

coherence

for b_{1} being Relation st b_{1} = R ~ holds

b_{1} is Y -defined

end;
let R be Y -valued Relation;

coherence

for b

b

proof end;

registration

let Y be non empty set ;

let R be Y -valued onto Relation;

coherence

for b_{1} being Y -defined Relation st b_{1} = R ~ holds

b_{1} is total

end;
let R be Y -valued onto Relation;

coherence

for b

b

proof end;

registration

let X, Y be non empty set ;

let R be onto Relation of X,Y;

coherence

for b_{1} being Relation of Y,X st b_{1} = R ~ holds

b_{1} is total
;

end;
let R be onto Relation of X,Y;

coherence

for b

b

registration

let Y be non empty set ;

let R be Y -valued onto Relation;

coherence

for b_{1} being Y -defined Relation st b_{1} = R ~ holds

b_{1} is total
;

end;
let R be Y -valued onto Relation;

coherence

for b

b

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;

(n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) ;

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

(n -placesOf ((E -class) ~)) * ((n -placesOf E) -class) is Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) ;

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

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;

for b_{1} being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b_{1} = n -tuple2Class E holds

b_{1} is Function-like

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

coherence for b

b

proof end;

registration

let U be non empty set ;

let n be Nat;

let E be Equivalence_Relation of U;

coherence

for b_{1} being Relation of (n -tuples_on (Class E)),(Class (n -placesOf E)) st b_{1} = n -tuple2Class E holds

b_{1} is total
;

end;
let n be Nat;

let E be Equivalence_Relation of U;

coherence

for b

b

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

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;

( ( not s is relational implies (|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),E)) is set ) & ( s is relational implies ((|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN) is set ) ) ;

consistency

for b_{1} being set holds verum
;

end;
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 (|.(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);

( ( not s is relational implies (|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),E)) is set ) & ( s is relational implies ((|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN) is set ) ) ;

consistency

for b

:: deftheorem Def15 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 = (|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),E)) ) & ( s is relational implies f quotient E = ((|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),(id BOOLEAN)))) * (peeler BOOLEAN) ) );

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 = (|.(ar s).| -tuple2Class E) * (f quotient ((|.(ar s).| -placesOf E),E)) ) & ( s is relational implies f quotient E = ((|.(ar s).| -tuple2Class E) * (f quotient ((|.(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

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

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;

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;

coherence

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

coherence

for b_{1} being Element of OwnSymbolsOf S holds b_{1} is ofAtomicFormula
;

end;
coherence

for b

coherence

for b

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;

coherence

for b_{1} being Interpreter of o,U st b_{1} is E -respecting holds

b_{1} is |.(ar o).| -placesOf E,E -respecting
by Def10;

end;
let U be non empty set ;

let o be non relational ofAtomicFormula Element of S;

let E be Relation of U;

coherence

for b

b

registration

let S be Language;

let U be non empty set ;

let r be relational Element of S;

let E be Relation of U;

coherence

for b_{1} being Interpreter of r,U st b_{1} is E -respecting holds

b_{1} is |.(ar r).| -placesOf E, id BOOLEAN -respecting
by Def10;

end;
let U be non empty set ;

let r be relational Element of S;

let E be Relation of U;

coherence

for b

b

registration

let n be Nat;

let U1, U2 be non empty set ;

let f be Function-like Relation of U1,U2;

coherence

for b_{1} being Relation st b_{1} = n -placesOf f holds

b_{1} is Function-like

end;
let U1, U2 be non empty set ;

let f be Function-like Relation of U1,U2;

coherence

for b

b

proof end;

registration

let U1, U2 be non empty set ;

let n be zero Nat;

let R be Relation of U1,U2;

coherence

for b_{1} being set st b_{1} = (n -placesOf R) \+\ (id {{}}) holds

b_{1} is empty

end;
let n be zero Nat;

let R be Relation of U1,U2;

coherence

for b

b

proof end;

registration

let X be set ;

let Y be functional set ;

coherence

for b_{1} being set st b_{1} = X /\ Y holds

b_{1} is functional
;

end;
let Y be functional set ;

coherence

for b

b

theorem :: FOMODEL3:2

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;

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

for s being own Element of S holds I . s is E -respecting ;

:: deftheorem Def16 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_{1},b_{2} -interpreter-like Function holds

( I is E -respecting iff for s being own Element of S holds I . s is E -respecting );

for S being Language

for U being non empty set

for E being Equivalence_Relation of U

for I being b

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

ex b_{1} being Function st

( dom b_{1} = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b_{1} . o = (I . o) quotient E ) )

for b_{1}, b_{2} being Function st dom b_{1} = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b_{1} . o = (I . o) quotient E ) & dom b_{2} = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b_{2} . o = (I . o) quotient E ) holds

b_{1} = b_{2}

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

existence ( dom it = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds it . o = (I . o) quotient E ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def17 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_{1},b_{2} -interpreter-like Function

for b_{5} being Function holds

( b_{5} = I quotient E iff ( dom b_{5} = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds b_{5} . o = (I . o) quotient E ) ) );

for S being Language

for U being non empty set

for E being Equivalence_Relation of U

for I being b

for b

( b

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;

for b_{1} being Function holds

( b_{1} = I quotient E iff ( dom b_{1} = OwnSymbolsOf S & ( for o being own Element of S holds b_{1} . o = (I . o) quotient E ) ) )

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

for b

( b

proof end;

:: deftheorem Def18 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_{1},b_{2} -interpreter-like Function

for b_{5} being Function holds

( b_{5} = I quotient E iff ( dom b_{5} = OwnSymbolsOf S & ( for o being own Element of S holds b_{5} . o = (I . o) quotient E ) ) );

for S being Language

for U being non empty set

for E being Equivalence_Relation of U

for I being b

for b

( b

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;

coherence

I quotient E is OwnSymbolsOf S -defined

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

let E be Equivalence_Relation of U;

coherence

I quotient E is OwnSymbolsOf S -defined

proof end;

registration

let S be Language;

let U be non empty set ;

let E be Equivalence_Relation of U;

ex b_{1} being Element of U -InterpretersOf S st b_{1} is E -respecting

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

existence ex b

proof end;

registration

let S be Language;

let U be non empty set ;

let E be Equivalence_Relation of U;

ex b_{1} being S,U -interpreter-like Function st b_{1} is E -respecting

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

existence ex b

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

coherence

for b_{1} being Interpreter of o,U st b_{1} = I . o holds

b_{1} is E -respecting
by Def16;

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

coherence

for b

b

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;

coherence

for b_{1} being Function st b_{1} = I quotient E holds

b_{1} is S, Class E -interpreter-like

end;
let U be non empty set ;

let E be Equivalence_Relation of U;

let I be S,U -interpreter-like E -respecting Function;

coherence

for b

b

proof 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

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

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

proof end;

Lm19: for U1, U2 being non empty set

for m being Nat

for p being b

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

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

proof end;

Lm25: for U being non empty set

for S being Language

for E being Equivalence_Relation of U

for I being b

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

(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_{2},b_{1} -interpreter-like b_{3} -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval) by Lm25;

for S being Language

for E being Equivalence_Relation of U

for I being b

theorem :: FOMODEL3:4

for X being set

for S being Language holds ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S) by Lm29;

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_{2},b_{1} -interpreter-like b_{3} -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds

(i quotient R) -AtomicEval phi = i -AtomicEval phi by Lm26;

for S being Language

for R being Equivalence_Relation of U1

for phi being 0wff string of S

for i being b

(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

(x,s) -SymbolSubstIn w is string of S

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

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;

coherence

for b_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn t holds

b_{1} is m -termal

end;
let l1, l2 be literal Element of S;

let m be Nat;

let t be m -termal string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let t be termal string of S;

let l1, l2 be literal Element of S;

coherence

for b_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn t holds

b_{1} is termal

end;
let t be termal string of S;

let l1, l2 be literal Element of S;

coherence

for b

b

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

coherence

for b_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn phi holds

b_{1} is 0wff

end;
let l1, l2 be literal Element of S;

let phi be 0wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let m0 be zero number ;

let phi be m0 -wff string of S;

coherence

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

b_{1} is zero
by FOMODEL2:def 31;

end;
let m0 be zero number ;

let phi be m0 -wff string of S;

coherence

for b

b

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

w null m is string of S ;

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

registration

let S be Language;

let phi be wff string of S;

let m be Nat;

coherence

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

b_{1} is (Depth phi) + m -wff

end;
let phi be wff string of S;

let m be Nat;

coherence

for b

b

proof end;

registration

let S be Language;

let m be Nat;

let phi be m -wff string of S;

coherence

for b_{1} being ExtReal st b_{1} = m - (Depth phi) holds

not b_{1} is negative

end;
let m be Nat;

let phi be m -wff string of S;

coherence

for b

not b

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

coherence

for b_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn phi holds

b_{1} is m -wff

end;
let l1, l2 be literal Element of S;

let m be Nat;

let phi be m -wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let l1, l2 be literal Element of S;

let phi be wff string of S;

coherence

for b_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn phi holds

b_{1} is wff

end;
let l1, l2 be literal Element of S;

let phi be wff string of S;

coherence

for b

b

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

coherence

for b_{1} being set st b_{1} = (Depth ((l1,l2) -SymbolSubstIn phi)) \+\ (Depth phi) holds

b_{1} is empty

end;
let l1, l2 be literal Element of S;

let phi be wff string of S;

coherence

for b

b

proof end;

theorem :: FOMODEL3:6

for X being set

for S being Language

for a being ofAtomicFormula Element of S

for T being |.(ar b_{3}).| -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) ) )

for S being Language

for a being ofAtomicFormula Element of S

for T being |.(ar b

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

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

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

end;
cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like finite-support termal for string of (AllSymbolsOf S);

existence ex b

proof end;

cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like finite-support 0wff for string of (AllSymbolsOf S);

existence ex b

proof 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_{4},b_{2} -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)

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

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;

<*((S -firstChar) . phi0)*> ^ ((S -multiCat) . ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0))) is FinSequence ;

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

<*((S -firstChar) . phi0)*> ^ ((S -multiCat) . ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0))) is FinSequence ;

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

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

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

(l,tt) AtomicSubst phi0 is string of S by Lm35;

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

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;

coherence

for b_{1} being string of S st b_{1} = (l,tt) AtomicSubst phi0 holds

b_{1} is 0wff
by Lm35;

end;
let l be literal Element of S;

let tt be Element of AllTermsOf S;

let phi0 be 0wff string of S;

coherence

for b

b

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

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_{2},b_{1} -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

for S being Language

for l being literal Element of S

for phi0 being 0wff string of S

for I being b

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;

for b_{1} being Relation st b_{1} = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) holds

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

end;
let l1, l2 be literal Element of S;

let m be Nat;

cluster K18((l1 SubstWith l2),((S -termsOfMaxDepth) . m)) -> (S -termsOfMaxDepth) . m -valued for Relation;

coherence for b

b

proof end;

registration

let S be Language;

let l1, l2 be literal Element of S;

coherence

for b_{1} being Relation st b_{1} = (l1 SubstWith l2) | (AllTermsOf S) holds

b_{1} is AllTermsOf S -valued

end;
let l1, l2 be literal Element of S;

coherence

for b

b

proof 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

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

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

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;

( ( 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_{1} being FinSequence st Depth phi = n + 1 & not phi is exal & Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l holds

( b_{1} = (<*(TheNorSymbOf S)*> ^ (f . (head phi))) ^ (f . (tail phi)) iff b_{1} = <* 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;
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 (<*(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;

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

( b

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

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;

coherence

for b_{1} being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds b_{1} is FinSequence-yielding
;

end;
coherence

for b

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

(l,t,n,f) Subst2 phi is wff string of S by Lm42;

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

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;

coherence

for b_{1} being string of S st b_{1} = (l,t,n,f) Subst2 phi holds

b_{1} is wff
;

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

coherence

for b

b

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

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

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

ex b_{1} being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) st

for phi being wff string of S holds b_{1} . phi = (l,t,n,f) Subst2 phi

for b_{1}, b_{2} being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) st ( for phi being wff string of S holds b_{1} . phi = (l,t,n,f) Subst2 phi ) & ( for phi being wff string of S holds b_{2} . phi = (l,t,n,f) Subst2 phi ) holds

b_{1} = b_{2}

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

existence for phi being wff string of S holds it . phi = (l,t,n,f) Subst2 phi;

ex b

for phi being wff string of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def21 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_{6} being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds

( b_{6} = (l,t,n,f) Subst3 iff for phi being wff string of S holds b_{6} . phi = (l,t,n,f) Subst2 phi );

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

( b

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_{1}( Nat, Element of Funcs ((AllFormulasOf S),(AllFormulasOf S))) -> Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) = (l,t,$1,$2) Subst3 ;

ex b_{1} being sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))) st

( b_{1} . 0 = f & ( for m being Nat holds b_{1} . (m + 1) = (l,t,m,(b_{1} . m)) Subst3 ) )

for b_{1}, b_{2} being sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))) st b_{1} . 0 = f & ( for m being Nat holds b_{1} . (m + 1) = (l,t,m,(b_{1} . m)) Subst3 ) & b_{2} . 0 = f & ( for m being Nat holds b_{2} . (m + 1) = (l,t,m,(b_{2} . m)) Subst3 ) holds

b_{1} = b_{2}

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

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

existence ( it . 0 = f & ( for m being Nat holds it . (m + 1) = (l,t,m,(it . m)) Subst3 ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 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_{5} being sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))) holds

( b_{5} = (l,t) Subst4 f iff ( b_{5} . 0 = f & ( for m being Nat holds b_{5} . (m + 1) = (l,t,m,(b_{5} . m)) Subst3 ) ) );

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

( b

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;

ex b_{1} 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_{1} . phi0 = (l,tt) AtomicSubst phi0

for b_{1}, b_{2} 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_{1} . phi0 = (l,tt) AtomicSubst phi0 ) & ( for phi0 being 0wff string of S

for tt being Element of AllTermsOf S st tt = t holds

b_{2} . phi0 = (l,tt) AtomicSubst phi0 ) holds

b_{1} = b_{2}

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

existence for phi0 being 0wff string of S

for tt being Element of AllTermsOf S st tt = t holds

it . phi0 = (l,tt) AtomicSubst phi0;

ex b

for phi0 being 0wff string of S

for tt being Element of AllTermsOf S st tt = t holds

b

proof end;

uniqueness for b

for tt being Element of AllTermsOf S st tt = t holds

b

for tt being Element of AllTermsOf S st tt = t holds

b

b

proof end;

:: deftheorem Def23 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_{4} being Function of (AtomicFormulasOf S),(AtomicFormulasOf S) holds

( b_{4} = l AtomicSubst t iff for phi0 being 0wff string of S

for tt being Element of AllTermsOf S st tt = t holds

b_{4} . phi0 = (l,tt) AtomicSubst phi0 );

for S being Language

for l being literal Element of S

for t being termal string of S

for b

( b

for tt being Element of AllTermsOf S st tt = t holds

b

definition

let S be Language;

let l be literal Element of S;

let t be termal string of S;

coherence

(id (AllFormulasOf S)) +* (l AtomicSubst t) is Function ;

end;
let l be literal Element of S;

let t be termal string of S;

coherence

(id (AllFormulasOf S)) +* (l AtomicSubst t) is Function ;

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

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

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

l Subst1 t is Element of Funcs ((AllFormulasOf S),((AllSymbolsOf S) *))

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

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

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

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;

(((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi is wff string of S

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

(((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi is wff string of S

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

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;

coherence

for b_{1} being string of S st b_{1} = (l,t) SubstIn phi holds

b_{1} is wff
;

end;
let l be literal Element of S;

let t be termal string of S;

let phi be wff string of S;

coherence

for b

b

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;

compatibility

(l,tt) SubstIn phi0 = (l,tt) AtomicSubst phi0

(l,tt) AtomicSubst phi0 = (l,tt) SubstIn phi0 ;

end;
let l be literal Element of S;

let tt be Element of AllTermsOf S;

let phi0 be 0wff string of S;

compatibility

(l,tt) SubstIn phi0 = (l,tt) AtomicSubst phi0

proof end;

compatibility (l,tt) AtomicSubst phi0 = (l,tt) SubstIn phi0 ;

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

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;

coherence

for b_{1} being string of S st b_{1} = (l,t) SubstIn phi holds

b_{1} is m -wff

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

coherence

for b

b

proof end;

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

Lm48: 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 Th12: :: 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 )

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;

Lm49: 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 S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

( X is I1 -satisfied iff X is I2 -satisfied )

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

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 l is X -absent & X is I -satisfied holds

X is (l,u) ReassignIn I -satisfied

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 l is X -absent & 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_{5} -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

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

proof end;

theorem :: FOMODEL3:16

for U being non empty set

for S1, S2 being Language st TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 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 the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) holds

ex phi2 being wff string of S2 st phi1 = phi2

for S1, S2 being Language st TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 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 the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) holds

ex phi2 being wff string of S2 st phi1 = phi2

proof end;

theorem :: FOMODEL3:17

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 S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

( X is I1 -satisfied iff X is I2 -satisfied ) by Lm49;

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 S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

( X is I1 -satisfied iff X is I2 -satisfied ) by Lm49;

Lm50: for X, x being set

for U being non empty set

for R being total reflexive Relation of U

for f being Function of X,U st x in X holds

f is {[x,x]},R -respecting

proof end;

Lm51: for U being non empty set

for S being Language

for l being literal Element of S

for E being total reflexive Relation of U

for f being Interpreter of l,U holds f is E -respecting

proof end;

theorem :: FOMODEL3:18