let Al be QC-alphabet ; for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds
|- (Ant f) ^ <*p*>
let p, q be Element of CQC-WFF Al; for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds
|- (Ant f) ^ <*p*>
let f be FinSequence of CQC-WFF Al; ( p '&' q = Suc f & |- f implies |- (Ant f) ^ <*p*> )
assume that
A1:
p '&' q = Suc f
and
A2:
|- f
; |- (Ant f) ^ <*p*>
consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A3:
PR is a_proof
and
A4:
(PR . (len PR)) `1 = f
by A2;
A5:
(Ant f) ^ <*p*> in set_of_CQC-WFF-seq Al
by Def6;
then
rng <*[((Ant f) ^ <*p*>),6]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
;
then reconsider PR1 = <*[((Ant f) ^ <*p*>),6]*> 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 A6:
1 in dom PR1
by FINSEQ_1:38;
set PR2 = PR ^ PR1;
reconsider PR2 = PR ^ PR1 as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;
A7:
PR <> {}
by A3;
now for n being Nat st 1 <= n & n <= len PR2 holds
PR2,n is_a_correct_step let n be
Nat;
( 1 <= n & n <= len PR2 implies PR2,n is_a_correct_step )assume
( 1
<= n &
n <= len PR2 )
;
PR2,n is_a_correct_step then A8:
n in dom PR2
by FINSEQ_3:25;
A9:
now ( ex k being Nat st
( k in dom PR1 & n = (len PR) + k ) implies PR2,n is_a_correct_step )A10:
1
<= len PR
by A7, Th6;
then
len PR in dom PR
by FINSEQ_3:25;
then A11:
f = (PR2 . (len PR)) `1
by A4, FINSEQ_1:def 7;
given k being
Nat such that A12:
k in dom PR1
and A13:
n = (len PR) + k
;
PR2,n is_a_correct_step
k in Seg 1
by A12, FINSEQ_1:38;
then A14:
k = 1
by FINSEQ_1:2, TARSKI:def 1;
then A15:
PR1 . k = [((Ant f) ^ <*p*>),6]
by FINSEQ_1:40;
then
(PR1 . k) `1 = (Ant f) ^ <*p*>
;
then A16:
(PR2 . n) `1 = (Ant f) ^ <*p*>
by A12, A13, FINSEQ_1:def 7;
(PR1 . k) `2 = 6
by A15;
then A17:
(PR2 . n) `2 = 6
by A12, A13, FINSEQ_1:def 7;
len PR < n
by A13, A14, NAT_1:13;
hence
PR2,
n is_a_correct_step
by A1, A16, A17, A10, A11, Def7;
verum end; hence
PR2,
n is_a_correct_step
by A8, A9, FINSEQ_1:25;
verum end;
then A19:
PR2 is a_proof
;
PR2 . (len PR2) = PR2 . ((len PR) + (len PR1))
by FINSEQ_1:22;
then
PR2 . (len PR2) = PR2 . ((len PR) + 1)
by FINSEQ_1:39;
then
PR2 . (len PR2) = PR1 . 1
by A6, FINSEQ_1:def 7;
then
PR2 . (len PR2) = [((Ant f) ^ <*p*>),6]
by FINSEQ_1:40;
then
(PR2 . (len PR2)) `1 = (Ant f) ^ <*p*>
;
hence
|- (Ant f) ^ <*p*>
by A19; verum