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

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

hence
PHI is Al -Consistent
; :: thesis: verum
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)

end;assume A1: PHI = S ; :: thesis: S is Consistent

assume A2: S is Inconsistent ; :: thesis: contradiction

PHI |- 'not' (VERUM Al2)

proof

hence
contradiction
by GOEDELCP:24; :: thesis: verum
consider f being FinSequence of CQC-WFF Al such that

A3: ( rng f c= S & |- f ^ <*('not' (VERUM Al))*> ) by A2, GOEDELCP:24, HENMODEL:def 1;

set f2 = f;

for x being object st x in rng f holds

x in CQC-WFF Al2

consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that

A5: ( PR is a_proof & f ^ <*('not' (VERUM Al))*> = (PR . (len PR)) `1 ) by A3, CALCUL_1:def 9;

A6: ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds

PR,n is_a_correct_step ) ) by A5, CALCUL_1:def 8;

set PR2 = PR;

PR is FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:]

A8: PR2 is a_proof

hence PHI |- 'not' (VERUM Al2) by A1, A3, HENMODEL:def 1; :: thesis: verum

end;A3: ( rng f c= S & |- f ^ <*('not' (VERUM Al))*> ) by A2, GOEDELCP:24, HENMODEL:def 1;

set f2 = f;

for x being object st x in rng f holds

x in CQC-WFF Al2

proof

then reconsider f2 = f as FinSequence of CQC-WFF Al2 by FINSEQ_1:def 4, TARSKI:def 3;
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;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

consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that

A5: ( PR is a_proof & f ^ <*('not' (VERUM Al))*> = (PR . (len PR)) `1 ) by A3, CALCUL_1:def 9;

A6: ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds

PR,n is_a_correct_step ) ) by A5, CALCUL_1:def 8;

set PR2 = PR;

PR is FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:]

proof

then reconsider PR2 = PR as FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] ;
for p being object st p in CQC-WFF Al holds

p in CQC-WFF Al2

for x being object st x in set_of_CQC-WFF-seq Al holds

x in set_of_CQC-WFF-seq Al2

then [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] c= [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] by ZFMISC_1:95;

then rng PR c= [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] ;

hence PR is FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] by FINSEQ_1:def 4; :: thesis: verum

end;p in CQC-WFF Al2

proof

then A7:
( CQC-WFF Al c= CQC-WFF Al2 & rng PR c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] )
;
let p be object ; :: thesis: ( p in CQC-WFF Al implies p in CQC-WFF Al2 )

assume p in CQC-WFF Al ; :: thesis: p in CQC-WFF Al2

then p is Element of CQC-WFF Al2 by Th7;

hence p in CQC-WFF Al2 ; :: thesis: verum

end;assume p in CQC-WFF Al ; :: thesis: p in CQC-WFF Al2

then p is Element of CQC-WFF Al2 by Th7;

hence p in CQC-WFF Al2 ; :: thesis: verum

for x being object st x in set_of_CQC-WFF-seq Al holds

x in set_of_CQC-WFF-seq Al2

proof

then
set_of_CQC-WFF-seq Al c= set_of_CQC-WFF-seq Al2
;
let x be object ; :: thesis: ( x in set_of_CQC-WFF-seq Al implies x in set_of_CQC-WFF-seq Al2 )

assume x in set_of_CQC-WFF-seq Al ; :: thesis: x in set_of_CQC-WFF-seq Al2

then reconsider x = x as FinSequence of CQC-WFF Al by CALCUL_1:def 6;

rng x c= CQC-WFF Al2 by A7;

then x is FinSequence of CQC-WFF Al2 by FINSEQ_1:def 4;

hence x in set_of_CQC-WFF-seq Al2 by CALCUL_1:def 6; :: thesis: verum

end;assume x in set_of_CQC-WFF-seq Al ; :: thesis: x in set_of_CQC-WFF-seq Al2

then reconsider x = x as FinSequence of CQC-WFF Al by CALCUL_1:def 6;

rng x c= CQC-WFF Al2 by A7;

then x is FinSequence of CQC-WFF Al2 by FINSEQ_1:def 4;

hence x in set_of_CQC-WFF-seq Al2 by CALCUL_1:def 6; :: thesis: verum

then [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] c= [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] by ZFMISC_1:95;

then rng PR c= [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] ;

hence PR is FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] by FINSEQ_1:def 4; :: thesis: verum

A8: PR2 is a_proof

proof

|- f2 ^ <*('not' (VERUM Al2))*>
by A5, A8, CALCUL_1:def 9;
for n being Nat st 1 <= n & n <= len PR2 holds

PR2,n is_a_correct_step

end;PR2,n is_a_correct_step

proof

hence
PR2 is a_proof
by A6, CALCUL_1:def 8; :: thesis: verum
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 )

not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 by CALCUL_1:31, A9;

end;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

A13:
PR,n is_a_correct_step
by A5, CALCUL_1:def 8, A9;
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

then n in dom PR2 by A9, FINSEQ_1:1;

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;(PR2 . i) `1 in set_of_CQC-WFF-seq Al2 :: thesis: (PR2 . n) `1 in set_of_CQC-WFF-seq Al2

proof

dom PR2 = Seg (len PR2)
by FINSEQ_1:def 3;
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 A9, NAT_1:21;

len PR2 = n + k ;

then A12: ( 1 <= i & i <= len PR2 ) by A11, NAT_1:12;

dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;

then i in dom PR2 by A12, FINSEQ_1:1;

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;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 A9, NAT_1:21;

len PR2 = n + k ;

then A12: ( 1 <= i & i <= len PR2 ) by A11, NAT_1:12;

dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;

then i in dom PR2 by A12, FINSEQ_1:1;

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

then n in dom PR2 by A9, FINSEQ_1:1;

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

not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 by CALCUL_1:31, A9;

per cases then
( (PR2 . n) `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 )
;

end;

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 A13, CALCUL_1:def 7;

g2 is FinSequence of CQC-WFF Al2 by A10, A15, CALCUL_1:def 6;

then consider g being FinSequence of CQC-WFF Al2 such that

A16: g = g2 ;

A17: ( Suc g = Suc g2 & Ant g = Ant g2 ) by A16, Th11;

thus PR2,n is_a_correct_step by A14, A15, A16, A17, CALCUL_1:def 7; :: thesis: verum

end;A15: ( Suc g2 is_tail_of Ant g2 & (PR2 . n) `1 = g2 ) by A13, CALCUL_1:def 7;

g2 is FinSequence of CQC-WFF Al2 by A10, A15, CALCUL_1:def 6;

then consider g being FinSequence of CQC-WFF Al2 such that

A16: g = g2 ;

A17: ( Suc g = Suc g2 & Ant g = Ant g2 ) by A16, Th11;

thus PR2,n is_a_correct_step by A14, A15, A16, A17, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

g2 ^ <*(VERUM Al)*> is FinSequence of CQC-WFF Al2 by A10, A19, CALCUL_1:def 6;

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 A20, A21, FINSEQ_2:17;

hence PR2,n is_a_correct_step by A18, A19, A20, A21, CALCUL_1:def 7; :: thesis: verum

end;A19: (PR . n) `1 = g2 ^ <*(VERUM Al)*> by A13, CALCUL_1:def 7;

g2 ^ <*(VERUM Al)*> is FinSequence of CQC-WFF Al2 by A10, A19, CALCUL_1:def 6;

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 A20, A21, FINSEQ_2:17;

hence PR2,n is_a_correct_step by A18, A19, A20, A21, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

( g2 in set_of_CQC-WFF-seq Al2 & h2 in set_of_CQC-WFF-seq Al2 ) by A10, A23;

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 A24, Th11

.= Suc h by A23, A24, Th11 ;

consider N being Subset of NAT such that

A26: Ant g2 c= Seq ((Ant h2) | N) by A23, CALCUL_1:def 4;

(Ant h2) | N = (Ant h) | N by A24, Th11;

then Ant g c= Seq ((Ant h) | N) by A24, A26, Th11;

then A27: Ant g is_Subsequence_of Ant h by CALCUL_1:def 4;

thus PR2,n is_a_correct_step by A22, A23, A24, A25, A27, CALCUL_1:def 7; :: thesis: verum

end;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 A13, CALCUL_1:def 7;

( g2 in set_of_CQC-WFF-seq Al2 & h2 in set_of_CQC-WFF-seq Al2 ) by A10, A23;

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 A24, Th11

.= Suc h by A23, A24, Th11 ;

consider N being Subset of NAT such that

A26: Ant g2 c= Seq ((Ant h2) | N) by A23, CALCUL_1:def 4;

(Ant h2) | N = (Ant h) | N by A24, Th11;

then Ant g c= Seq ((Ant h) | N) by A24, A26, Th11;

then A27: Ant g is_Subsequence_of Ant h by CALCUL_1:def 4;

thus PR2,n is_a_correct_step by A22, A23, A24, A25, A27, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A29, XXREAL_0:2;

then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A29;

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 A30, Th11;

then A32: Ant (Ant g2) = Ant (Ant g) by Th11

.= Ant (Ant h2) by A29, A31, Th11 ;

A33: 'not' (Suc (Ant g2)) = 'not' (Al2 -Cast (Suc (Ant g))) by A31, Th11

.= Suc (Ant h2) by A29, A31, Th11 ;

A34: Suc g2 = Suc g by A30, Th11

.= Suc h2 by A29, A30, Th11 ;

A35: (PR2 . n) `1 = (Ant (Ant g)) ^ <*(Suc g2)*> by A29, A30, Th11

.= (Ant (Ant g2)) ^ <*(Suc g2)*> by A31, Th11 ;

thus PR2,n is_a_correct_step by A28, A29, A30, A32, A33, A34, A35, CALCUL_1:def 7; :: thesis: verum

end;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 A13, CALCUL_1:def 7;

( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A29, XXREAL_0:2;

then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A29;

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 A30, Th11;

then A32: Ant (Ant g2) = Ant (Ant g) by Th11

.= Ant (Ant h2) by A29, A31, Th11 ;

A33: 'not' (Suc (Ant g2)) = 'not' (Al2 -Cast (Suc (Ant g))) by A31, Th11

.= Suc (Ant h2) by A29, A31, Th11 ;

A34: Suc g2 = Suc g by A30, Th11

.= Suc h2 by A29, A30, Th11 ;

A35: (PR2 . n) `1 = (Ant (Ant g)) ^ <*(Suc g2)*> by A29, A30, Th11

.= (Ant (Ant g2)) ^ <*(Suc g2)*> by A31, Th11 ;

thus PR2,n is_a_correct_step by A28, A29, A30, A32, A33, A34, A35, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A37, XXREAL_0:2;

then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A37;

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 A38, Th11

.= Ant h2 by A37, A38, Th11 ;

Ant g2 = Ant g by A38, Th11;

then A40: Suc (Ant g2) = 'not' (Al2 -Cast p) by A37, Th11;

A41: 'not' (Suc g2) = 'not' (Al2 -Cast (Suc g)) by A38, Th11

.= Suc h2 by A37, A38, Th11 ;

Ant g2 = Ant g by A38, Th11;

then (Ant (Ant g2)) ^ <*(Al2 -Cast p)*> = (PR2 . n) `1 by Th11, A37;

hence PR2,n is_a_correct_step by A36, A37, A38, A39, A40, A41, CALCUL_1:def 7; :: thesis: verum

end;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 A13, CALCUL_1:def 7;

( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A37, XXREAL_0:2;

then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A37;

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 A38, Th11

.= Ant h2 by A37, A38, Th11 ;

Ant g2 = Ant g by A38, Th11;

then A40: Suc (Ant g2) = 'not' (Al2 -Cast p) by A37, Th11;

A41: 'not' (Suc g2) = 'not' (Al2 -Cast (Suc g)) by A38, Th11

.= Suc h2 by A37, A38, Th11 ;

Ant g2 = Ant g by A38, Th11;

then (Ant (Ant g2)) ^ <*(Al2 -Cast p)*> = (PR2 . n) `1 by Th11, A37;

hence PR2,n is_a_correct_step by A36, A37, A38, A39, A40, A41, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A43, XXREAL_0:2;

then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A43;

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 A44, Th11;

then A45: (Ant g2) ^ <*((Suc g2) '&' (Suc h2))*> = (PR2 . n) `1 by A43, A44, Th11;

Ant g2 = Ant g by A44, Th11

.= Ant h2 by A43, A44, Th11 ;

hence PR2,n is_a_correct_step by A42, A43, A44, A45, CALCUL_1:def 7; :: thesis: verum

end;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 A13, CALCUL_1:def 7;

( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A43, XXREAL_0:2;

then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A43;

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 A44, Th11;

then A45: (Ant g2) ^ <*((Suc g2) '&' (Suc h2))*> = (PR2 . n) `1 by A43, A44, Th11;

Ant g2 = Ant g by A44, Th11

.= Ant h2 by A43, A44, Th11 ;

hence PR2,n is_a_correct_step by A42, A43, A44, A45, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A47;

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 A47, A48, Th11;

(Ant g2) ^ <*p*> = (PR2 . n) `1 by A47, A48, Th11;

hence PR2,n is_a_correct_step by A46, A47, A48, A49, CALCUL_1:def 7; :: thesis: verum

end;A47: ( 1 <= i & i < n & p '&' q = Suc g & g = (PR2 . i) `1 & (Ant g) ^ <*p*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A47;

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 A47, A48, Th11;

(Ant g2) ^ <*p*> = (PR2 . n) `1 by A47, A48, Th11;

hence PR2,n is_a_correct_step by A46, A47, A48, A49, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A51;

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 A51, Th11;

(Ant g2) ^ <*(Al2 -Cast q)*> = (PR2 . n) `1 by A51, Th11;

hence PR2,n is_a_correct_step by A50, A51, A52, CALCUL_1:def 7; :: thesis: verum

end;A51: ( 1 <= i & i < n & p '&' q = Suc g & g = (PR2 . i) `1 & (Ant g) ^ <*q*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A51;

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 A51, Th11;

(Ant g2) ^ <*(Al2 -Cast q)*> = (PR2 . n) `1 by A51, Th11;

hence PR2,n is_a_correct_step by A50, A51, A52, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A54;

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 Th4, Th7, TARSKI:def 3;

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 A54, A56, Th17

.= (Ant g2) ^ <*(q . (a,b))*> by A55, Th11 ;

Suc g2 = All (a,q) by A54, A55, A56, Th11;

hence PR2,n is_a_correct_step by A53, A54, A55, A57, CALCUL_1:def 7; :: thesis: verum

end;A54: ( 1 <= i & i < n & Suc g = All (x,p) & g = (PR2 . i) `1 & (Ant g) ^ <*(p . (x,y))*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A54;

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 Th4, Th7, TARSKI:def 3;

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 A54, A56, Th17

.= (Ant g2) ^ <*(q . (a,b))*> by A55, Th11 ;

Suc g2 = All (a,q) by A54, A55, A56, Th11;

hence PR2,n is_a_correct_step by A53, A54, A55, A57, CALCUL_1:def 7; :: thesis: verum

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 A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A59;

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 Th4, Th7, TARSKI:def 3;

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 A60, Th11

.= q . (a,b) by A59, A61, Th17 ;

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)

hence PR2,n is_a_correct_step by A58, A59, A60, A61, A62, A63, A64, CALCUL_1:def 7; :: thesis: verum

end;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 A13, CALCUL_1:def 7;

g in set_of_CQC-WFF-seq Al2 by A10, A59;

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 Th4, Th7, TARSKI:def 3;

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 A60, Th11

.= q . (a,b) by A59, A61, Th17 ;

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

(Ant g2) ^ <*(All (a,q))*> = (PR2 . n) `1
by A59, A60, A61, Th11;
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 A60, Th11;

r = (Ant g) . i by A60, A65, Th11;

then reconsider r = r as Element of CQC-WFF Al by A65, A66, FINSEQ_2:11;

( i in dom (Ant g) & Al2 -Cast r = (Ant g) . i & b in still_not-bound_in (Al2 -Cast r) ) by A60, A65, Th11;

then ( i in dom (Ant g) & r = (Ant g) . i & y in still_not-bound_in r ) by A61, Th12;

hence contradiction by A59, CALCUL_1:def 5; :: thesis: verum

end;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 A60, Th11;

r = (Ant g) . i by A60, A65, Th11;

then reconsider r = r as Element of CQC-WFF Al by A65, A66, FINSEQ_2:11;

( i in dom (Ant g) & Al2 -Cast r = (Ant g) . i & b in still_not-bound_in (Al2 -Cast r) ) by A60, A65, Th11;

then ( i in dom (Ant g) & r = (Ant g) . i & y in still_not-bound_in r ) by A61, Th12;

hence contradiction by A59, CALCUL_1:def 5; :: thesis: verum

hence PR2,n is_a_correct_step by A58, A59, A60, A61, A62, A63, A64, CALCUL_1:def 7; :: thesis: verum

hence PHI |- 'not' (VERUM Al2) by A1, A3, HENMODEL:def 1; :: thesis: verum