let Al be QC-alphabet ; :: thesis: for PHI being Consistent Subset of (CQC-WFF Al) ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
( PHI c= PSI & PSI is with_examples )
let PHI be Consistent Subset of (CQC-WFF Al); :: thesis: ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
( PHI c= PSI & PSI is with_examples )
deffunc H1( Nat) -> Al -expanding QC-alphabet = $1 -th_FCEx Al;
deffunc H2( Nat) -> Subset of (CQC-WFF ($1 -th_FCEx Al)) = $1 -th_EF (Al,PHI);
set Al2 = union { H1(n) where n is Element of NAT : verum } ;
set PSI = union { H2(n) where n is Element of NAT : verum } ;
A1: PHI c= union { H2(n) where n is Element of NAT : verum }
proof
PHI = H2( 0 ) by Def9;
then PHI in { H2(n) where n is Element of NAT : verum } ;
hence PHI c= union { H2(n) where n is Element of NAT : verum } by ZFMISC_1:74; :: thesis: verum
end;
A2: ( Al c= union { H1(n) where n is Element of NAT : verum } & ( for n being Element of NAT holds H1(n) c= union { H1(n) where n is Element of NAT : verum } ) )
proof
Al = H1( 0 ) by Def7;
then Al in { H1(n) where n is Element of NAT : verum } ;
hence Al c= union { H1(n) where n is Element of NAT : verum } by ZFMISC_1:74; :: thesis: for n being Element of NAT holds H1(n) c= union { H1(n) where n is Element of NAT : verum }
let n be Element of NAT ; :: thesis: H1(n) c= union { H1(n) where n is Element of NAT : verum }
H1(n) in { H1(k) where k is Element of NAT : verum } ;
hence H1(n) c= union { H1(n) where n is Element of NAT : verum } by ZFMISC_1:74; :: thesis: verum
end;
reconsider Al2 = union { H1(n) where n is Element of NAT : verum } as non empty set by A2;
set Al2sym = union { (QC-symbols H1(n)) where n is Element of NAT : verum } ;
( NAT c= union { (QC-symbols H1(n)) where n is Element of NAT : verum } & Al2 = [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] )
proof
for s being object st s in Al2 holds
s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
proof
let s be object ; :: thesis: ( s in Al2 implies s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] )
assume A3: s in Al2 ; :: thesis: s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
consider P being set such that
A4: ( s in P & P in { H1(n) where n is Element of NAT : verum } ) by A3, TARSKI:def 4;
consider n being Element of NAT such that
A5: P = H1(n) by A4;
A6: for y being set st y in QC-symbols H1(n) holds
y in union { (QC-symbols H1(n)) where n is Element of NAT : verum }
proof
let y be set ; :: thesis: ( y in QC-symbols H1(n) implies y in union { (QC-symbols H1(n)) where n is Element of NAT : verum } )
assume A7: y in QC-symbols H1(n) ; :: thesis: y in union { (QC-symbols H1(n)) where n is Element of NAT : verum }
QC-symbols H1(n) in { (QC-symbols H1(k)) where k is Element of NAT : verum } ;
hence y in union { (QC-symbols H1(n)) where n is Element of NAT : verum } by A7, TARSKI:def 4; :: thesis: verum
end;
s in [:NAT,(QC-symbols H1(n)):] by A5, A4, QC_LANG1:5;
then ex k, y being object st
( k in NAT & y in QC-symbols H1(n) & s = [k,y] ) by ZFMISC_1:def 2;
then ex k, y being set st
( k in NAT & y in union { (QC-symbols H1(n)) where n is Element of NAT : verum } & s = [k,y] ) by A6;
hence s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] by ZFMISC_1:87; :: thesis: verum
end;
then A8: Al2 c= [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] ;
QC-symbols Al = QC-symbols H1( 0 ) by Def7;
then QC-symbols Al in { (QC-symbols H1(n)) where n is Element of NAT : verum } ;
then ( NAT c= QC-symbols Al & QC-symbols Al c= union { (QC-symbols H1(n)) where n is Element of NAT : verum } ) by QC_LANG1:3, ZFMISC_1:74;
hence NAT c= union { (QC-symbols H1(n)) where n is Element of NAT : verum } ; :: thesis: Al2 = [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
for x being object st x in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] holds
x in Al2
proof
let x be object ; :: thesis: ( x in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] implies x in Al2 )
assume A9: x in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] ; :: thesis: x in Al2
consider m, y being object such that
A10: ( m in NAT & y in union { (QC-symbols H1(n)) where n is Element of NAT : verum } & x = [m,y] ) by A9, ZFMISC_1:def 2;
consider P being set such that
A11: ( y in P & P in { (QC-symbols H1(n)) where n is Element of NAT : verum } ) by A10, TARSKI:def 4;
consider n being Element of NAT such that
A12: P = QC-symbols H1(n) by A11;
[m,y] in [:NAT,(QC-symbols H1(n)):] by A10, A11, A12, ZFMISC_1:87;
then A13: [m,y] in H1(n) by QC_LANG1:5;
H1(n) c= Al2 by A2;
hence x in Al2 by A10, A13; :: thesis: verum
end;
then [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] c= Al2 ;
hence Al2 = [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] by A8, XBOOLE_0:def 10; :: thesis: verum
end;
then reconsider Al2 = Al2 as QC-alphabet by QC_LANG1:def 1;
reconsider Al2 = Al2 as Al -expanding QC-alphabet by A2, QC_TRANS:def 1;
for p being object st p in union { H2(n) where n is Element of NAT : verum } holds
p in CQC-WFF Al2
proof
let p be object ; :: thesis: ( p in union { H2(n) where n is Element of NAT : verum } implies p in CQC-WFF Al2 )
assume A14: p in union { H2(n) where n is Element of NAT : verum } ; :: thesis: p in CQC-WFF Al2
consider P being set such that
A15: ( p in P & P in { H2(n) where n is Element of NAT : verum } ) by A14, TARSKI:def 4;
consider n being Element of NAT such that
A16: P = H2(n) by A15;
Al2 is H1(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;
then p is Element of CQC-WFF Al2 by QC_TRANS:7, A15, A16;
hence p in CQC-WFF Al2 ; :: thesis: verum
end;
then reconsider PSI = union { H2(n) where n is Element of NAT : verum } as Subset of (CQC-WFF Al2) by TARSKI:def 3;
PSI is Consistent
proof
defpred S1[ Nat] means ( H2($1) is Consistent & H2($1) is Al2 -Consistent );
A17: S1[ 0 ]
proof
A18: H2( 0 ) = PHI by Def9;
PHI is Al2 -Consistent by QC_TRANS:23;
then ( H1( 0 ) = Al & ( for S being Subset of (CQC-WFF Al2) st H2( 0 ) = S holds
S is Consistent ) ) by A18, Def7, QC_TRANS:def 2;
hence S1[ 0 ] by A18, QC_TRANS:def 2; :: thesis: verum
end;
A19: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
A20: FCEx H1(n) = H1(n + 1) by Th5;
reconsider Al2 = Al2 as H1(n + 1) -expanding QC-alphabet by A2, QC_TRANS:def 1;
assume S1[n] ; :: thesis: S1[n + 1]
then reconsider PSIn = H2(n) as Consistent Subset of (CQC-WFF H1(n)) ;
H2(n + 1) = PSIn \/ (Example_Formulae_of H1(n)) by Def9;
then reconsider PSIn1 = H2(n + 1) as Consistent Subset of (CQC-WFF H1(n + 1)) by A20, Th9;
PSIn1 is Al2 -Consistent by QC_TRANS:23;
hence S1[n + 1] ; :: thesis: verum
end;
A21: for n being Nat holds S1[n] from NAT_1:sch 2(A17, A19);
 A22: for n being Element of NAT holds H2(n) c= PSI
proof
let n be Element of NAT ; :: thesis: H2(n) c= PSI
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in H2(n) or p in PSI )
assume A23: p in H2(n) ; :: thesis: p in PSI
H2(n) in { H2(k) where k is Element of NAT : verum } ;
hence p in PSI by A23, TARSKI:def 4; :: thesis: verum
end;
A24: for n being Element of NAT holds H2(n) in bool (CQC-WFF Al2)
proof
let n be Element of NAT ; :: thesis: H2(n) in bool (CQC-WFF Al2)
( H2(n) c= PSI & PSI c= CQC-WFF Al2 ) by A22;
then H2(n) c= CQC-WFF Al2 ;
hence H2(n) in bool (CQC-WFF Al2) ; :: thesis: verum
end;
consider f being Function such that
A25: ( dom f = NAT & ( for n being Element of NAT holds f . n = H2(n) ) ) from FUNCT_1:sch 4();
 for y being object st y in rng f holds
y in bool (CQC-WFF Al2)
proof
let y be object ; :: thesis: ( y in rng f implies y in bool (CQC-WFF Al2) )
assume A26: y in rng f ; :: thesis: y in bool (CQC-WFF Al2)
consider x being object such that
A27: ( x in dom f & y = f . x ) by A26, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A25, A27;
f . x = H2(x) by A25;
hence y in bool (CQC-WFF Al2) by A24, A27; :: thesis: verum
end;
then reconsider f = f as sequence of (bool (CQC-WFF Al2)) by A25, FUNCT_2:2, TARSKI:def 3;
set PSIp = union (rng f);
f in Funcs (NAT,(bool (CQC-WFF Al2))) by FUNCT_2:8;
then union (rng f) c= union (bool (CQC-WFF Al2)) by ZFMISC_1:77, FUNCT_2:92;
then reconsider PSIp = union (rng f) as Subset of (CQC-WFF Al2) by ZFMISC_1:81;
for n, m being Nat st m in dom f & n in dom f & n < m holds
( f . n is Consistent & f . n c= f . m )
proof
let nn, mm be Nat; :: thesis: ( mm in dom f & nn in dom f & nn < mm implies ( f . nn is Consistent & f . nn c= f . mm ) )
assume A28: ( mm in dom f & nn in dom f & nn < mm ) ; :: thesis: ( f . nn is Consistent & f . nn c= f . mm )
reconsider n = nn, m = mm as Element of NAT by ORDINAL1:def 12;
( f . n is Subset of (CQC-WFF Al2) & f . n = H2(n) & H2(n) is Al2 -Consistent ) by A21, A25;
hence f . nn is Consistent by QC_TRANS:def 2; :: thesis: f . nn c= f . mm
defpred S2[ Nat] means ( $1 <= m implies ex k being Element of NAT st
( k = m - $1 & H2(k) c= H2(m) ) );
A29: S2[ 0 ] ;
A30: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A31: S2[k] ; :: thesis: S2[k + 1]
set j1 = m - k;
set j2 = m - (k + 1);
per cases ( k + 1 <= m or not k + 1 <= m ) ;
suppose A32: k + 1 <= m ; :: thesis: S2[k + 1]
then k <= m by NAT_1:13;
then reconsider j1 = m - k, j2 = m - (k + 1) as Element of NAT by A32, NAT_1:21;
H2(j2 + 1) = ( the EF-Sequence of Al,PHI . j2) \/ (Example_Formulae_of (j2 -th_FCEx Al)) by Def9;
then ( H2(j2) c= H2(j1) & H2(j1) c= H2(m) ) by A31, A32, NAT_1:13, XBOOLE_1:7;
hence S2[k + 1] by XBOOLE_1:1; :: thesis: verum
end;
suppose not k + 1 <= m ; :: thesis: S2[k + 1]
hence S2[k + 1] ; :: thesis: verum
end;
end;
end;
A33: for k being Nat holds S2[k] from NAT_1:sch 2(A29, A30);
 set k = m - n;
reconsider k = m - n as Element of NAT by A28, NAT_1:21;
( S2[k] & k <= k + n ) by A33, NAT_1:11;
then ( H2(n) c= H2(m) & f . n = H2(n) & f . m = H2(m) ) by A25;
hence f . nn c= f . mm ; :: thesis: verum
end;
then reconsider PSIp = PSIp as Consistent Subset of (CQC-WFF Al2) by HENMODEL:11;
for y being object st y in { H2(n) where n is Element of NAT : verum } holds
ex x being object st
( x in dom f & y = f . x )
proof
let P be object ; :: thesis: ( P in { H2(n) where n is Element of NAT : verum } implies ex x being object st
( x in dom f & P = f . x ) )
assume A34: P in { H2(n) where n is Element of NAT : verum } ; :: thesis: ex x being object st
( x in dom f & P = f . x )
consider n being Element of NAT such that
A35: P = H2(n) by A34;
( n in dom f & f . n = P ) by A25, A35;
hence ex x being object st
( x in dom f & P = f . x ) ; :: thesis: verum
end;
then A36: { H2(n) where n is Element of NAT : verum } c= rng f by FUNCT_1:9;
for y being object st y in rng f holds
y in { H2(n) where n is Element of NAT : verum }
proof
let y be object ; :: thesis: ( y in rng f implies y in { H2(n) where n is Element of NAT : verum } )
assume A37: y in rng f ; :: thesis: y in { H2(n) where n is Element of NAT : verum }
consider x being object such that
A38: ( x in dom f & y = f . x ) by A37, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A25, A38;
f . x = H2(x) by A25;
hence y in { H2(n) where n is Element of NAT : verum } by A38; :: thesis: verum
end;
then rng f c= { H2(n) where n is Element of NAT : verum } ;
then PSIp = PSI by A36, XBOOLE_0:def 10;
hence PSI is Consistent ; :: thesis: verum
end;
then reconsider PSI = PSI as Consistent Subset of (CQC-WFF Al2) ;
set S = { H1(n) where n is Element of NAT : verum } ;
H1( 0 ) in { H1(n) where n is Element of NAT : verum } ;
then reconsider S = { H1(n) where n is Element of NAT : verum } as non empty set ;
A39: for a, b being set st a in S & b in S holds
ex c being set st
( a \/ b c= c & c in S )
proof
let a, b be set ; :: thesis: ( a in S & b in S implies ex c being set st
( a \/ b c= c & c in S ) )
assume A40: ( a in S & b in S ) ; :: thesis: ex c being set st
( a \/ b c= c & c in S )
consider i being Element of NAT such that
A41: a = H1(i) by A40;
consider j being Element of NAT such that
A42: b = H1(j) by A40;
per cases ( j <= i or not j <= i ) ;
suppose j <= i ; :: thesis: ex c being set st
( a \/ b c= c & c in S )
then H1(j) c= H1(i) by Th6;
hence ex c being set st
( a \/ b c= c & c in S ) by A40, A41, A42, XBOOLE_1:8; :: thesis: verum
end;
suppose not j <= i ; :: thesis: ex c being set st
( a \/ b c= c & c in S )
then H1(i) c= H1(j) by Th6;
hence ex c being set st
( a \/ b c= c & c in S ) by A40, A41, A42, XBOOLE_1:8; :: thesis: verum
end;
end;
end;
A43: for p being Element of CQC-WFF Al2 ex n being Element of NAT st p is Element of CQC-WFF H1(n)
proof
defpred S1[ Element of CQC-WFF Al2] means ex n being Element of NAT st $1 is Element of CQC-WFF H1(n);
A44: S1[ VERUM Al2]
proof
reconsider Al2 = Al2 as H1( 0 ) -expanding QC-alphabet by A2, QC_TRANS:def 1;
VERUM H1( 0 ) in CQC-WFF H1( 0 ) ;
then Al2 -Cast (VERUM H1( 0 )) in CQC-WFF H1( 0 ) by QC_TRANS:def 3;
then VERUM Al2 in CQC-WFF H1( 0 ) by QC_TRANS:8;
hence S1[ VERUM Al2] ; :: thesis: verum
end;
A45: for k being Nat
for P being QC-pred_symbol of k,Al2
for l being CQC-variable_list of k,Al2 holds S1[P ! l]
proof
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al2
for l being CQC-variable_list of k,Al2 holds S1[P ! l]
let P be QC-pred_symbol of k,Al2; :: thesis: for l being CQC-variable_list of k,Al2 holds S1[P ! l]
let l be CQC-variable_list of k,Al2; :: thesis: S1[P ! l]
ex n being Element of NAT st
( rng l c= bound_QC-variables H1(n) & P is QC-pred_symbol of k,H1(n) )
proof
A46: ( rng l c= bound_QC-variables Al2 & {P} c= QC-pred_symbols Al2 ) by ZFMISC_1:31;
( bound_QC-variables Al2 c= QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;
then A47: ( bound_QC-variables Al2 c= [:NAT,(QC-symbols Al2):] & QC-pred_symbols Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:6;
then ( rng l c= [:NAT,(QC-symbols Al2):] & {P} c= [:NAT,(QC-symbols Al2):] ) by A46;
then ( rng l c= Al2 & {P} c= Al2 ) by QC_LANG1:5;
then ( (rng l) \/ {P} c= union S & (rng l) \/ {P} is finite ) by XBOOLE_1:8;
then consider a being set such that
A48: ( a in S & (rng l) \/ {P} c= a ) by A39, COHSP_1:6, COHSP_1:13;
consider n being Element of NAT such that
A49: a = H1(n) by A48;
take n ; :: thesis: ( rng l c= bound_QC-variables H1(n) & P is QC-pred_symbol of k,H1(n) )
A50: ( rng l c= (rng l) \/ {P} & {P} c= (rng l) \/ {P} ) by XBOOLE_1:7;
for s being object st s in rng l holds
s in bound_QC-variables H1(n)
proof
let s be object ; :: thesis: ( s in rng l implies s in bound_QC-variables H1(n) )
assume A51: s in rng l ; :: thesis: s in bound_QC-variables H1(n)
s in bound_QC-variables Al2 by A51;
then s in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;
then consider s1, s2 being object such that
A52: ( s1 in {4} & s2 in QC-symbols Al2 & s = [s1,s2] ) by ZFMISC_1:def 2;
( rng l c= H1(n) & {P} c= H1(n) ) by A48, A49, A50;
then s in H1(n) by A51;
then s in [:NAT,(QC-symbols H1(n)):] by QC_LANG1:5;
then consider s3, s4 being object such that
A53: ( s3 in NAT & s4 in QC-symbols H1(n) & s = [s3,s4] ) by ZFMISC_1:def 2;
s = [s1,s4] by A52, A53, XTUPLE_0:1;
then s in [:{4},(QC-symbols H1(n)):] by A52, A53, ZFMISC_1:def 2;
hence s in bound_QC-variables H1(n) by QC_LANG1:def 4; :: thesis: verum
end;
hence rng l c= bound_QC-variables H1(n) ; :: thesis: P is QC-pred_symbol of k,H1(n)
thus P is QC-pred_symbol of k,H1(n) :: thesis: verum
proof
P in [:NAT,(QC-symbols Al2):] by A47;
then consider p1, p2 being object such that
A54: ( p1 in NAT & p2 in QC-symbols Al2 & P = [p1,p2] ) by ZFMISC_1:def 2;
( rng l c= H1(n) & P in H1(n) ) by A48, A49, A50, ZFMISC_1:31;
then P in [:NAT,(QC-symbols H1(n)):] by QC_LANG1:5;
then reconsider p2 = p2 as QC-symbol of H1(n) by A54, ZFMISC_1:87;
A55: P `1 = (the_arity_of P) + 7 by QC_LANG1:def 8
.= k + 7 by QC_LANG1:11 ;
reconsider p1 = p1 as Element of NAT by A54;
( P `1 = 7 + (the_arity_of P) & P `1 = p1 ) by A54, QC_LANG1:def 8;
then 7 <= p1 by NAT_1:11;
then [p1,p2] in { [m,x] where m is Nat, x is QC-symbol of H1(n) : 7 <= m } ;
then reconsider P = P as QC-pred_symbol of H1(n) by A54, QC_LANG1:def 7;
the_arity_of P = k by A55, QC_LANG1:def 8;
then P in { Q where Q is QC-pred_symbol of H1(n) : the_arity_of Q = k } ;
hence P is QC-pred_symbol of k,H1(n) by QC_LANG1:def 9; :: thesis: verum
end;
end;
then consider n being Element of NAT such that
A56: ( rng l c= bound_QC-variables H1(n) & P is QC-pred_symbol of k,H1(n) ) ;
l is CQC-variable_list of k,H1(n) by A56, FINSEQ_1:def 4, XBOOLE_1:1;
then consider l2 being CQC-variable_list of k,H1(n), P2 being QC-pred_symbol of k,H1(n) such that
A57: ( l2 = l & P = P2 ) by A56;
reconsider Al2 = Al2 as H1(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;
A58: ( Al2 -Cast P2 = P & Al2 -Cast l2 = l ) by A57, QC_TRANS:def 5, QC_TRANS:def 6;
P2 ! l2 = Al2 -Cast (P2 ! l2) by QC_TRANS:def 3
.= P ! l by A58, QC_TRANS:8 ;
hence S1[P ! l] ; :: thesis: verum
end;
A59: for r being Element of CQC-WFF Al2 st S1[r] holds
S1[ 'not' r]
proof
let r be Element of CQC-WFF Al2; :: thesis: ( S1[r] implies S1[ 'not' r] )
assume S1[r] ; :: thesis: S1[ 'not' r]
then consider n being Element of NAT such that
A60: r is Element of CQC-WFF H1(n) ;
consider r2 being Element of CQC-WFF H1(n) such that
A61: r = r2 by A60;
reconsider Al2 = Al2 as H1(n) -expanding QC-alphabet by A2, QC_TRANS:def 1;
'not' r2 = Al2 -Cast ('not' r2) by QC_TRANS:def 3
.= 'not' (Al2 -Cast r2) by QC_TRANS:8
.= 'not' r by A61, QC_TRANS:def 3 ;
hence S1[ 'not' r] ; :: thesis: verum
end;
A62: for r, s being Element of CQC-WFF Al2 st S1[r] & S1[s] holds
S1[r '&' s]
proof
let r, s be Element of CQC-WFF Al2; :: thesis: ( S1[r] & S1[s] implies S1[r '&' s] )
assume ( S1[r] & S1[s] ) ; :: thesis: S1[r '&' s]
then consider n, m being Element of NAT such that
A63: ( r is Element of CQC-WFF H1(n) & s is Element of CQC-WFF H1(m) ) ;
per cases ( n <= m or not n <= m ) ;
suppose n <= m ; :: thesis: S1[r '&' s]
then reconsider Sm = H1(m) as H1(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;
r is Element of CQC-WFF Sm by A63, QC_TRANS:7;
then consider r2, s2 being Element of CQC-WFF Sm such that
A64: ( r2 = r & s2 = s ) by A63;
reconsider Al2 = Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;
A65: ( r = Al2 -Cast r2 & s = Al2 -Cast s2 ) by A64, QC_TRANS:def 3;
r2 '&' s2 = Al2 -Cast (r2 '&' s2) by QC_TRANS:def 3
.= r '&' s by A65, QC_TRANS:8 ;
hence S1[r '&' s] ; :: thesis: verum
end;
suppose not n <= m ; :: thesis: S1[r '&' s]
then reconsider Sn = H1(n) as H1(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;
s is Element of CQC-WFF Sn by A63, QC_TRANS:7;
then consider r2, s2 being Element of CQC-WFF Sn such that
A66: ( r2 = r & s2 = s ) by A63;
reconsider Al2 = Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;
A67: ( r = Al2 -Cast r2 & s = Al2 -Cast s2 ) by A66, QC_TRANS:def 3;
r2 '&' s2 = Al2 -Cast (r2 '&' s2) by QC_TRANS:def 3
.= r '&' s by A67, QC_TRANS:8 ;
hence S1[r '&' s] ; :: thesis: verum
end;
end;
end;
for x being bound_QC-variable of Al2
for r being Element of CQC-WFF Al2 st S1[r] holds
S1[ All (x,r)]
proof
let x be bound_QC-variable of Al2; :: thesis: for r being Element of CQC-WFF Al2 st S1[r] holds
S1[ All (x,r)]
let r be Element of CQC-WFF Al2; :: thesis: ( S1[r] implies S1[ All (x,r)] )
( x in QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;
then ( x in [:NAT,(QC-symbols Al2):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;
then ( {x} c= union S & {x} is finite ) by ZFMISC_1:31;
then consider a being set such that
A68: ( a in S & {x} c= a ) by A39, COHSP_1:6, COHSP_1:13;
consider n being Element of NAT such that
A69: a = H1(n) by A68;
assume S1[r] ; :: thesis: S1[ All (x,r)]
then consider m being Element of NAT such that
A70: r is Element of CQC-WFF H1(m) ;
x in bound_QC-variables Al2 ;
then x in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;
then consider x1, x2 being object such that
A71: ( x1 in {4} & x2 in QC-symbols Al2 & x = [x1,x2] ) by ZFMISC_1:def 2;
A72: x in H1(n) by A68, A69, ZFMISC_1:31;
per cases ( n <= m or not n <= m ) ;
suppose A73: n <= m ; :: thesis: S1[ All (x,r)]
then reconsider Sm = H1(m) as H1(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;
H1(n) c= H1(m) by A73, Th6;
then x in H1(m) by A72;
then x in [:NAT,(QC-symbols H1(m)):] by QC_LANG1:5;
then consider x3, x4 being object such that
A74: ( x3 in NAT & x4 in QC-symbols H1(m) & x = [x3,x4] ) by ZFMISC_1:def 2;
x = [x1,x4] by A71, A74, XTUPLE_0:1;
then x in [:{4},(QC-symbols Sm):] by A71, A74, ZFMISC_1:def 2;
then x is bound_QC-variable of Sm by QC_LANG1:def 4;
then consider x2 being bound_QC-variable of Sm, r2 being Element of CQC-WFF Sm such that
A75: ( x2 = x & r2 = r ) by A70;
reconsider Al2 = Al2 as Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;
A76: ( r = Al2 -Cast r2 & x = Al2 -Cast x2 ) by A75, QC_TRANS:def 3, QC_TRANS:def 4;
All (x2,r2) = Al2 -Cast (All (x2,r2)) by QC_TRANS:def 3
.= All (x,r) by A76, QC_TRANS:8 ;
hence S1[ All (x,r)] ; :: thesis: verum
end;
suppose not n <= m ; :: thesis: S1[ All (x,r)]
then reconsider Sn = H1(n) as H1(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;
x in [:NAT,(QC-symbols Sn):] by A72, QC_LANG1:5;
then consider x3, x4 being object such that
A77: ( x3 in NAT & x4 in QC-symbols Sn & x = [x3,x4] ) by ZFMISC_1:def 2;
x = [x1,x4] by A71, A77, XTUPLE_0:1;
then x in [:{4},(QC-symbols Sn):] by A71, A77, ZFMISC_1:def 2;
then ( x is bound_QC-variable of Sn & r is Element of CQC-WFF Sn ) by A70, QC_TRANS:7, QC_LANG1:def 4;
then consider x2 being bound_QC-variable of Sn, r2 being Element of CQC-WFF Sn such that
A78: ( x2 = x & r2 = r ) ;
reconsider Al2 = Al2 as Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;
A79: ( r = Al2 -Cast r2 & x = Al2 -Cast x2 ) by A78, QC_TRANS:def 3, QC_TRANS:def 4;
All (x2,r2) = Al2 -Cast (All (x2,r2)) by QC_TRANS:def 3
.= All (x,r) by A79, QC_TRANS:8 ;
hence S1[ All (x,r)] ; :: thesis: verum
end;
end;
end;
then A80: for r, s being Element of CQC-WFF Al2
for x being bound_QC-variable of Al2
for k being Nat
for l being CQC-variable_list of k,Al2
for P being QC-pred_symbol of k,Al2 holds
( S1[ VERUM Al2] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A44, A45, A59, A62;
for p being Element of CQC-WFF Al2 holds S1[p] from CQC_LANG:sch 1(A80);
 hence for p being Element of CQC-WFF Al2 ex n being Element of NAT st p is Element of CQC-WFF H1(n) ; :: thesis: verum
end;
PSI is with_examples
proof
for x being bound_QC-variable of Al2
for p being Element of CQC-WFF Al2 ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))
proof
let x be bound_QC-variable of Al2; :: thesis: for p being Element of CQC-WFF Al2 ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))
let p be Element of CQC-WFF Al2; :: thesis: ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))
ex n being Element of NAT st
( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) )
proof
consider m being Element of NAT such that
A81: p is Element of CQC-WFF H1(m) by A43;
( x in QC-variables Al2 & QC-variables Al2 c= [:NAT,(QC-symbols Al2):] ) by QC_LANG1:4;
then ( x in [:NAT,(QC-symbols Al2):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;
then ( {x} c= union S & {x} is finite ) by ZFMISC_1:31;
then consider a being set such that
A82: ( a in S & {x} c= a ) by A39, COHSP_1:6, COHSP_1:13;
consider n being Element of NAT such that
A83: a = H1(n) by A82;
x in bound_QC-variables Al2 ;
then x in [:{4},(QC-symbols Al2):] by QC_LANG1:def 4;
then consider x1, x2 being object such that
A84: ( x1 in {4} & x2 in QC-symbols Al2 & x = [x1,x2] ) by ZFMISC_1:def 2;
A85: x in H1(n) by A82, A83, ZFMISC_1:31;
per cases ( n <= m or not n <= m ) ;
suppose A86: n <= m ; :: thesis: ex n being Element of NAT st
( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) )
then reconsider Sm = H1(m) as H1(n) -expanding QC-alphabet by Th6, QC_TRANS:def 1;
H1(n) c= H1(m) by A86, Th6;
then x in H1(m) by A85;
then x in [:NAT,(QC-symbols H1(m)):] by QC_LANG1:5;
then consider x3, x4 being object such that
A87: ( x3 in NAT & x4 in QC-symbols H1(m) & x = [x3,x4] ) by ZFMISC_1:def 2;
x = [x1,x4] by A84, A87, XTUPLE_0:1;
then x in [:{4},(QC-symbols Sm):] by A84, A87, ZFMISC_1:def 2;
then x is bound_QC-variable of Sm by QC_LANG1:def 4;
hence ex n being Element of NAT st
( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) ) by A81; :: thesis: verum
end;
suppose not n <= m ; :: thesis: ex n being Element of NAT st
( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) )
then reconsider Sn = H1(n) as H1(m) -expanding QC-alphabet by Th6, QC_TRANS:def 1;
x in [:NAT,(QC-symbols H1(n)):] by A85, QC_LANG1:5;
then consider x3, x4 being object such that
A88: ( x3 in NAT & x4 in QC-symbols H1(n) & x = [x3,x4] ) by ZFMISC_1:def 2;
x = [x1,x4] by A84, A88, XTUPLE_0:1;
then x in [:{4},(QC-symbols Sn):] by A84, A88, ZFMISC_1:def 2;
then ( x is bound_QC-variable of Sn & p is Element of CQC-WFF Sn ) by A81, QC_TRANS:7, QC_LANG1:def 4;
hence ex n being Element of NAT st
( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) ) ; :: thesis: verum
end;
end;
end;
then consider n being Element of NAT such that
A89: ( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) ) ;
A90: FCEx H1(n) = H1(n + 1) by Th5;
A91: H2(n + 1) = H2(n) \/ (Example_Formulae_of H1(n)) by Def9;
consider x2 being bound_QC-variable of H1(n), p2 being Element of CQC-WFF H1(n) such that
A92: ( x2 = x & p2 = p ) by A89;
Example_Formula_of (p2,x2) in Example_Formulae_of H1(n) ;
then A93: Example_Formula_of (p2,x2) in H2(n + 1) by A91, XBOOLE_0:def 3;
H1(n) c= H1(n + 1) by Th6, NAT_1:11;
then reconsider Sn1 = H1(n + 1) as H1(n) -expanding QC-alphabet by QC_TRANS:def 1;
set y2 = Example_of (p2,x2);
reconsider y2 = Example_of (p2,x2) as bound_QC-variable of Sn1 by Th5;
reconsider Al2 = Al2 as Sn1 -expanding QC-alphabet by A2, QC_TRANS:def 1;
y2 is bound_QC-variable of Al2 by TARSKI:def 3, QC_TRANS:4;
then consider y being bound_QC-variable of Al2 such that
A94: y = y2 ;
A95: ( Sn1 -Cast p2 = p & Sn1 -Cast x2 = x ) by A92, QC_TRANS:def 3, QC_TRANS:def 4;
then A96: ( Al2 -Cast (Sn1 -Cast p2) = p & Al2 -Cast (Sn1 -Cast x2) = x ) by QC_TRANS:def 3, QC_TRANS:def 4;
A97: Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))) = Ex (x,p) by A96, Th7;
reconsider p = p as Element of CQC-WFF Al2 ;
reconsider x = x as bound_QC-variable of Al2 ;
A98: (Sn1 -Cast p2) . ((Sn1 -Cast x2),y2) = p . (x,y) by A94, A95, QC_TRANS:17;
A99: Example_Formula_of (p2,x2) = Al2 -Cast (('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2)))) 'or' ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by A90, QC_TRANS:def 3
.= (Al2 -Cast ('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by Th7
.= ('not' (Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2))) by QC_TRANS:8
.= ('not' (Ex (x,p))) 'or' (p . (x,y)) by A97, A98, QC_TRANS:def 3 ;
set example = ('not' (Ex (x,p))) 'or' (p . (x,y));
reconsider example = ('not' (Ex (x,p))) 'or' (p . (x,y)) as Element of CQC-WFF Al2 ;
reconsider PSI = PSI as Consistent Subset of (CQC-WFF Al2) ;
H2(n + 1) in { H2(m) where m is Element of NAT : verum } ;
then H2(n + 1) c= PSI by ZFMISC_1:74;
hence ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A93, A99, GOEDELCP:21; :: thesis: verum
end;
hence PSI is with_examples by GOEDELCP:def 2; :: thesis: verum
end;
hence ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
( PHI c= PSI & PSI is with_examples ) by A1; :: thesis: verum