begin
:: deftheorem Def1 defines Ant CALCUL_1:def 1 :
:: deftheorem Def2 defines Suc CALCUL_1:def 2 :
:: deftheorem Def3 defines is_tail_of CALCUL_1:def 3 :
:: deftheorem Def4 defines is_Subsequence_of CALCUL_1:def 4 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
begin
:: deftheorem Def5 defines still_not-bound_in CALCUL_1:def 5 :
:: deftheorem Def6 defines set_of_CQC-WFF-seq CALCUL_1:def 6 :
definition
let PR be
FinSequence of
[:set_of_CQC-WFF-seq ,Proof_Step_Kinds :];
let n be
Nat;
pred PR,
n is_a_correct_step means :
Def7:
ex
f being
FinSequence of
CQC-WFF st
(
Suc f is_tail_of Ant f &
(PR . n) `1 = f )
if (PR . n) `2 = 0 ex
f being
FinSequence of
CQC-WFF st
(PR . n) `1 = f ^ <*VERUM *> if (PR . n) `2 = 1
ex
i being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF st
( 1
<= i &
i < n &
Ant f is_Subsequence_of Ant g &
Suc f = Suc g &
(PR . i) `1 = f &
(PR . n) `1 = g )
if (PR . n) `2 = 2
ex
i,
j being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
len f > 1 &
len g > 1 &
Ant (Ant f) = Ant (Ant g) &
'not' (Suc (Ant f)) = Suc (Ant g) &
Suc f = Suc g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 )
if (PR . n) `2 = 3
ex
i,
j being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF ex
p being
Element of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
len f > 1 &
Ant f = Ant g &
Suc (Ant f) = 'not' p &
'not' (Suc f) = Suc g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*p*> = (PR . n) `1 )
if (PR . n) `2 = 4
ex
i,
j being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
Ant f = Ant g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 )
if (PR . n) `2 = 5
ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p,
q being
Element of
CQC-WFF st
( 1
<= i &
i < n &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*p*> = (PR . n) `1 )
if (PR . n) `2 = 6
ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p,
q being
Element of
CQC-WFF st
( 1
<= i &
i < n &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*q*> = (PR . n) `1 )
if (PR . n) `2 = 7
ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p being
Element of
CQC-WFF ex
x,
y being
bound_QC-variable st
( 1
<= i &
i < n &
Suc f = All x,
p &
f = (PR . i) `1 &
(Ant f) ^ <*(p . x,y)*> = (PR . n) `1 )
if (PR . n) `2 = 8
ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p being
Element of
CQC-WFF ex
x,
y being
bound_QC-variable st
( 1
<= i &
i < n &
Suc f = p . x,
y & not
y in still_not-bound_in (Ant f) & not
y in still_not-bound_in (All x,p) &
f = (PR . i) `1 &
(Ant f) ^ <*(All x,p)*> = (PR . n) `1 )
if (PR . n) `2 = 9
;
consistency
( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 3 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 4 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 5 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 6 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 7 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 5 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 5 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 5 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 6 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 7 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 6 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 7 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 7 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) )
;
end;
:: deftheorem Def7 defines is_a_correct_step CALCUL_1:def 7 :
for
PR being
FinSequence of
[:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] for
n being
Nat holds
( (
(PR . n) `2 = 0 implies (
PR,
n is_a_correct_step iff ex
f being
FinSequence of
CQC-WFF st
(
Suc f is_tail_of Ant f &
(PR . n) `1 = f ) ) ) & (
(PR . n) `2 = 1 implies (
PR,
n is_a_correct_step iff ex
f being
FinSequence of
CQC-WFF st
(PR . n) `1 = f ^ <*VERUM *> ) ) & (
(PR . n) `2 = 2 implies (
PR,
n is_a_correct_step iff ex
i being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF st
( 1
<= i &
i < n &
Ant f is_Subsequence_of Ant g &
Suc f = Suc g &
(PR . i) `1 = f &
(PR . n) `1 = g ) ) ) & (
(PR . n) `2 = 3 implies (
PR,
n is_a_correct_step iff ex
i,
j being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
len f > 1 &
len g > 1 &
Ant (Ant f) = Ant (Ant g) &
'not' (Suc (Ant f)) = Suc (Ant g) &
Suc f = Suc g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & (
(PR . n) `2 = 4 implies (
PR,
n is_a_correct_step iff ex
i,
j being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF ex
p being
Element of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
len f > 1 &
Ant f = Ant g &
Suc (Ant f) = 'not' p &
'not' (Suc f) = Suc g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & (
(PR . n) `2 = 5 implies (
PR,
n is_a_correct_step iff ex
i,
j being
Element of
NAT ex
f,
g being
FinSequence of
CQC-WFF st
( 1
<= i &
i < n & 1
<= j &
j < i &
Ant f = Ant g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & (
(PR . n) `2 = 6 implies (
PR,
n is_a_correct_step iff ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p,
q being
Element of
CQC-WFF st
( 1
<= i &
i < n &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & (
(PR . n) `2 = 7 implies (
PR,
n is_a_correct_step iff ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p,
q being
Element of
CQC-WFF st
( 1
<= i &
i < n &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & (
(PR . n) `2 = 8 implies (
PR,
n is_a_correct_step iff ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p being
Element of
CQC-WFF ex
x,
y being
bound_QC-variable st
( 1
<= i &
i < n &
Suc f = All x,
p &
f = (PR . i) `1 &
(Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & (
(PR . n) `2 = 9 implies (
PR,
n is_a_correct_step iff ex
i being
Element of
NAT ex
f being
FinSequence of
CQC-WFF ex
p being
Element of
CQC-WFF ex
x,
y being
bound_QC-variable st
( 1
<= i &
i < n &
Suc f = p . x,
y & not
y in still_not-bound_in (Ant f) & not
y in still_not-bound_in (All x,p) &
f = (PR . i) `1 &
(Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) );
:: deftheorem Def8 defines a_proof CALCUL_1:def 8 :
:: deftheorem Def9 defines |- CALCUL_1:def 9 :
:: deftheorem Def10 defines is_formal_provable_from CALCUL_1:def 10 :
:: deftheorem Def11 defines |= CALCUL_1:def 11 :
:: deftheorem defines |= CALCUL_1:def 12 :
:: deftheorem defines |= CALCUL_1:def 13 :
:: deftheorem Def14 defines |= CALCUL_1:def 14 :
:: deftheorem Def15 defines |= CALCUL_1:def 15 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
Lm1:
for n being Element of NAT
for PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= n & n <= len PR holds
(PR . n) `1 is FinSequence of CQC-WFF
theorem
begin
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem
theorem
theorem
theorem Th53:
theorem Th54:
theorem Th55:
theorem
theorem Th57:
theorem
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem