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 f holds
( f,n is_a_correct_step_wrt_IPC X iff f ^ g,n 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 f holds
( f,n is_a_correct_step_wrt_IPC X iff f ^ g,n is_a_correct_step_wrt_IPC X )
let f, g be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: ( 1 <= n & n <= len f implies ( f,n is_a_correct_step_wrt_IPC X iff f ^ g,n is_a_correct_step_wrt_IPC X ) )
assume that
A1: 1 <= n and
A2: n <= len f ; :: thesis: ( f,n is_a_correct_step_wrt_IPC X iff f ^ g,n is_a_correct_step_wrt_IPC X )
n in dom f by A1, A2, FINSEQ_3:25;
then A3: (f ^ g) . n = f . n by FINSEQ_1:def 7;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then len f <= len (f ^ g) by NAT_1:11;
then A4: n <= len (f ^ g) by A2, XXREAL_0:2;
thus ( f,n is_a_correct_step_wrt_IPC X implies f ^ g,n is_a_correct_step_wrt_IPC X ) :: thesis: ( f ^ g,n is_a_correct_step_wrt_IPC X implies f,n is_a_correct_step_wrt_IPC X )
proof
assume A5: f,n is_a_correct_step_wrt_IPC X ; :: thesis: f ^ g,n is_a_correct_step_wrt_IPC X
not not ((f ^ g) . n) `2 = 0 & ... & not ((f ^ g) . n) `2 = 10 by A1, A4, Th3;
per cases then ( ((f ^ g) . n) `2 = 0 or ((f ^ g) . n) `2 = 1 or ((f ^ g) . n) `2 = 2 or ((f ^ g) . n) `2 = 3 or ((f ^ g) . n) `2 = 4 or ((f ^ g) . n) `2 = 5 or ((f ^ g) . n) `2 = 6 or ((f ^ g) . n) `2 = 7 or ((f ^ g) . n) `2 = 8 or ((f ^ g) . n) `2 = 9 or ((f ^ g) . n) `2 = 10 ) ;
:: according to INTPRO_2:def 3
case ((f ^ g) . n) `2 = 0 ; :: thesis: ((f ^ g) . n) `1 in X
hence ((f ^ g) . n) `1 in X by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 1 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = p => (q => p)
hence ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = p => (q => p) by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 2 ; :: thesis: ex p, q, r being Element of MC-wff st ((f ^ g) . n) `1 = (p => (q => r)) => ((p => q) => (p => r))
hence ex p, q, r being Element of MC-wff st ((f ^ g) . n) `1 = (p => (q => r)) => ((p => q) => (p => r)) by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 3 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = (p '&' q) => p
hence ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = (p '&' q) => p by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 4 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = (p '&' q) => q
hence ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = (p '&' q) => q by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 5 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = p => (q => (p '&' q))
hence ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = p => (q => (p '&' q)) by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 6 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = p => (p 'or' q)
hence ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = p => (p 'or' q) by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 7 ; :: thesis: ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = q => (p 'or' q)
hence ex p, q being Element of MC-wff st ((f ^ g) . n) `1 = q => (p 'or' q) by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 8 ; :: thesis: ex p, q, r being Element of MC-wff st ((f ^ g) . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r))
hence ex p, q, r being Element of MC-wff st ((f ^ g) . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r)) by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 9 ; :: thesis: ex p being Element of MC-wff st ((f ^ g) . n) `1 = FALSUM => p
hence ex p being Element of MC-wff st ((f ^ g) . n) `1 = FALSUM => p by A3, A5, Def3; :: thesis: verum
end;
case ((f ^ g) . n) `2 = 10 ; :: thesis: ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = p => q )
then consider i, j being Nat, r, t being Element of MC-wff such that
A6: 1 <= i and
A7: i < n and
A8: 1 <= j and
A9: j < i and
A10: ( r = (f . j) `1 & t = (f . n) `1 & (f . i) `1 = r => t ) by A3, A5, Def3;
A11: i <= len f by A2, A7, XXREAL_0:2;
then j <= len f by A9, XXREAL_0:2;
then A16: j in dom f by FINSEQ_3:25, A8;
i in dom f by A6, A11, FINSEQ_3:25;
then A17: f . i = (f ^ g) . i by FINSEQ_1:def 7;
f . j = (f ^ g) . j by A16, FINSEQ_1:def 7;
hence ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = p => q ) by A3, A6, A7, A8, A9, A10, A17; :: thesis: verum
end;
end;
end;
assume A24: f ^ g,n is_a_correct_step_wrt_IPC X ; :: thesis: f,n is_a_correct_step_wrt_IPC X
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10 by A1, A2, Th3;
per cases then ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 or (f . n) `2 = 10 ) ;
:: according to INTPRO_2:def 3
case (f . n) `2 = 0 ; :: thesis: (f . n) `1 in X
hence (f . n) `1 in X by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 1 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = p => (q => p)
hence ex p, q being Element of MC-wff st (f . n) `1 = p => (q => p) by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 2 ; :: thesis: ex p, q, r being Element of MC-wff st (f . n) `1 = (p => (q => r)) => ((p => q) => (p => r))
hence ex p, q, r being Element of MC-wff st (f . n) `1 = (p => (q => r)) => ((p => q) => (p => r)) by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 3 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => p
hence ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => p by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 4 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => q
hence ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => q by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 5 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = p => (q => (p '&' q))
hence ex p, q being Element of MC-wff st (f . n) `1 = p => (q => (p '&' q)) by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 6 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = p => (p 'or' q)
hence ex p, q being Element of MC-wff st (f . n) `1 = p => (p 'or' q) by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 7 ; :: thesis: ex p, q being Element of MC-wff st (f . n) `1 = q => (p 'or' q)
hence ex p, q being Element of MC-wff st (f . n) `1 = q => (p 'or' q) by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 8 ; :: thesis: ex p, q, r being Element of MC-wff st (f . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r))
hence ex p, q, r being Element of MC-wff st (f . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r)) by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 9 ; :: thesis: ex p being Element of MC-wff st (f . n) `1 = FALSUM => p
hence ex p being Element of MC-wff st (f . n) `1 = FALSUM => p by A3, A24, Def3; :: thesis: verum
end;
case (f . n) `2 = 10 ; :: thesis: ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q )
then consider i, j being Nat, r, t being Element of MC-wff such that
A25: 1 <= i and
A26: i < n and
A27: 1 <= j and
A28: j < i and
A29: ( r = ((f ^ g) . j) `1 & t = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = r => t ) by A3, A24, Def3;
A30: i <= len f by A2, A26, XXREAL_0:2;
then A31: j <= len f by A28, XXREAL_0:2;
i in dom f by A25, A30, FINSEQ_3:25;
then A36: f . i = (f ^ g) . i by FINSEQ_1:def 7;
j in dom f by A27, A31, FINSEQ_3:25;
then f . j = (f ^ g) . j by FINSEQ_1:def 7;
hence ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A3, A25, A26, A27, A28, A29, A36; :: thesis: verum
end;
end;