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

for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) } holds

q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) }

let p, q be Element of CQC-WFF Al; :: thesis: for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) } holds

q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) }

let X be Subset of (CQC-WFF Al); :: thesis: ( p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) } implies q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) } )

assume that

A1: p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } and

A2: p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } ; :: thesis: q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) }

ex t being Element of CQC-WFF Al st

( t = p & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = t ) ) by A1;

then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A3: f is_a_proof_wrt X and

A4: Effect f = p ;

ex r being Element of CQC-WFF Al st

( r = p => q & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = r ) ) by A2;

then consider g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A5: g is_a_proof_wrt X and

A6: Effect g = p => q ;

reconsider qq = [q,7] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th17, ZFMISC_1:87;

set h = (f ^ g) ^ <*qq*>;

A7: len ((f ^ g) ^ <*qq*>) = (len (f ^ g)) + (len <*qq*>) by FINSEQ_1:22

.= (len (f ^ g)) + 1 by FINSEQ_1:40 ;

then A8: len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1 by FINSEQ_1:22;

((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq by A7, FINSEQ_1:42;

then (((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q ;

then A9: Effect ((f ^ g) ^ <*qq*>) = q by Def6;

for n being Nat st 1 <= n & n <= len ((f ^ g) ^ <*qq*>) holds

(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X

hence q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) } by A9; :: thesis: verum

for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) } holds

q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) }

let p, q be Element of CQC-WFF Al; :: thesis: for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) } holds

q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) }

let X be Subset of (CQC-WFF Al); :: thesis: ( p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) } implies q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) } )

assume that

A1: p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } and

A2: p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } ; :: thesis: q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) }

ex t being Element of CQC-WFF Al st

( t = p & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = t ) ) by A1;

then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A3: f is_a_proof_wrt X and

A4: Effect f = p ;

ex r being Element of CQC-WFF Al st

( r = p => q & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = r ) ) by A2;

then consider g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A5: g is_a_proof_wrt X and

A6: Effect g = p => q ;

reconsider qq = [q,7] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th17, ZFMISC_1:87;

set h = (f ^ g) ^ <*qq*>;

A7: len ((f ^ g) ^ <*qq*>) = (len (f ^ g)) + (len <*qq*>) by FINSEQ_1:22

.= (len (f ^ g)) + 1 by FINSEQ_1:40 ;

then A8: len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1 by FINSEQ_1:22;

((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq by A7, FINSEQ_1:42;

then (((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q ;

then A9: Effect ((f ^ g) ^ <*qq*>) = q by Def6;

for n being Nat st 1 <= n & n <= len ((f ^ g) ^ <*qq*>) holds

(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X

proof

then
(f ^ g) ^ <*qq*> is_a_proof_wrt X
;
let n be Nat; :: thesis: ( 1 <= n & n <= len ((f ^ g) ^ <*qq*>) implies (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X )

assume that

A10: 1 <= n and

A11: n <= len ((f ^ g) ^ <*qq*>) ; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X

end;assume that

A10: 1 <= n and

A11: n <= len ((f ^ g) ^ <*qq*>) ; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X

now :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt Xend;

hence
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
; :: thesis: verumper cases
( n <= (len f) + (len g) or n = len ((f ^ g) ^ <*qq*>) )
by A8, A11, NAT_1:8;

end;

suppose
n <= (len f) + (len g)
; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X

then A12:
n <= len (f ^ g)
by FINSEQ_1:22;

f ^ g is_a_proof_wrt X by A3, A5, Th25;

then f ^ g,n is_a_correct_step_wrt X by A10, A12;

hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A10, A12, Th23; :: thesis: verum

end;f ^ g is_a_proof_wrt X by A3, A5, Th25;

then f ^ g,n is_a_correct_step_wrt X by A10, A12;

hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A10, A12, Th23; :: thesis: verum

suppose A13:
n = len ((f ^ g) ^ <*qq*>)
; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X

then
((f ^ g) ^ <*qq*>) . n = qq
by A7, FINSEQ_1:42;

then A14: ( (((f ^ g) ^ <*qq*>) . n) `2 = 7 & (((f ^ g) ^ <*qq*>) . n) `1 = q ) ;

len f <> 0 by A3;

then len f in Seg (len f) by FINSEQ_1:3;

then A15: len f in dom f by FINSEQ_1:def 3;

(f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>) by FINSEQ_1:32;

then A16: (((f ^ g) ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by A15, FINSEQ_1:def 7

.= p by A4, A3, Def6 ;

( dom g = Seg (len g) & len g <> 0 ) by A5, FINSEQ_1:def 3;

then A17: len g in dom g by FINSEQ_1:3;

( 1 <= len f & len f <= (len f) + (len g) ) by A3, Th21, NAT_1:11;

then (len f) + (len g) in Seg ((len f) + (len g)) by FINSEQ_1:3;

then (len f) + (len g) in Seg (len (f ^ g)) by FINSEQ_1:22;

then (len f) + (len g) in dom (f ^ g) by FINSEQ_1:def 3;

then A18: (((f ^ g) ^ <*qq*>) . ((len f) + (len g))) `1 = ((f ^ g) . ((len f) + (len g))) `1 by FINSEQ_1:def 7

.= (g . (len g)) `1 by A17, FINSEQ_1:def 7

.= p => q by A6, A5, Def6 ;

1 <= len g by A5, Th21;

then (len f) + 1 <= (len f) + (len g) by XREAL_1:7;

then A19: len f < (len f) + (len g) by NAT_1:13;

A20: ( 1 <= len f & 1 <= (len f) + (len g) ) by A3, Th21, NAT_1:12;

(len f) + (len g) < n by A8, A13, NAT_1:13;

hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A14, A16, A18, A19, A20, Def4; :: thesis: verum

end;then A14: ( (((f ^ g) ^ <*qq*>) . n) `2 = 7 & (((f ^ g) ^ <*qq*>) . n) `1 = q ) ;

len f <> 0 by A3;

then len f in Seg (len f) by FINSEQ_1:3;

then A15: len f in dom f by FINSEQ_1:def 3;

(f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>) by FINSEQ_1:32;

then A16: (((f ^ g) ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by A15, FINSEQ_1:def 7

.= p by A4, A3, Def6 ;

( dom g = Seg (len g) & len g <> 0 ) by A5, FINSEQ_1:def 3;

then A17: len g in dom g by FINSEQ_1:3;

( 1 <= len f & len f <= (len f) + (len g) ) by A3, Th21, NAT_1:11;

then (len f) + (len g) in Seg ((len f) + (len g)) by FINSEQ_1:3;

then (len f) + (len g) in Seg (len (f ^ g)) by FINSEQ_1:22;

then (len f) + (len g) in dom (f ^ g) by FINSEQ_1:def 3;

then A18: (((f ^ g) ^ <*qq*>) . ((len f) + (len g))) `1 = ((f ^ g) . ((len f) + (len g))) `1 by FINSEQ_1:def 7

.= (g . (len g)) `1 by A17, FINSEQ_1:def 7

.= p => q by A6, A5, Def6 ;

1 <= len g by A5, Th21;

then (len f) + 1 <= (len f) + (len g) by XREAL_1:7;

then A19: len f < (len f) + (len g) by NAT_1:13;

A20: ( 1 <= len f & 1 <= (len f) + (len g) ) by A3, Th21, NAT_1:12;

(len f) + (len g) < n by A8, A13, NAT_1:13;

hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A14, A16, A18, A19, A20, Def4; :: thesis: verum

hence q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) } by A9; :: thesis: verum