let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds
PHI is Al -Consistent

let Al2 be Al -expanding QC-alphabet ; :: thesis: for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds
PHI is Al -Consistent

let PHI be Consistent Subset of (CQC-WFF Al2); :: thesis: ( PHI is Subset of (CQC-WFF Al) implies PHI is Al -Consistent )
assume PHI is Subset of (CQC-WFF Al) ; :: thesis: PHI is Al -Consistent
for S being Subset of (CQC-WFF Al) st PHI = S holds
S is Consistent
proof
let S be Subset of (CQC-WFF Al); :: thesis: ( PHI = S implies S is Consistent )
assume A1: PHI = S ; :: thesis: S is Consistent
assume A2: S is Inconsistent ; :: thesis: contradiction
PHI |- 'not' (VERUM Al2)
proof
consider f being FinSequence of CQC-WFF Al such that
A3: ( rng f c= S & |- f ^ <*('not' (VERUM Al))*> ) by ;
set f2 = f;
for x being object st x in rng f holds
x in CQC-WFF Al2
proof
let x be object ; :: thesis: ( x in rng f implies x in CQC-WFF Al2 )
assume A4: x in rng f ; :: thesis: x in CQC-WFF Al2
x in PHI by A1, A3, A4;
hence x in CQC-WFF Al2 ; :: thesis: verum
end;
then reconsider f2 = f as FinSequence of CQC-WFF Al2 by ;
consider PR being FinSequence of such that
A5: ( PR is a_proof & f ^ <*('not' (VERUM Al))*> = (PR . (len PR)) `1 ) by ;
A6: ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds
PR,n is_a_correct_step ) ) by ;
set PR2 = PR;
PR is FinSequence of
proof end;
then reconsider PR2 = PR as FinSequence of ;
A8: PR2 is a_proof
proof
for n being Nat st 1 <= n & n <= len PR2 holds
PR2,n is_a_correct_step
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len PR2 implies PR2,n is_a_correct_step )
assume A9: ( 1 <= n & n <= len PR2 ) ; :: thesis: PR2,n is_a_correct_step
A10: ( ( for i being Nat st 1 <= i & i < n holds
(PR2 . i) `1 in set_of_CQC-WFF-seq Al2 ) & (PR2 . n) `1 in set_of_CQC-WFF-seq Al2 )
proof
thus for i being Nat st 1 <= i & i < n holds
(PR2 . i) `1 in set_of_CQC-WFF-seq Al2 :: thesis: (PR2 . n) `1 in set_of_CQC-WFF-seq Al2
proof
let i be Nat; :: thesis: ( 1 <= i & i < n implies (PR2 . i) `1 in set_of_CQC-WFF-seq Al2 )
assume A11: ( 1 <= i & i < n ) ; :: thesis: (PR2 . i) `1 in set_of_CQC-WFF-seq Al2
set k = (len PR2) - n;
reconsider k = (len PR2) - n as Element of NAT by ;
len PR2 = n + k ;
then A12: ( 1 <= i & i <= len PR2 ) by ;
dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;
then i in dom PR2 by ;
then PR2 . i in rng PR2 by FUNCT_1:def 3;
hence (PR2 . i) `1 in set_of_CQC-WFF-seq Al2 by MCART_1:10; :: thesis: verum
end;
dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;
then n in dom PR2 by ;
then PR2 . n in rng PR2 by FUNCT_1:def 3;
hence (PR2 . n) `1 in set_of_CQC-WFF-seq Al2 by MCART_1:10; :: thesis: verum
end;
A13: PR,n is_a_correct_step by ;
not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 by ;
per cases ) `2 = 0 or (PR2 . n) `2 = 1 or (PR2 . n) `2 = 2 or (PR2 . n) `2 = 3 or (PR2 . n) `2 = 4 or (PR2 . n) `2 = 5 or (PR2 . n) `2 = 6 or (PR2 . n) `2 = 7 or (PR2 . n) `2 = 8 or (PR2 . n) `2 = 9 ) ;
suppose A14: (PR2 . n) `2 = 0 ; :: thesis: PR2,n is_a_correct_step
then consider g2 being FinSequence of CQC-WFF Al such that
A15: ( Suc g2 is_tail_of Ant g2 & (PR2 . n) `1 = g2 ) by ;
g2 is FinSequence of CQC-WFF Al2 by ;
then consider g being FinSequence of CQC-WFF Al2 such that
A16: g = g2 ;
A17: ( Suc g = Suc g2 & Ant g = Ant g2 ) by ;
thus PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A18: (PR2 . n) `2 = 1 ; :: thesis: PR2,n is_a_correct_step
then consider g2 being FinSequence of CQC-WFF Al such that
A19: (PR . n) `1 = g2 ^ <*(VERUM Al)*> by ;
g2 ^ <*(VERUM Al)*> is FinSequence of CQC-WFF Al2 by ;
then consider gp being FinSequence of CQC-WFF Al2 such that
A20: gp = g2 ^ <*(VERUM Al)*> ;
len gp <> 0 by A20;
then consider g being FinSequence of CQC-WFF Al2, v being Element of CQC-WFF Al2 such that
A21: gp = g ^ <*v*> by FINSEQ_2:19;
v = VERUM Al2 by ;
hence PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A22: (PR2 . n) `2 = 2 ; :: thesis: PR2,n is_a_correct_step
then consider i being Nat, g2, h2 being FinSequence of CQC-WFF Al such that
A23: ( 1 <= i & i < n & Ant g2 is_Subsequence_of Ant h2 & Suc g2 = Suc h2 & (PR2 . i) `1 = g2 & (PR2 . n) `1 = h2 ) by ;
( g2 in set_of_CQC-WFF-seq Al2 & h2 in set_of_CQC-WFF-seq Al2 ) by ;
then ( h2 is FinSequence of CQC-WFF Al2 & g2 is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g, h being FinSequence of CQC-WFF Al2 such that
A24: ( g = g2 & h = h2 ) ;
A25: Suc g = Suc g2 by
.= Suc h by ;
consider N being Subset of NAT such that
A26: Ant g2 c= Seq ((Ant h2) | N) by ;
(Ant h2) | N = (Ant h) | N by ;
then Ant g c= Seq ((Ant h) | N) by ;
then A27: Ant g is_Subsequence_of Ant h by CALCUL_1:def 4;
thus PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A28: (PR2 . n) `2 = 3 ; :: thesis: PR2,n is_a_correct_step
then consider i, j being Nat, g, h being FinSequence of CQC-WFF Al such that
A29: ( 1 <= i & i < n & 1 <= j & j < i & len g > 1 & len h > 1 & Ant (Ant g) = Ant (Ant h) & 'not' (Suc (Ant g)) = Suc (Ant h) & Suc g = Suc h & g = (PR2 . j) `1 & h = (PR2 . i) `1 & (Ant (Ant g)) ^ <*(Suc g)*> = (PR2 . n) `1 ) by ;
( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by ;
then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by ;
then ( h is FinSequence of CQC-WFF Al2 & g is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g2, h2 being FinSequence of CQC-WFF Al2 such that
A30: ( g2 = g & h2 = h ) ;
A31: ( Ant g2 = Ant g & Ant h2 = Ant h ) by ;
then A32: Ant (Ant g2) = Ant (Ant g) by Th11
.= Ant (Ant h2) by ;
A33: 'not' (Suc (Ant g2)) = 'not' (Al2 -Cast (Suc (Ant g))) by
.= Suc (Ant h2) by ;
A34: Suc g2 = Suc g by
.= Suc h2 by ;
A35: (PR2 . n) `1 = (Ant (Ant g)) ^ <*(Suc g2)*> by
.= (Ant (Ant g2)) ^ <*(Suc g2)*> by ;
thus PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A36: (PR2 . n) `2 = 4 ; :: thesis: PR2,n is_a_correct_step
then consider i, j being Nat, g, h being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al such that
A37: ( 1 <= i & i < n & 1 <= j & j < i & len g > 1 & Ant g = Ant h & Suc (Ant g) = 'not' p & 'not' (Suc g) = Suc h & g = (PR2 . j) `1 & h = (PR2 . i) `1 & (Ant (Ant g)) ^ <*p*> = (PR2 . n) `1 ) by ;
( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by ;
then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by ;
then ( h is FinSequence of CQC-WFF Al2 & g is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g2, h2 being FinSequence of CQC-WFF Al2 such that
A38: ( g2 = g & h2 = h ) ;
A39: Ant g2 = Ant g by
.= Ant h2 by ;
Ant g2 = Ant g by ;
then A40: Suc (Ant g2) = 'not' (Al2 -Cast p) by ;
A41: 'not' (Suc g2) = 'not' (Al2 -Cast (Suc g)) by
.= Suc h2 by ;
Ant g2 = Ant g by ;
then (Ant (Ant g2)) ^ <*(Al2 -Cast p)*> = (PR2 . n) `1 by ;
hence PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A42: (PR2 . n) `2 = 5 ; :: thesis: PR2,n is_a_correct_step
then consider i, j being Nat, g, h being FinSequence of CQC-WFF Al such that
A43: ( 1 <= i & i < n & 1 <= j & j < i & Ant g = Ant h & g = (PR2 . j) `1 & h = (PR2 . i) `1 & (Ant g) ^ <*((Suc g) '&' (Suc h))*> = (PR2 . n) `1 ) by ;
( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by ;
then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by ;
then ( h is FinSequence of CQC-WFF Al2 & g is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g2, h2 being FinSequence of CQC-WFF Al2 such that
A44: ( g = g2 & h = h2 ) ;
( Al2 -Cast (Suc g) = Suc g2 & Al2 -Cast (Suc h) = Suc h2 ) by ;
then A45: (Ant g2) ^ <*((Suc g2) '&' (Suc h2))*> = (PR2 . n) `1 by ;
Ant g2 = Ant g by
.= Ant h2 by ;
hence PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A46: (PR2 . n) `2 = 6 ; :: thesis: PR2,n is_a_correct_step
then consider i being Nat, g being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A47: ( 1 <= i & i < n & p '&' q = Suc g & g = (PR2 . i) `1 & (Ant g) ^ <*p*> = (PR2 . n) `1 ) by ;
g in set_of_CQC-WFF-seq Al2 by ;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF Al2 such that
A48: g = g2 ;
A49: Suc g2 = (Al2 -Cast p) '&' (Al2 -Cast q) by ;
(Ant g2) ^ <*p*> = (PR2 . n) `1 by ;
hence PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A50: (PR2 . n) `2 = 7 ; :: thesis: PR2,n is_a_correct_step
then consider i being Nat, g being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A51: ( 1 <= i & i < n & p '&' q = Suc g & g = (PR2 . i) `1 & (Ant g) ^ <*q*> = (PR2 . n) `1 ) by ;
g in set_of_CQC-WFF-seq Al2 by ;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then reconsider g2 = g as FinSequence of CQC-WFF Al2 ;
A52: Suc g2 = (Al2 -Cast p) '&' (Al2 -Cast q) by ;
(Ant g2) ^ <*(Al2 -Cast q)*> = (PR2 . n) `1 by ;
hence PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A53: (PR2 . n) `2 = 8 ; :: thesis: PR2,n is_a_correct_step
then consider i being Nat, g being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A54: ( 1 <= i & i < n & Suc g = All (x,p) & g = (PR2 . i) `1 & (Ant g) ^ <*(p . (x,y))*> = (PR2 . n) `1 ) by ;
g in set_of_CQC-WFF-seq Al2 by ;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF Al2 such that
A55: g = g2 ;
( p is Element of CQC-WFF Al2 & x is bound_QC-variable of Al2 & y is bound_QC-variable of Al2 ) by ;
then consider q being Element of CQC-WFF Al2, a, b being bound_QC-variable of Al2 such that
A56: ( a = x & b = y & q = p ) ;
A57: (PR2 . n) `1 = (Ant g) ^ <*(q . (a,b))*> by
.= (Ant g2) ^ <*(q . (a,b))*> by ;
Suc g2 = All (a,q) by ;
hence PR2,n is_a_correct_step by ; :: thesis: verum
end;
suppose A58: (PR2 . n) `2 = 9 ; :: thesis: PR2,n is_a_correct_step
then consider i being Nat, g being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A59: ( 1 <= i & i < n & Suc g = p . (x,y) & not y in still_not-bound_in (Ant g) & not y in still_not-bound_in (All (x,p)) & g = (PR2 . i) `1 & (Ant g) ^ <*(All (x,p))*> = (PR2 . n) `1 ) by ;
g in set_of_CQC-WFF-seq Al2 by ;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF Al2 such that
A60: g = g2 ;
( p is Element of CQC-WFF Al2 & x is bound_QC-variable of Al2 & y is bound_QC-variable of Al2 ) by ;
then consider q being Element of CQC-WFF Al2, a, b being bound_QC-variable of Al2 such that
A61: ( q = p & a = x & b = y ) ;
A62: Suc g2 = Suc g by
.= q . (a,b) by ;
A63: still_not-bound_in (All (x,p)) = still_not-bound_in (Al2 -Cast (All (x,p))) by Th12
.= still_not-bound_in (All (a,q)) by A61 ;
A64: not b in still_not-bound_in (Ant g2)
proof
assume b in still_not-bound_in (Ant g2) ; :: thesis: contradiction
then consider i being Nat, r being Element of CQC-WFF Al2 such that
A65: ( i in dom (Ant g2) & r = (Ant g2) . i & b in still_not-bound_in r ) by CALCUL_1:def 5;
A66: dom (Ant g2) = dom (Ant g) by ;
r = (Ant g) . i by ;
then reconsider r = r as Element of CQC-WFF Al by ;
( i in dom (Ant g) & Al2 -Cast r = (Ant g) . i & b in still_not-bound_in (Al2 -Cast r) ) by ;
then ( i in dom (Ant g) & r = (Ant g) . i & y in still_not-bound_in r ) by ;
hence contradiction by A59, CALCUL_1:def 5; :: thesis: verum
end;
(Ant g2) ^ <*(All (a,q))*> = (PR2 . n) `1 by ;
hence PR2,n is_a_correct_step by ; :: thesis: verum
end;
end;
end;
hence PR2 is a_proof by ; :: thesis: verum
end;
|- f2 ^ <*('not' (VERUM Al2))*> by ;
hence PHI |- 'not' (VERUM Al2) by ; :: thesis: verum
end;
hence contradiction by GOEDELCP:24; :: thesis: verum
end;
hence PHI is Al -Consistent ; :: thesis: verum