let p, q be Element of CQC-WFF ; :: thesis: 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 ; :: thesis: ( 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 ) }
; :: thesis: 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 ) }
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;
then consider f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that
A3:
( f is_a_proof_wrt X & Effect f = p )
;
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;
then consider g being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that
A4:
( g is_a_proof_wrt X & Effect g = p => q )
;
A5:
( f <> {} & g <> {} )
by A3, A4, Def5;
reconsider qq = [q,7] as Element of [:CQC-WFF ,Proof_Step_Kinds :] by Th43, ZFMISC_1:106;
set h = (f ^ g) ^ <*qq*>;
A6: len ((f ^ g) ^ <*qq*>) =
(len (f ^ g)) + (len <*qq*>)
by FINSEQ_1:35
.=
(len (f ^ g)) + 1
by FINSEQ_1:57
;
then A7:
len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1
by FINSEQ_1:35;
((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq
by A6, FINSEQ_1:59;
then
(((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q
by MCART_1:7;
then A8:
Effect ((f ^ g) ^ <*qq*>) = q
by Def6;
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 ;
:: thesis: ( 1 <= n & n <= len ((f ^ g) ^ <*qq*>) implies (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X )
assume A9:
( 1
<= n &
n <= len ((f ^ g) ^ <*qq*>) )
;
:: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
now per cases
( n <= (len f) + (len g) or n = len ((f ^ g) ^ <*qq*>) )
by A7, A9, NAT_1:8;
suppose A11:
n = len ((f ^ g) ^ <*qq*>)
;
:: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt Xthen
((f ^ g) ^ <*qq*>) . n = qq
by A6, FINSEQ_1:59;
then A12:
(
(((f ^ g) ^ <*qq*>) . n) `2 = 7 &
(((f ^ g) ^ <*qq*>) . n) `1 = q )
by MCART_1:7;
len f <> 0
by A3, Th58;
then
len f in Seg (len f)
by FINSEQ_1:5;
then
(
len f in dom f &
(f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>) )
by FINSEQ_1:45, FINSEQ_1:def 3;
then A13:
(((f ^ g) ^ <*qq*>) . (len f)) `1 =
(f . (len f)) `1
by FINSEQ_1:def 7
.=
p
by A3, A5, Def6
;
(
dom g = Seg (len g) &
len g <> 0 )
by A4, Th58, FINSEQ_1:def 3;
then A14:
len g in dom g
by FINSEQ_1:5;
( 1
<= len f &
len f <= (len f) + (len g) )
by A3, Th58, NAT_1:11;
then
(len f) + (len g) in Seg ((len f) + (len g))
by FINSEQ_1:5;
then
(len f) + (len g) in Seg (len (f ^ g))
by FINSEQ_1:35;
then
(len f) + (len g) in dom (f ^ g)
by FINSEQ_1:def 3;
then A15:
(((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 A14, FINSEQ_1:def 7
.=
p => q
by A4, A5, Def6
;
( 1
<= len g &
len f <= len f )
by A4, Th58;
then
(
len f < (len f) + 1 &
(len f) + 1
<= (len f) + (len g) )
by NAT_1:13, XREAL_1:9;
then A16:
( 1
<= len f &
len f < (len f) + (len g) )
by A3, Th58, XXREAL_0:2;
then
( 1
<= (len f) + (len g) &
(len f) + (len g) < n )
by A7, A11, NAT_1:12, NAT_1:13;
hence
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
by A12, A13, A15, A16, Def4;
:: thesis: verum end;
hence
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
;
:: thesis: verum
end;
then
(f ^ g) ^ <*qq*> is_a_proof_wrt X
by Def5;
hence
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 A8; :: thesis: verum