let U be non empty set ; :: thesis: for S being Language
for t1, t2 being termal string of S
for I being b₁,U -interpreter-like Function holds
( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 iff (I -TermEval) . t1 = (I -TermEval) . t2 )
let S be Language; :: thesis: for t1, t2 being termal string of S
for I being S,U -interpreter-like Function holds
( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 iff (I -TermEval) . t1 = (I -TermEval) . t2 )
let t1, t2 be termal string of S; :: thesis: for I being S,U -interpreter-like Function holds
( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 iff (I -TermEval) . t1 = (I -TermEval) . t2 )
set E = TheEqSymbOf S;
set phi0 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2;
set ST = SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2);
set F = S -firstChar ;
( (<*(TheEqSymbOf S)*> ^ t1) ^ t2 = <*(TheEqSymbOf S)*> ^ (t1 ^ t2) & ((<*(TheEqSymbOf S)*> ^ (t1 ^ t2)) . 1) \+\ (TheEqSymbOf S) = {} ) by FINSEQ_1:32;
then A1: TheEqSymbOf S = ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) . 1 by FOMODEL0:29
.= (S -firstChar) . ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) by FOMODEL0:6 ;
(SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> = {} ;
then SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = <*t1,t2*> by FOMODEL0:29;
then ( (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) . 1 = t1 & (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) . 2 = t2 ) by FINSEQ_1:44;
hence for I being S,U -interpreter-like Function holds
( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 iff (I -TermEval) . t1 = (I -TermEval) . t2 ) by A1, FOMODEL2:15; :: thesis: verum