let Al be QC-alphabet ; 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; 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); ( 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 ) }
; 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
let n be
Nat;
( 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*>)
;
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
now (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt Xper cases
( n <= (len f) + (len g) or n = len ((f ^ g) ^ <*qq*>) )
by A8, A11, NAT_1:8;
suppose A13:
n = len ((f ^ g) ^ <*qq*>)
;
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt Xthen
((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;
verum end; end; end;
hence
(f ^ g) ^ <*qq*>,
n is_a_correct_step_wrt X
;
verum
end;
then
(f ^ g) ^ <*qq*> is_a_proof_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; verum