let p, q be Element of CQC-WFF ; for X being Subset of CQC-WFF st p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) } holds
q in { H where H is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = H ) }
let X be Subset of CQC-WFF ; ( p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) } implies q in { H where H is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,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 : ex f being FinSequence of [:CQC-WFF ,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 : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
; q in { H where H is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = H ) }
A3:
ex t being Element of CQC-WFF st
( t = p & ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = t ) )
by A1;
consider f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that
A4:
f is_a_proof_wrt X
and
A5:
Effect f = p
by A3;
A6:
ex r being Element of CQC-WFF st
( r = p => q & ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = r ) )
by A2;
consider g being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that
A7:
g is_a_proof_wrt X
and
A8:
Effect g = p => q
by A6;
A9:
f <> {}
by A4, Def5;
A10:
g <> {}
by A7, Def5;
reconsider qq = [q,7] as Element of [:CQC-WFF ,Proof_Step_Kinds :] by Th43, ZFMISC_1:106;
set h = (f ^ g) ^ <*qq*>;
A11: len ((f ^ g) ^ <*qq*>) =
(len (f ^ g)) + (len <*qq*>)
by FINSEQ_1:35
.=
(len (f ^ g)) + 1
by FINSEQ_1:57
;
A12:
len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1
by A11, FINSEQ_1:35;
A13:
((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq
by A11, FINSEQ_1:59;
A14:
(((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q
by A13, MCART_1:7;
A15:
Effect ((f ^ g) ^ <*qq*>) = q
by A14, Def6;
A16:
for n being Element of NAT st 1 <= n & n <= len ((f ^ g) ^ <*qq*>) holds
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
proof
let n be
Element of
NAT ;
( 1 <= n & n <= len ((f ^ g) ^ <*qq*>) implies (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X )
assume that A17:
1
<= n
and A18:
n <= len ((f ^ g) ^ <*qq*>)
;
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
A19:
now per cases
( n <= (len f) + (len g) or n = len ((f ^ g) ^ <*qq*>) )
by A12, A18, NAT_1:8;
suppose A20:
n <= (len f) + (len g)
;
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt XA21:
n <= len (f ^ g)
by A20, FINSEQ_1:35;
A22:
f ^ g is_a_proof_wrt X
by A4, A7, Th62;
A23:
f ^ g,
n is_a_correct_step_wrt X
by A17, A21, A22, Def5;
thus
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
by A17, A21, A23, Th60;
verum end; suppose A24:
n = len ((f ^ g) ^ <*qq*>)
;
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt XA25:
((f ^ g) ^ <*qq*>) . n = qq
by A11, A24, FINSEQ_1:59;
A26:
(
(((f ^ g) ^ <*qq*>) . n) `2 = 7 &
(((f ^ g) ^ <*qq*>) . n) `1 = q )
by A25, MCART_1:7;
A27:
len f <> 0
by A4, Th58;
A28:
len f in Seg (len f)
by A27, FINSEQ_1:5;
A29:
len f in dom f
by A28, FINSEQ_1:def 3;
A30:
(f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>)
by FINSEQ_1:45;
A31:
(((f ^ g) ^ <*qq*>) . (len f)) `1 =
(f . (len f)) `1
by A29, A30, FINSEQ_1:def 7
.=
p
by A5, A9, Def6
;
A32:
(
dom g = Seg (len g) &
len g <> 0 )
by A7, Th58, FINSEQ_1:def 3;
A33:
len g in dom g
by A32, FINSEQ_1:5;
A34:
( 1
<= len f &
len f <= (len f) + (len g) )
by A4, Th58, NAT_1:11;
A35:
(len f) + (len g) in Seg ((len f) + (len g))
by A34, FINSEQ_1:5;
A36:
(len f) + (len g) in Seg (len (f ^ g))
by A35, FINSEQ_1:35;
A37:
(len f) + (len g) in dom (f ^ g)
by A36, FINSEQ_1:def 3;
A38:
(((f ^ g) ^ <*qq*>) . ((len f) + (len g))) `1 =
((f ^ g) . ((len f) + (len g))) `1
by A37, FINSEQ_1:def 7
.=
(g . (len g)) `1
by A33, FINSEQ_1:def 7
.=
p => q
by A8, A10, Def6
;
A39:
1
<= len g
by A7, Th58;
A40:
(len f) + 1
<= (len f) + (len g)
by A39, XREAL_1:9;
A41:
len f < (len f) + (len g)
by A40, NAT_1:13;
A42:
( 1
<= len f & 1
<= (len f) + (len g) )
by A4, Th58, NAT_1:12;
A43:
(len f) + (len g) < n
by A12, A24, NAT_1:13;
thus
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
by A26, A31, A38, A41, A42, A43, Def4;
verum end;
thus
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
by A19;
verum
end;
A44:
(f ^ g) ^ <*qq*> is_a_proof_wrt X
by A16, Def5;
thus
q in { H where H is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = H ) }
by A15, A44; verum