let S be Language; :: thesis: R3d S is Correct

now

set f = R3d S;
set R = P3d S;
set Q = S -sequents ;
set E = TheEqSymbOf S;
set N = TheNorSymbOf S;
set FF = AllFormulasOf S;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
let X be set ; :: thesis: ( X is S -correct implies (R3d S) . X is S -correct )
assume B0: X is S -correct ; :: thesis: (R3d S) . X is S -correct

now

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S
for x being b₁ -satisfied set
for psi being wff string of S st [x,psi] in (R3d S) . X holds
I -TruthEval psi = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: for x being I -satisfied set
for psi being wff string of S st [x,psi] in (R3d S) . X holds
I -TruthEval psi = 1
let x be I -satisfied set ; :: thesis: for psi being wff string of S st [x,psi] in (R3d S) . X holds
I -TruthEval psi = 1
let psi be wff string of S; :: thesis: ( [x,psi] in (R3d S) . X implies I -TruthEval psi = 1 )
set s = [x,psi];
set TE = I -TermEval ;
set d = U -deltaInterpreter ;
CC0: ( ([x,psi] `1) \+\ x = {} & ([x,psi] `2) \+\ psi = {} ) ;
assume DD1: [x,psi] in (R3d S) . X ; :: thesis: I -TruthEval psi = 1
then D1: ( [x,psi] in S -sequents & [X,[x,psi]] in P3d S ) by Lm1e;
then X in dom (P3d S) by RELAT_1:def 4;
then reconsider Seqts = X as S -correct Subset of (S -sequents) by B0;
reconsider seqt = [x,psi] as Element of S -sequents by DD1, Lm1e;
seqt Rule3d Seqts by D1, DefP3d;
then consider r being low-compounding Element of S, T1, T2 being abs (ar r) -element Element of (AllTermsOf S) * such that
D2: ( r is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg (abs (ar r)), TT1, TT2 is Function of (Seg (abs (ar r))),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (r -compound T1)) ^ (r -compound T2) ) by Def3d;
reconsider t1 = r -compound T1, t2 = r -compound T2 as termal string of S by D2;
( (t1 . 1) \+\ r = {} & (t2 . 1) \+\ r = {} ) ;
then ( t1 . 1 = r & t2 . 1 = r ) by FOMODEL0:29;
then D3: ( (S -firstChar) . t1 = r & (S -firstChar) . t2 = r ) by FOMODEL0:6;
then ( SubTerms t1 = T1 & SubTerms t2 = T2 ) by FOMODEL1:def 37;
then D4: ( (I -TermEval) . t1 = (I . r) . ((I -TermEval) * T1) & (I -TermEval) . t2 = (I . r) . ((I -TermEval) * T2) ) by D3, FOMODEL2:21;
reconsider Fam = { ((<*(TheEqSymbOf S)*> ^ (TT1 . j)) ^ (TT2 . j)) where j is Element of Seg (abs (ar r)), TT1, TT2 is Function of (Seg (abs (ar r))),(((AllSymbolsOf S) *) \ {{}}) : ( TT1 = T1 & TT2 = T2 ) } null {} as Subset of x by D2, CC0, FOMODEL0:29;

now

set p = (I -TermEval) * T1;
set q = (I -TermEval) * T2;
len ((I -TermEval) * T1) = abs (ar r) by CARD_1:def 7;
hence len ((I -TermEval) * T2) = len ((I -TermEval) * T1) by CARD_1:def 7; :: thesis: for k being Nat st 1 <= k & k <= len ((I -TermEval) * T1) holds
((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len ((I -TermEval) * T1) implies ((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k )
assume EE0: ( 1 <= k & k <= len ((I -TermEval) * T1) ) ; :: thesis: ((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k
then E0: ( 1 <= k & k <= abs (ar r) ) by CARD_1:def 7;
then reconsider kk = k as Element of Seg (abs (ar r)) by FINSEQ_1:1;
k - k <= (abs (ar r)) - k by E0, XREAL_1:9;
then reconsider h = (abs (ar r)) - k as Nat ;
reconsider k1 = k as non zero Nat by EE0;
( dom (T1 null 0) = Seg ((abs (ar r)) + 0) & rng T1 c= ((AllSymbolsOf S) *) \ {{}} & dom (T2 null 0) = Seg ((abs (ar r)) + 0) & rng T2 c= ((AllSymbolsOf S) *) \ {{}} ) by PARTFUN1:def 2, RELAT_1:def 19;
then ( T1 is Element of Funcs ((Seg (abs (ar r))),(((AllSymbolsOf S) *) \ {{}})) & T2 is Element of Funcs ((Seg (abs (ar r))),(((AllSymbolsOf S) *) \ {{}})) ) by FUNCT_2:def 2;
then reconsider TT1 = T1, TT2 = T2 as Function of (Seg (abs (ar r))),(((AllSymbolsOf S) *) \ {{}}) ;
( T1 is k1 + h -element & T2 is k1 + h -element ) ;
then ( {(T1 . k1)} \ (AllTermsOf S) = {} & {(T2 . k1)} \ (AllTermsOf S) = {} ) ;
then ( T1 . k in AllTermsOf S & T2 . k in AllTermsOf S ) by ZFMISC_1:60;
then reconsider t1 = T1 . k, t2 = T2 . k as termal string of S ;
reconsider z = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as 0wff string of S ;
( ((I -TermEval) . (TT1 . kk)) \+\ (((I -TermEval) * TT1) . kk) = {} & ((I -TermEval) . (TT2 . kk)) \+\ (((I -TermEval) * TT2) . kk) = {} ) ;
then E1: ( (I -TermEval) . (TT1 . kk) = ((I -TermEval) * TT1) . kk & (I -TermEval) . (TT2 . kk) = ((I -TermEval) * TT2) . kk ) by FOMODEL0:29;
set ST = <*t1,t2*>;
(<*(TheEqSymbOf S)*> ^ (TT1 . kk)) ^ (TT2 . kk) in Fam ;
then I -TruthEval z = 1 by FOMODEL2:def 42;
hence ((I -TermEval) * T1) . k = ((I -TermEval) * T2) . k by E1, Lm36; :: thesis: verum

end;

then (I -TermEval) . t1 = (I -TermEval) . t2 by D4, FINSEQ_1:14;
then ( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 & psi = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 ) by Lm36, CC0, D2, FOMODEL0:29;
hence I -TruthEval psi = 1 ; :: thesis: verum

end;

hence (R3d S) . X is S -correct by FOMODEL2:def 44; :: thesis: verum

end;

hence R3d S is Correct by RuleCorr; :: thesis: verum