begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
deffunc H1( set ) -> set = $1 `1 ;
theorem
theorem
:: deftheorem Def1 defines being_a_theory CQC_THE1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def2 defines Cn CQC_THE1:def 2 :
theorem
canceled;
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
Lm1:
for X being Subset of CQC-WFF holds Cn (Cn X) c= Cn X
theorem
theorem Th41:
:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :
theorem
canceled;
theorem Th43:
theorem
theorem Th45:
definition
let PR be
FinSequence of
[:CQC-WFF ,Proof_Step_Kinds :];
let n be
Nat;
let X be
Subset of
CQC-WFF ;
pred PR,
n is_a_correct_step_wrt X means :
Def4:
(PR . n) `1 in X if (PR . n) `2 = 0 (PR . n) `1 = VERUM if (PR . n) `2 = 1
ex
p being
Element of
CQC-WFF st
(PR . n) `1 = (('not' p) => p) => p if (PR . n) `2 = 2
ex
p,
q being
Element of
CQC-WFF st
(PR . n) `1 = p => (('not' p) => q) if (PR . n) `2 = 3
ex
p,
q,
r being
Element of
CQC-WFF st
(PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) if (PR . n) `2 = 4
ex
p,
q being
Element of
CQC-WFF st
(PR . n) `1 = (p '&' q) => (q '&' p) if (PR . n) `2 = 5
ex
p being
Element of
CQC-WFF ex
x being
bound_QC-variable st
(PR . n) `1 = (All x,p) => p if (PR . n) `2 = 6
ex
i,
j being
Element of
NAT ex
p,
q being
Element of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
p = (PR . j) `1 &
q = (PR . n) `1 &
(PR . i) `1 = p => q )
if (PR . n) `2 = 7
ex
i being
Element of
NAT ex
p,
q being
Element of
CQC-WFF ex
x being
bound_QC-variable st
( 1
<= i &
i < n &
(PR . i) `1 = p => q & not
x in still_not-bound_in p &
(PR . n) `1 = p => (All x,q) )
if (PR . n) `2 = 8
ex
i being
Element of
NAT ex
x,
y being
bound_QC-variable ex
s being
QC-formula st
( 1
<= i &
i < n &
s . x in CQC-WFF &
s . y in CQC-WFF & not
x in still_not-bound_in s &
s . x = (PR . i) `1 &
s . y = (PR . n) `1 )
if (PR . n) `2 = 9
;
consistency
( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( (PR . n) `1 in X iff (PR . n) `1 = VERUM ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 3 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 4 implies ( (PR . n) `1 in X iff ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 5 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 6 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 7 implies ( (PR . n) `1 in X iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( (PR . n) `1 in X iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( (PR . n) `1 in X iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( (PR . n) `1 = VERUM iff ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( (PR . n) `1 = VERUM iff ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( (PR . n) `1 = VERUM iff ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 5 implies ( (PR . n) `1 = VERUM iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( (PR . n) `1 = VERUM iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( (PR . n) `1 = VERUM iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( (PR . n) `1 = VERUM iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( (PR . n) `1 = VERUM iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 5 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 5 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 6 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 7 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All x,q) ) iff ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) )
;
end;
:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :
for
PR being
FinSequence of
[:CQC-WFF ,Proof_Step_Kinds :] for
n being
Nat for
X being
Subset of
CQC-WFF holds
( (
(PR . n) `2 = 0 implies (
PR,
n is_a_correct_step_wrt X iff
(PR . n) `1 in X ) ) & (
(PR . n) `2 = 1 implies (
PR,
n is_a_correct_step_wrt X iff
(PR . n) `1 = VERUM ) ) & (
(PR . n) `2 = 2 implies (
PR,
n is_a_correct_step_wrt X iff ex
p being
Element of
CQC-WFF st
(PR . n) `1 = (('not' p) => p) => p ) ) & (
(PR . n) `2 = 3 implies (
PR,
n is_a_correct_step_wrt X iff ex
p,
q being
Element of
CQC-WFF st
(PR . n) `1 = p => (('not' p) => q) ) ) & (
(PR . n) `2 = 4 implies (
PR,
n is_a_correct_step_wrt X iff ex
p,
q,
r being
Element of
CQC-WFF st
(PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & (
(PR . n) `2 = 5 implies (
PR,
n is_a_correct_step_wrt X iff ex
p,
q being
Element of
CQC-WFF st
(PR . n) `1 = (p '&' q) => (q '&' p) ) ) & (
(PR . n) `2 = 6 implies (
PR,
n is_a_correct_step_wrt X iff ex
p being
Element of
CQC-WFF ex
x being
bound_QC-variable st
(PR . n) `1 = (All x,p) => p ) ) & (
(PR . n) `2 = 7 implies (
PR,
n is_a_correct_step_wrt X iff ex
i,
j being
Element of
NAT ex
p,
q being
Element of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
p = (PR . j) `1 &
q = (PR . n) `1 &
(PR . i) `1 = p => q ) ) ) & (
(PR . n) `2 = 8 implies (
PR,
n is_a_correct_step_wrt X iff ex
i being
Element of
NAT ex
p,
q being
Element of
CQC-WFF ex
x being
bound_QC-variable st
( 1
<= i &
i < n &
(PR . i) `1 = p => q & not
x in still_not-bound_in p &
(PR . n) `1 = p => (All x,q) ) ) ) & (
(PR . n) `2 = 9 implies (
PR,
n is_a_correct_step_wrt X iff ex
i being
Element of
NAT ex
x,
y being
bound_QC-variable ex
s being
QC-formula st
( 1
<= i &
i < n &
s . x in CQC-WFF &
s . y in CQC-WFF & not
x in still_not-bound_in s &
s . x = (PR . i) `1 &
s . y = (PR . n) `1 ) ) ) );
:: deftheorem Def5 defines is_a_proof_wrt CQC_THE1:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem
theorem Th64:
:: deftheorem Def6 defines Effect CQC_THE1:def 6 :
theorem
canceled;
theorem Th66:
Lm2:
for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } c= CQC-WFF
theorem Th67:
Lm3:
for X being Subset of CQC-WFF holds VERUM 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 ) }
Lm4:
for p being Element of CQC-WFF
for X being Subset of CQC-WFF holds (('not' p) => 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 ) }
Lm5:
for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds p => (('not' 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 ) }
Lm6:
for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) 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 ) }
Lm7:
for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds (p '&' q) => (q '&' 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 ) }
Lm8:
for p, q being 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 ) }
Lm9:
for p being 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 ) }
Lm10:
for p, q being Element of CQC-WFF
for x being bound_QC-variable
for X being Subset of CQC-WFF st 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 ) } & not x in still_not-bound_in p holds
p => (All x,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 ) }
Lm11:
for s being QC-formula
for x, y being bound_QC-variable
for X being Subset of CQC-WFF st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x 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 ) } holds
s . y 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 ) }
theorem Th68:
Lm12:
for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } c= Cn X
theorem Th69:
theorem Th70:
theorem
:: deftheorem CQC_THE1:def 7 :
canceled;
:: deftheorem defines TAUT CQC_THE1:def 8 :
theorem
canceled;
theorem
canceled;
theorem Th74:
theorem
theorem Th76:
theorem Th77:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines |- CQC_THE1:def 9 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def10 defines valid CQC_THE1:def 10 :
Lm13:
for s being QC-formula holds
( s is valid iff s in TAUT )
:: deftheorem defines valid CQC_THE1:def 11 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem