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 ) }
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
and
A4:
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
A5:
g is_a_proof_wrt X
and
A6:
Effect g = p => q
;
A7:
f <> {}
by A3, Def5;
A8:
g <> {}
by A5, Def5;
reconsider qq = [q,7] as Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43, ZFMISC_1:87;
set h = (f ^ g) ^ <*qq*>;
A9: len ((f ^ g) ^ <*qq*>) =
(len (f ^ g)) + (len <*qq*>)
by FINSEQ_1:22
.=
(len (f ^ g)) + 1
by FINSEQ_1:40
;
then A10:
len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1
by FINSEQ_1:22;
((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq
by A9, FINSEQ_1:42;
then
(((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q
by MCART_1:7;
then A11:
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 ;
( 1 <= n & n <= len ((f ^ g) ^ <*qq*>) implies (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X )
assume that A12:
1
<= n
and A13:
n <= len ((f ^ g) ^ <*qq*>)
;
(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 A10, A13, NAT_1:8;
suppose A15:
n = len ((f ^ g) ^ <*qq*>)
;
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt Xthen
((f ^ g) ^ <*qq*>) . n = qq
by A9, FINSEQ_1:42;
then A16:
(
(((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:3;
then A17:
len f in dom f
by FINSEQ_1:def 3;
(f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>)
by FINSEQ_1:32;
then A18:
(((f ^ g) ^ <*qq*>) . (len f)) `1 =
(f . (len f)) `1
by A17, FINSEQ_1:def 7
.=
p
by A4, A7, Def6
;
(
dom g = Seg (len g) &
len g <> 0 )
by A5, Th58, FINSEQ_1:def 3;
then A19:
len g in dom g
by FINSEQ_1:3;
( 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: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 A20:
(((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 A19, FINSEQ_1:def 7
.=
p => q
by A6, A8, Def6
;
1
<= len g
by A5, Th58;
then
(len f) + 1
<= (len f) + (len g)
by XREAL_1:7;
then A21:
len f < (len f) + (len g)
by NAT_1:13;
A22:
( 1
<= len f & 1
<= (len f) + (len g) )
by A3, Th58, NAT_1:12;
(len f) + (len g) < n
by A10, A15, NAT_1:13;
hence
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
by A16, A18, A20, A21, A22, Def4;
verum end;
hence
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
;
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 A11; verum