let S be Language; for U1, U2 being non empty set
for m being Nat
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval m) holds
[I2,w] in dom ((S,U2) -TruthEval m)
let U1, U2 be non empty set ; for m being Nat
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval m) holds
[I2,w] in dom ((S,U2) -TruthEval m)
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set II1 = U1 -InterpretersOf S;
set II2 = U2 -InterpretersOf S;
set AF = AtomicFormulasOf S;
defpred S1[ Nat] means for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval $1) holds
[I2,w] in dom ((S,U2) -TruthEval $1);
A1:
S1[ 0 ]
proof
set f1 = (
S,
U1)
-TruthEval 0;
set f2 = (
S,
U2)
-TruthEval 0;
reconsider Z =
0 as
Element of
NAT ;
reconsider g1 =
((S,U1) -TruthEval) . Z as
Element of
PFuncs (
[:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN) ;
reconsider g2 =
((S,U2) -TruthEval) . Z as
Element of
PFuncs (
[:(U2 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN) ;
A2:
( (
S,
U1)
-TruthEval 0 = g1 & (
S,
U2)
-TruthEval 0 = g2 )
by Def20;
A3:
(
g1 = S -TruthEval U1 &
g2 = S -TruthEval U2 )
by Def19;
A4:
dom ((S,U1) -TruthEval 0) = [:(U1 -InterpretersOf S),(AtomicFormulasOf S):]
by A2, FUNCT_2:def 1, A3;
A5:
dom ((S,U2) -TruthEval 0) = [:(U2 -InterpretersOf S),(AtomicFormulasOf S):]
by A2, FUNCT_2:def 1, A3;
let I1 be
Element of
U1 -InterpretersOf S;
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval 0) holds
[I2,w] in dom ((S,U2) -TruthEval 0)let I2 be
Element of
U2 -InterpretersOf S;
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval 0) holds
[I2,w] in dom ((S,U2) -TruthEval 0)let w be
string of
S;
( [I1,w] in dom ((S,U1) -TruthEval 0) implies [I2,w] in dom ((S,U2) -TruthEval 0) )
assume
[I1,w] in dom ((S,U1) -TruthEval 0)
;
[I2,w] in dom ((S,U2) -TruthEval 0)
then
(
I1 in U1 -InterpretersOf S &
w in AtomicFormulasOf S )
by ZFMISC_1:87, A4;
hence
[I2,w] in dom ((S,U2) -TruthEval 0)
by A5, ZFMISC_1:87;
verum
end;
A6:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
reconsider nn =
n,
NN =
n + 1 as
Element of
NAT by ORDINAL1:def 12;
assume A7:
S1[
n]
;
S1[n + 1]
let I1 be
Element of
U1 -InterpretersOf S;
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval (n + 1)) holds
[I2,w] in dom ((S,U2) -TruthEval (n + 1))let I2 be
Element of
U2 -InterpretersOf S;
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval (n + 1)) holds
[I2,w] in dom ((S,U2) -TruthEval (n + 1))
set f1n = (
S,
U1)
-TruthEval n;
set f1N = (
S,
U1)
-TruthEval (n + 1);
set f2n = (
S,
U2)
-TruthEval n;
set f2N = (
S,
U2)
-TruthEval (n + 1);
A8:
dom ((S,U1) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U1) -TruthEval n))) \/ (dom (NorIterator ((S,U1) -TruthEval n)))) \/ (dom ((S,U1) -TruthEval n))
proof
reconsider g1N =
((S,U1) -TruthEval) . NN as
Element of
PFuncs (
[:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN) ;
reconsider g1n =
((S,U1) -TruthEval) . nn as
Element of
PFuncs (
[:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN) ;
A9:
( (
S,
U1)
-TruthEval n = g1n & (
S,
U1)
-TruthEval (n + 1) = g1N )
by Def20;
then
(
S,
U1)
-TruthEval (n + 1) = ((ExIterator g1n) +* (NorIterator g1n)) +* g1n
by Def19;
then dom ((S,U1) -TruthEval (n + 1)) =
(dom ((ExIterator g1n) +* (NorIterator g1n))) \/ (dom g1n)
by FUNCT_4:def 1
.=
((dom (ExIterator g1n)) \/ (dom (NorIterator g1n))) \/ (dom g1n)
by FUNCT_4:def 1
;
hence
dom ((S,U1) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U1) -TruthEval n))) \/ (dom (NorIterator ((S,U1) -TruthEval n)))) \/ (dom ((S,U1) -TruthEval n))
by A9;
verum
end;
A10:
dom ((S,U2) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U2) -TruthEval n))) \/ (dom (NorIterator ((S,U2) -TruthEval n)))) \/ (dom ((S,U2) -TruthEval n))
proof
reconsider g2N =
((S,U2) -TruthEval) . NN as
Element of
PFuncs (
[:(U2 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN) ;
reconsider g2n =
((S,U2) -TruthEval) . nn as
Element of
PFuncs (
[:(U2 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN) ;
A11:
( (
S,
U2)
-TruthEval n = g2n & (
S,
U2)
-TruthEval (n + 1) = g2N )
by Def20;
then
(
S,
U2)
-TruthEval (n + 1) = ((ExIterator g2n) +* (NorIterator g2n)) +* g2n
by Def19;
then dom ((S,U2) -TruthEval (n + 1)) =
(dom ((ExIterator g2n) +* (NorIterator g2n))) \/ (dom g2n)
by FUNCT_4:def 1
.=
((dom (ExIterator g2n)) \/ (dom (NorIterator g2n))) \/ (dom g2n)
by FUNCT_4:def 1
;
hence
dom ((S,U2) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U2) -TruthEval n))) \/ (dom (NorIterator ((S,U2) -TruthEval n)))) \/ (dom ((S,U2) -TruthEval n))
by A11;
verum
end;
let w be
string of
S;
( [I1,w] in dom ((S,U1) -TruthEval (n + 1)) implies [I2,w] in dom ((S,U2) -TruthEval (n + 1)) )
set x =
[I1,w];
assume A12:
[I1,w] in dom ((S,U1) -TruthEval (n + 1))
;
[I2,w] in dom ((S,U2) -TruthEval (n + 1))
per cases
( [I1,w] in dom (ExIterator ((S,U1) -TruthEval n)) or [I1,w] in dom (NorIterator ((S,U1) -TruthEval n)) or [I1,w] in dom ((S,U1) -TruthEval n) )
by A12, Lm8, A8;
suppose
[I1,w] in dom (ExIterator ((S,U1) -TruthEval n))
;
[I2,w] in dom ((S,U2) -TruthEval (n + 1))then consider v being
literal Element of
S,
ww being
string of
S such that A13:
(
[I1,ww] in dom ((S,U1) -TruthEval n) &
w = <*v*> ^ ww )
by Def16;
(
[I2,ww] in dom ((S,U2) -TruthEval n) &
w = <*v*> ^ ww )
by A13, A7;
then
[I2,w] in dom (ExIterator ((S,U2) -TruthEval n))
by Def16;
hence
[I2,w] in dom ((S,U2) -TruthEval (n + 1))
by Lm8, A10;
verum end; suppose
[I1,w] in dom (NorIterator ((S,U1) -TruthEval n))
;
[I2,w] in dom ((S,U2) -TruthEval (n + 1))then consider phi1,
phi2 being
string of
S such that A14:
(
w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &
[I1,phi1] in dom ((S,U1) -TruthEval n) &
[I1,phi2] in dom ((S,U1) -TruthEval n) )
by Def18;
(
w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &
[I2,phi1] in dom ((S,U2) -TruthEval n) &
[I2,phi2] in dom ((S,U2) -TruthEval n) )
by A14, A7;
then
[I2,w] in dom (NorIterator ((S,U2) -TruthEval n))
by Def18;
hence
[I2,w] in dom ((S,U2) -TruthEval (n + 1))
by Lm8, A10;
verum end;
end;
thus
for m being Nat holds S1[m]
from NAT_1:sch 2(A1, A6); verum