:: deftheorem Def3 defines is_a_correct_step_wrt_IPC INTPRO_2:def 3 :
for PR being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]
for n being Nat
for X being Subset of MC-wff holds
( ( (PR . n) `2 = 0 implies ( PR,n is_a_correct_step_wrt_IPC X iff (PR . n) `1 in X ) ) & ( (PR . n) `2 = 1 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q being Element of MC-wff st (PR . n) `1 = p => (q => p) ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q, r being Element of MC-wff st (PR . n) `1 = (p => (q => r)) => ((p => q) => (p => r)) ) ) & ( (PR . n) `2 = 3 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q being Element of MC-wff st (PR . n) `1 = (p '&' q) => p ) ) & ( (PR . n) `2 = 4 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q being Element of MC-wff st (PR . n) `1 = (p '&' q) => q ) ) & ( (PR . n) `2 = 5 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q being Element of MC-wff st (PR . n) `1 = p => (q => (p '&' q)) ) ) & ( (PR . n) `2 = 6 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q being Element of MC-wff st (PR . n) `1 = p => (p 'or' q) ) ) & ( (PR . n) `2 = 7 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q being Element of MC-wff st (PR . n) `1 = q => (p 'or' q) ) ) & ( (PR . n) `2 = 8 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p, q, r being Element of MC-wff st (PR . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r)) ) ) & ( (PR . n) `2 = 9 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex p being Element of MC-wff st (PR . n) `1 = FALSUM => p ) ) & ( (PR . n) `2 = 10 implies ( PR,n is_a_correct_step_wrt_IPC X iff ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) );