:: deftheorem Def7 defines is_a_correct_step CALCUL_1:def 7 :
for Al being QC-alphabet
for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),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 Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step iff ex i being Nat ex f, g being FinSequence of CQC-WFF Al 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 Nat ex f, g being FinSequence of CQC-WFF Al 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 Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al 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 Nat ex f, g being FinSequence of CQC-WFF Al 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 Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 ) ) ) );