let p be Element of CQC-WFF ; for x being bound_QC-variable
for X being Subset of CQC-WFF holds (All x,p) => 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 ) }
let x be bound_QC-variable; for X being Subset of CQC-WFF holds (All x,p) => 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 ) }
let X be Subset of CQC-WFF ; (All x,p) => 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 ) }
reconsider pp = [((All x,p) => p),6] as Element of [:CQC-WFF ,Proof_Step_Kinds :] by Th43, ZFMISC_1:106;
set f = <*pp*>;
A1:
len <*pp*> = 1
by FINSEQ_1:57;
A2:
<*pp*> . 1 = pp
by FINSEQ_1:57;
A3:
(<*pp*> . (len <*pp*>)) `1 = (All x,p) => p
by A1, A2, MCART_1:7;
A4:
Effect <*pp*> = (All x,p) => p
by A3, Def6;
A5:
for n being Element of NAT st 1 <= n & n <= len <*pp*> holds
<*pp*>,n is_a_correct_step_wrt X
proof
let n be
Element of
NAT ;
( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X )
assume A6:
( 1
<= n &
n <= len <*pp*> )
;
<*pp*>,n is_a_correct_step_wrt X
A7:
n = 1
by A1, A6, XXREAL_0:1;
A8:
(<*pp*> . 1) `2 = 6
by A2, MCART_1:7;
A9:
(<*pp*> . n) `1 = (All x,p) => p
by A2, A7, MCART_1:7;
thus
<*pp*>,
n is_a_correct_step_wrt X
by A7, A8, A9, Def4;
verum
end;
A10:
<*pp*> is_a_proof_wrt X
by A5, Def5;
thus
(All x,p) => 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 ) }
by A4, A10; verum