let S be Language; :: thesis: for U being non empty set

for I being S,b_{1} -interpreter-like Function

for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds

( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

let U be non empty set ; :: thesis: for I being S,U -interpreter-like Function

for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds

( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

let I be S,U -interpreter-like Function; :: thesis: for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds

( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

let phi be 0wff string of S; :: thesis: ( (S -firstChar) . phi = TheEqSymbOf S implies ( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) ) )

set E = TheEqSymbOf S;

set p = SubTerms phi;

set F = S -firstChar ;

set s = (S -firstChar) . phi;

set UV = I -TermEval ;

set V = I -AtomicEval phi;

set d = U -deltaInterpreter ;

set U2 = 2 -tuples_on U;

set TT = AllTermsOf S;

set D = { <*u,u*> where u is Element of U : verum } ;

set n = |.(ar ((S -firstChar) . phi)).|;

A1: 2 -tuples_on U = { <*u1,u2*> where u1, u2 is Element of U : verum } by FINSEQ_2:99;

A2: |.(ar (TheEqSymbOf S)).| - 2 = 0 ;

reconsider r = (S -firstChar) . phi as relational Element of S ;

set f = (I ===) . r;

reconsider EE = TheEqSymbOf S as relational Element of S ;

assume A3: (S -firstChar) . phi = TheEqSymbOf S ; :: thesis: ( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

then ( I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) & |.(ar ((S -firstChar) . phi)).| = 2 ) by Th14, A2;

then ( I -AtomicEval phi = 1 iff (I -TermEval) * (SubTerms phi) in (U -deltaInterpreter) " {1} ) by FOMODEL0:25;

then A4: ( I -AtomicEval phi = 1 iff (I -TermEval) * (SubTerms phi) in { <*u,u*> where u is Element of U : verum } ) by Th13;

reconsider pp = SubTerms phi as 2 -element FinSequence of AllTermsOf S by FINSEQ_1:def 11, A3, A2;

reconsider q = (I -TermEval) * pp as FinSequence of U ;

reconsider qq = q as Element of 2 -tuples_on U by FOMODEL0:16;

qq in 2 -tuples_on U ;

then consider u1, u2 being Element of U such that

A5: qq = <*u1,u2*> by A1;

A6: ( qq . 1 = u1 & qq . 2 = u2 ) by A5, FINSEQ_1:44;

1 <= 2 ;

then ( 1 <= 1 & 1 <= len q & 1 <= 2 & 2 <= len q ) by CARD_1:def 7;

then ( 1 in Seg (len q) & 2 in Seg (len q) ) ;

then ( 1 in dom q & 2 in dom q ) by FINSEQ_1:def 3;

then A7: ( q . 1 = (I -TermEval) . ((SubTerms phi) . 1) & q . 2 = (I -TermEval) . ((SubTerms phi) . 2) ) by FUNCT_1:12;

( q in { <*u,u*> where u is Element of U : verum } implies (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

for I being S,b

for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds

( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

let U be non empty set ; :: thesis: for I being S,U -interpreter-like Function

for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds

( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

let I be S,U -interpreter-like Function; :: thesis: for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds

( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

let phi be 0wff string of S; :: thesis: ( (S -firstChar) . phi = TheEqSymbOf S implies ( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) ) )

set E = TheEqSymbOf S;

set p = SubTerms phi;

set F = S -firstChar ;

set s = (S -firstChar) . phi;

set UV = I -TermEval ;

set V = I -AtomicEval phi;

set d = U -deltaInterpreter ;

set U2 = 2 -tuples_on U;

set TT = AllTermsOf S;

set D = { <*u,u*> where u is Element of U : verum } ;

set n = |.(ar ((S -firstChar) . phi)).|;

A1: 2 -tuples_on U = { <*u1,u2*> where u1, u2 is Element of U : verum } by FINSEQ_2:99;

A2: |.(ar (TheEqSymbOf S)).| - 2 = 0 ;

reconsider r = (S -firstChar) . phi as relational Element of S ;

set f = (I ===) . r;

reconsider EE = TheEqSymbOf S as relational Element of S ;

assume A3: (S -firstChar) . phi = TheEqSymbOf S ; :: thesis: ( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

then ( I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) & |.(ar ((S -firstChar) . phi)).| = 2 ) by Th14, A2;

then ( I -AtomicEval phi = 1 iff (I -TermEval) * (SubTerms phi) in (U -deltaInterpreter) " {1} ) by FOMODEL0:25;

then A4: ( I -AtomicEval phi = 1 iff (I -TermEval) * (SubTerms phi) in { <*u,u*> where u is Element of U : verum } ) by Th13;

reconsider pp = SubTerms phi as 2 -element FinSequence of AllTermsOf S by FINSEQ_1:def 11, A3, A2;

reconsider q = (I -TermEval) * pp as FinSequence of U ;

reconsider qq = q as Element of 2 -tuples_on U by FOMODEL0:16;

qq in 2 -tuples_on U ;

then consider u1, u2 being Element of U such that

A5: qq = <*u1,u2*> by A1;

A6: ( qq . 1 = u1 & qq . 2 = u2 ) by A5, FINSEQ_1:44;

1 <= 2 ;

then ( 1 <= 1 & 1 <= len q & 1 <= 2 & 2 <= len q ) by CARD_1:def 7;

then ( 1 in Seg (len q) & 2 in Seg (len q) ) ;

then ( 1 in dom q & 2 in dom q ) by FINSEQ_1:def 3;

then A7: ( q . 1 = (I -TermEval) . ((SubTerms phi) . 1) & q . 2 = (I -TermEval) . ((SubTerms phi) . 2) ) by FUNCT_1:12;

( q in { <*u,u*> where u is Element of U : verum } implies (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

proof

hence
( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )
by A4, A7, A5, A6; :: thesis: verum
assume
q in { <*u,u*> where u is Element of U : verum }
; :: thesis: (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2)

then consider u being Element of U such that

A8: <*u,u*> = q ;

( q . 1 = u & q . 2 = u ) by A8, FINSEQ_1:44;

hence (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) by A7; :: thesis: verum

end;then consider u being Element of U such that

A8: <*u,u*> = q ;

( q . 1 = u & q . 2 = u ) by A8, FINSEQ_1:44;

hence (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) by A7; :: thesis: verum