let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for f, g being FinSequence of CQC-WFF Al st len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g holds

|- (Ant (Ant f)) ^ <*p*>

let p be Element of CQC-WFF Al; :: thesis: for f, g being FinSequence of CQC-WFF Al st len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g holds

|- (Ant (Ant f)) ^ <*p*>

let f, g be FinSequence of CQC-WFF Al; :: thesis: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g implies |- (Ant (Ant f)) ^ <*p*> )

assume that

A1: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g ) and

A2: |- f and

A3: |- g ; :: thesis: |- (Ant (Ant f)) ^ <*p*>

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

A4: PR1 is a_proof and

A5: g = (PR1 . (len PR1)) `1 by A3;

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

A6: PR is a_proof and

A7: f = (PR . (len PR)) `1 by A2;

A8: (Ant (Ant f)) ^ <*p*> in set_of_CQC-WFF-seq Al by Def6;

then reconsider PR2 = <*[((Ant (Ant f)) ^ <*p*>),4]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;

1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;

then A9: 1 in dom PR2 by FINSEQ_1:38;

set PR3 = (PR ^ PR1) ^ PR2;

reconsider PR3 = (PR ^ PR1) ^ PR2 as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;

A10: PR <> {} by A6;

PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + (len PR2)) by FINSEQ_1:22;

then PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + 1) by FINSEQ_1:39;

then PR3 . (len PR3) = PR2 . 1 by A9, FINSEQ_1:def 7;

then PR3 . (len PR3) = [((Ant (Ant f)) ^ <*p*>),4] by FINSEQ_1:40;

then (PR3 . (len PR3)) `1 = (Ant (Ant f)) ^ <*p*> ;

hence |- (Ant (Ant f)) ^ <*p*> by A39; :: thesis: verum

for f, g being FinSequence of CQC-WFF Al st len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g holds

|- (Ant (Ant f)) ^ <*p*>

let p be Element of CQC-WFF Al; :: thesis: for f, g being FinSequence of CQC-WFF Al st len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g holds

|- (Ant (Ant f)) ^ <*p*>

let f, g be FinSequence of CQC-WFF Al; :: thesis: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g implies |- (Ant (Ant f)) ^ <*p*> )

assume that

A1: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g ) and

A2: |- f and

A3: |- g ; :: thesis: |- (Ant (Ant f)) ^ <*p*>

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

A4: PR1 is a_proof and

A5: g = (PR1 . (len PR1)) `1 by A3;

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

A6: PR is a_proof and

A7: f = (PR . (len PR)) `1 by A2;

A8: (Ant (Ant f)) ^ <*p*> in set_of_CQC-WFF-seq Al by Def6;

now :: thesis: for a being object st a in rng <*[((Ant (Ant f)) ^ <*p*>),4]*> holds

a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

then
rng <*[((Ant (Ant f)) ^ <*p*>),4]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
;a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

let a be object ; :: thesis: ( a in rng <*[((Ant (Ant f)) ^ <*p*>),4]*> implies a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] )

assume a in rng <*[((Ant (Ant f)) ^ <*p*>),4]*> ; :: thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

then a in {[((Ant (Ant f)) ^ <*p*>),4]} by FINSEQ_1:38;

then a = [((Ant (Ant f)) ^ <*p*>),4] by TARSKI:def 1;

hence a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by A8, CQC_THE1:21, ZFMISC_1:87; :: thesis: verum

end;assume a in rng <*[((Ant (Ant f)) ^ <*p*>),4]*> ; :: thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

then a in {[((Ant (Ant f)) ^ <*p*>),4]} by FINSEQ_1:38;

then a = [((Ant (Ant f)) ^ <*p*>),4] by TARSKI:def 1;

hence a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by A8, CQC_THE1:21, ZFMISC_1:87; :: thesis: verum

then reconsider PR2 = <*[((Ant (Ant f)) ^ <*p*>),4]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;

1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;

then A9: 1 in dom PR2 by FINSEQ_1:38;

set PR3 = (PR ^ PR1) ^ PR2;

reconsider PR3 = (PR ^ PR1) ^ PR2 as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;

A10: PR <> {} by A6;

now :: thesis: for n being Nat st 1 <= n & n <= len PR3 holds

PR3,n is_a_correct_step

then A39:
PR3 is a_proof
;PR3,n is_a_correct_step

let n be Nat; :: thesis: ( 1 <= n & n <= len PR3 implies PR3,n is_a_correct_step )

assume ( 1 <= n & n <= len PR3 ) ; :: thesis: PR3,n is_a_correct_step

then A11: n in dom PR3 by FINSEQ_3:25;

end;assume ( 1 <= n & n <= len PR3 ) ; :: thesis: PR3,n is_a_correct_step

then A11: n in dom PR3 by FINSEQ_3:25;

A12: now :: thesis: ( ex k being Nat st

( k in dom PR2 & n = (len (PR ^ PR1)) + k ) implies PR3,n is_a_correct_step )

( k in dom PR2 & n = (len (PR ^ PR1)) + k ) implies PR3,n is_a_correct_step )

given k being Nat such that A13:
k in dom PR2
and

A14: n = (len (PR ^ PR1)) + k ; :: thesis: PR3,n is_a_correct_step

k in Seg 1 by A13, FINSEQ_1:38;

then A15: k = 1 by FINSEQ_1:2, TARSKI:def 1;

then A16: PR2 . k = [((Ant (Ant f)) ^ <*p*>),4] by FINSEQ_1:40;

then (PR2 . k) `1 = (Ant (Ant f)) ^ <*p*> ;

then A17: (PR3 . n) `1 = (Ant (Ant f)) ^ <*p*> by A13, A14, FINSEQ_1:def 7;

(PR2 . k) `2 = 4 by A16;

then A18: (PR3 . n) `2 = 4 by A13, A14, FINSEQ_1:def 7;

A19: len (PR ^ PR1) < n by A14, A15, NAT_1:13;

A20: 1 <= len PR by A10, Th6;

then len PR in dom PR by FINSEQ_3:25;

then A21: f = ((PR ^ PR1) . (len PR)) `1 by A7, FINSEQ_1:def 7;

A22: PR1 <> {} by A4;

then A23: len PR < len (PR ^ PR1) by Th6;

then len PR in dom (PR ^ PR1) by A20, FINSEQ_3:25;

then A24: f = (PR3 . (len PR)) `1 by A21, FINSEQ_1:def 7;

1 <= len PR1 by A22, Th6;

then len PR1 in dom PR1 by FINSEQ_3:25;

then g = ((PR ^ PR1) . ((len PR) + (len PR1))) `1 by A5, FINSEQ_1:def 7;

then A25: g = ((PR ^ PR1) . (len (PR ^ PR1))) `1 by FINSEQ_1:22;

1 <= len (PR ^ PR1) by A10, Th6;

then len (PR ^ PR1) in dom (PR ^ PR1) by FINSEQ_3:25;

then A26: g = (PR3 . (len (PR ^ PR1))) `1 by A25, FINSEQ_1:def 7;

1 <= len (PR ^ PR1) by A10, Th6;

hence PR3,n is_a_correct_step by A1, A17, A18, A20, A23, A24, A19, A26, Def7; :: thesis: verum

end;A14: n = (len (PR ^ PR1)) + k ; :: thesis: PR3,n is_a_correct_step

k in Seg 1 by A13, FINSEQ_1:38;

then A15: k = 1 by FINSEQ_1:2, TARSKI:def 1;

then A16: PR2 . k = [((Ant (Ant f)) ^ <*p*>),4] by FINSEQ_1:40;

then (PR2 . k) `1 = (Ant (Ant f)) ^ <*p*> ;

then A17: (PR3 . n) `1 = (Ant (Ant f)) ^ <*p*> by A13, A14, FINSEQ_1:def 7;

(PR2 . k) `2 = 4 by A16;

then A18: (PR3 . n) `2 = 4 by A13, A14, FINSEQ_1:def 7;

A19: len (PR ^ PR1) < n by A14, A15, NAT_1:13;

A20: 1 <= len PR by A10, Th6;

then len PR in dom PR by FINSEQ_3:25;

then A21: f = ((PR ^ PR1) . (len PR)) `1 by A7, FINSEQ_1:def 7;

A22: PR1 <> {} by A4;

then A23: len PR < len (PR ^ PR1) by Th6;

then len PR in dom (PR ^ PR1) by A20, FINSEQ_3:25;

then A24: f = (PR3 . (len PR)) `1 by A21, FINSEQ_1:def 7;

1 <= len PR1 by A22, Th6;

then len PR1 in dom PR1 by FINSEQ_3:25;

then g = ((PR ^ PR1) . ((len PR) + (len PR1))) `1 by A5, FINSEQ_1:def 7;

then A25: g = ((PR ^ PR1) . (len (PR ^ PR1))) `1 by FINSEQ_1:22;

1 <= len (PR ^ PR1) by A10, Th6;

then len (PR ^ PR1) in dom (PR ^ PR1) by FINSEQ_3:25;

then A26: g = (PR3 . (len (PR ^ PR1))) `1 by A25, FINSEQ_1:def 7;

1 <= len (PR ^ PR1) by A10, Th6;

hence PR3,n is_a_correct_step by A1, A17, A18, A20, A23, A24, A19, A26, Def7; :: thesis: verum

now :: thesis: ( n in dom (PR ^ PR1) implies PR3,n is_a_correct_step )

hence PR3,n is_a_correct_step by A34, A27, FINSEQ_1:25; :: thesis: verum

end;

hence
PR3,n is_a_correct_step
by A11, A12, FINSEQ_1:25; :: thesis: verumA27: now :: thesis: ( ex k being Nat st

( k in dom PR1 & n = (len PR) + k ) implies PR3,n is_a_correct_step )

( k in dom PR1 & n = (len PR) + k ) implies PR3,n is_a_correct_step )

given k being Nat such that A28:
k in dom PR1
and

A29: n = (len PR) + k ; :: thesis: PR3,n is_a_correct_step

A30: 1 <= k by A28, FINSEQ_3:25;

A31: k <= len PR1 by A28, FINSEQ_3:25;

then n <= (len PR1) + (len PR) by A29, XREAL_1:6;

then A32: n <= len (PR ^ PR1) by FINSEQ_1:22;

k <= n by A29, NAT_1:11;

then A33: 1 <= n by A30, XXREAL_0:2;

PR1,k is_a_correct_step by A4, A30, A31;

then PR ^ PR1,n is_a_correct_step by A29, A30, A31, Th35;

hence PR3,n is_a_correct_step by A33, A32, Th34; :: thesis: verum

end;A29: n = (len PR) + k ; :: thesis: PR3,n is_a_correct_step

A30: 1 <= k by A28, FINSEQ_3:25;

A31: k <= len PR1 by A28, FINSEQ_3:25;

then n <= (len PR1) + (len PR) by A29, XREAL_1:6;

then A32: n <= len (PR ^ PR1) by FINSEQ_1:22;

k <= n by A29, NAT_1:11;

then A33: 1 <= n by A30, XXREAL_0:2;

PR1,k is_a_correct_step by A4, A30, A31;

then PR ^ PR1,n is_a_correct_step by A29, A30, A31, Th35;

hence PR3,n is_a_correct_step by A33, A32, Th34; :: thesis: verum

A34: now :: thesis: ( n in dom PR implies PR3,n is_a_correct_step )

assume
n in dom (PR ^ PR1)
; :: thesis: PR3,n is_a_correct_step assume A35:
n in dom PR
; :: thesis: PR3,n is_a_correct_step

then A36: 1 <= n by FINSEQ_3:25;

A37: n <= len PR by A35, FINSEQ_3:25;

len PR <= len (PR ^ PR1) by Th6;

then A38: n <= len (PR ^ PR1) by A37, XXREAL_0:2;

PR,n is_a_correct_step by A6, A36, A37;

then PR ^ PR1,n is_a_correct_step by A36, A37, Th34;

hence PR3,n is_a_correct_step by A36, A38, Th34; :: thesis: verum

end;then A36: 1 <= n by FINSEQ_3:25;

A37: n <= len PR by A35, FINSEQ_3:25;

len PR <= len (PR ^ PR1) by Th6;

then A38: n <= len (PR ^ PR1) by A37, XXREAL_0:2;

PR,n is_a_correct_step by A6, A36, A37;

then PR ^ PR1,n is_a_correct_step by A36, A37, Th34;

hence PR3,n is_a_correct_step by A36, A38, Th34; :: thesis: verum

hence PR3,n is_a_correct_step by A34, A27, FINSEQ_1:25; :: thesis: verum

PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + (len PR2)) by FINSEQ_1:22;

then PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + 1) by FINSEQ_1:39;

then PR3 . (len PR3) = PR2 . 1 by A9, FINSEQ_1:def 7;

then PR3 . (len PR3) = [((Ant (Ant f)) ^ <*p*>),4] by FINSEQ_1:40;

then (PR3 . (len PR3)) `1 = (Ant (Ant f)) ^ <*p*> ;

hence |- (Ant (Ant f)) ^ <*p*> by A39; :: thesis: verum