let n be Nat; :: thesis: for X being Subset of MC-wff
for f, g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt_IPC X holds
f ^ g,n + (len f) is_a_correct_step_wrt_IPC X
let X be Subset of MC-wff; :: thesis: for f, g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt_IPC X holds
f ^ g,n + (len f) is_a_correct_step_wrt_IPC X
let f, g be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: ( 1 <= n & n <= len g & g,n is_a_correct_step_wrt_IPC X implies f ^ g,n + (len f) is_a_correct_step_wrt_IPC X )
assume that
A1: 1 <= n and
A2: n <= len g and
A3: g,n is_a_correct_step_wrt_IPC X ; :: thesis: f ^ g,n + (len f) is_a_correct_step_wrt_IPC X
n in dom g by A1, A2, FINSEQ_3:25;
then A4: g . n = (f ^ g) . (n + (len f)) by FINSEQ_1:def 7;
n + (len f) <= (len f) + (len g) by A2, XREAL_1:6;
then n + (len f) <= len (f ^ g) by FINSEQ_1:22;
then not not ((f ^ g) . (n + (len f))) `2 = 0 & ... & not ((f ^ g) . (n + (len f))) `2 = 10 by A1, Th3, NAT_1:12;
per cases then ( ((f ^ g) . (n + (len f))) `2 = 0 or ((f ^ g) . (n + (len f))) `2 = 1 or ((f ^ g) . (n + (len f))) `2 = 2 or ((f ^ g) . (n + (len f))) `2 = 3 or ((f ^ g) . (n + (len f))) `2 = 4 or ((f ^ g) . (n + (len f))) `2 = 5 or ((f ^ g) . (n + (len f))) `2 = 6 or ((f ^ g) . (n + (len f))) `2 = 7 or ((f ^ g) . (n + (len f))) `2 = 8 or ((f ^ g) . (n + (len f))) `2 = 9 or ((f ^ g) . (n + (len f))) `2 = 10 ) ;
:: according to INTPRO_2:def 3
case ((f ^ g) . (n + (len f))) `2 = 0 ; :: thesis: ((f ^ g) . (n + (len f))) `1 in X
hence ((f ^ g) . (n + (len f))) `1 in X by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 1 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = p => (q => p)
hence ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = p => (q => p) by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 2 ; :: thesis: ex p, q, r being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p => (q => r)) => ((p => q) => (p => r))
hence ex p, q, r being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p => (q => r)) => ((p => q) => (p => r)) by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 3 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => p
hence ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => p by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 4 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => q
hence ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => q by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 5 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = p => (q => (p '&' q))
hence ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = p => (q => (p '&' q)) by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 6 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = p => (p 'or' q)
hence ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = p => (p 'or' q) by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 7 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = q => (p 'or' q)
hence ex p, q being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = q => (p 'or' q) by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 8 ; :: thesis: ex p, q, r being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p => r) => ((q => r) => ((p 'or' q) => r))
hence ex p, q, r being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = (p => r) => ((q => r) => ((p 'or' q) => r)) by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 9 ; :: thesis: ex p being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = FALSUM => p
hence ex p being Element of MC-wff st ((f ^ g) . (n + (len f))) `1 = FALSUM => p by A3, A4, Def3; :: thesis: verum
end;
case ((f ^ g) . (n + (len f))) `2 = 10 ; :: thesis: ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q )
then consider i, j being Nat, r, t being Element of MC-wff such that
A5: 1 <= i and
A6: i < n and
A7: 1 <= j and
A8: j < i and
A9: ( r = (g . j) `1 & t = (g . n) `1 & (g . i) `1 = r => t ) by A3, A4, Def3;
A10: ( 1 <= i + (len f) & i + (len f) < n + (len f) ) by A5, A6, NAT_1:12, XREAL_1:6;
A11: ( 1 <= j + (len f) & j + (len f) < i + (len f) ) by A7, A8, NAT_1:12, XREAL_1:6;
A12: i <= len g by A2, A6, XXREAL_0:2;
then A13: j <= len g by A8, XXREAL_0:2;
i in dom g by A5, A12, FINSEQ_3:25;
then A18: g . i = (f ^ g) . (i + (len f)) by FINSEQ_1:def 7;
j in dom g by A7, A13, FINSEQ_3:25;
then g . j = (f ^ g) . (j + (len f)) by FINSEQ_1:def 7;
hence ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q ) by A4, A9, A10, A11, A18; :: thesis: verum
end;
end;