let Al be QC-alphabet ; :: thesis: for n being Nat

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

let n be Nat; :: thesis: for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

let X be Subset of (CQC-WFF Al); :: thesis: for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

let f, g be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len f implies ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X ) )

assume that

A1: 1 <= n and

A2: n <= len f ; :: thesis: ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

n in Seg (len f) by A1, A2, FINSEQ_1:1;

then n in dom f by FINSEQ_1:def 3;

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 X implies f ^ g,n is_a_correct_step_wrt X ) :: thesis: ( f ^ g,n is_a_correct_step_wrt X implies f,n is_a_correct_step_wrt X )

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 by A1, A2, Th19;

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

let n be Nat; :: thesis: for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

let X be Subset of (CQC-WFF Al); :: thesis: for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

let f, g be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len f implies ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X ) )

assume that

A1: 1 <= n and

A2: n <= len f ; :: thesis: ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

n in Seg (len f) by A1, A2, FINSEQ_1:1;

then n in dom f by FINSEQ_1:def 3;

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 X implies f ^ g,n is_a_correct_step_wrt X ) :: thesis: ( f ^ g,n is_a_correct_step_wrt X implies f,n is_a_correct_step_wrt X )

proof

assume A24:
f ^ g,n is_a_correct_step_wrt X
; :: thesis: f,n is_a_correct_step_wrt X
assume A5:
f,n is_a_correct_step_wrt X
; :: thesis: f ^ g,n is_a_correct_step_wrt X

not not ((f ^ g) . n) `2 = 0 & ... & not ((f ^ g) . n) `2 = 9 by A1, A4, Th19;

end;not not ((f ^ g) . n) `2 = 0 & ... & not ((f ^ g) . n) `2 = 9 by A1, A4, Th19;

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 )
;

:: according to CQC_THE1:def 4end;

:: according to CQC_THE1:def 4

case
((f ^ g) . n) `2 = 2
; :: thesis: ex p being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (('not' p) => p) => p

hence
ex p being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (('not' p) => p) => p
by A3, A5, Def4; :: thesis: verum

end;case
((f ^ g) . n) `2 = 3
; :: thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = p => (('not' p) => q)

hence
ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = p => (('not' p) => q)
by A3, A5, Def4; :: thesis: verum

end;case
((f ^ g) . n) `2 = 4
; :: thesis: ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))

hence
ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
by A3, A5, Def4; :: thesis: verum

end;case
((f ^ g) . n) `2 = 5
; :: thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p '&' q) => (q '&' p)

hence
ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p '&' q) => (q '&' p)
by A3, A5, Def4; :: thesis: verum

end;case
((f ^ g) . n) `2 = 6
; :: thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . n) `1 = (All (x,p)) => p

hence
ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . n) `1 = (All (x,p)) => p
by A3, A5, Def4; :: thesis: verum

end;case
((f ^ g) . n) `2 = 7
; :: thesis: ex i, j being Nat ex p, q being Element of CQC-WFF Al 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 )

( 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 CQC-WFF Al 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, Def4;

A11: i <= len f by A2, A7, XXREAL_0:2;

then A12: j <= len f by A9, XXREAL_0:2;

A13: i in Seg (len f) by A6, A11, FINSEQ_1:1;

A14: j in Seg (len f) by A8, A12, FINSEQ_1:1;

A15: i in dom f by A13, FINSEQ_1:def 3;

A16: j in dom f by A14, FINSEQ_1:def 3;

A17: f . i = (f ^ g) . i by A15, 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 CQC-WFF Al 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;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, Def4;

A11: i <= len f by A2, A7, XXREAL_0:2;

then A12: j <= len f by A9, XXREAL_0:2;

A13: i in Seg (len f) by A6, A11, FINSEQ_1:1;

A14: j in Seg (len f) by A8, A12, FINSEQ_1:1;

A15: i in dom f by A13, FINSEQ_1:def 3;

A16: j in dom f by A14, FINSEQ_1:def 3;

A17: f . i = (f ^ g) . i by A15, 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 CQC-WFF Al 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

case
((f ^ g) . n) `2 = 8
; :: thesis: ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All (x,q)) )

( 1 <= i & i < n & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All (x,q)) )

then consider i being Nat, r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that

A18: 1 <= i and

A19: i < n and

A20: ( (f . i) `1 = r => t & not x in still_not-bound_in r & (f . n) `1 = r => (All (x,t)) ) by A3, A5, Def4;

i <= len f by A2, A19, XXREAL_0:2;

then i in Seg (len f) by A18, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All (x,q)) ) by A3, A18, A19, A20; :: thesis: verum

end;A18: 1 <= i and

A19: i < n and

A20: ( (f . i) `1 = r => t & not x in still_not-bound_in r & (f . n) `1 = r => (All (x,t)) ) by A3, A5, Def4;

i <= len f by A2, A19, XXREAL_0:2;

then i in Seg (len f) by A18, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All (x,q)) ) by A3, A18, A19, A20; :: thesis: verum

case
((f ^ g) . n) `2 = 9
; :: thesis: ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . n) `1 )

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . n) `1 )

then consider i being Nat, x, y being bound_QC-variable of Al, s being QC-formula of Al such that

A21: 1 <= i and

A22: i < n and

A23: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . n) `1 = s . y ) by A3, A5, Def4;

i <= len f by A2, A22, XXREAL_0:2;

then i in Seg (len f) by A21, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . n) `1 ) by A3, A21, A22, A23; :: thesis: verum

end;A21: 1 <= i and

A22: i < n and

A23: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . n) `1 = s . y ) by A3, A5, Def4;

i <= len f by A2, A22, XXREAL_0:2;

then i in Seg (len f) by A21, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . n) `1 ) by A3, A21, A22, A23; :: thesis: verum

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 by A1, A2, Th19;

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 )
;

:: according to CQC_THE1:def 4end;

:: according to CQC_THE1:def 4

case
(f . n) `2 = 2
; :: thesis: ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p

hence
ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p
by A3, A24, Def4; :: thesis: verum

end;case
(f . n) `2 = 3
; :: thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q)

hence
ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q)
by A3, A24, Def4; :: thesis: verum

end;case
(f . n) `2 = 4
; :: thesis: ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))

hence
ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
by A3, A24, Def4; :: thesis: verum

end;case
(f . n) `2 = 5
; :: thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p)

hence
ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p)
by A3, A24, Def4; :: thesis: verum

end;case
(f . n) `2 = 6
; :: thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p

hence
ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p
by A3, A24, Def4; :: thesis: verum

end;case
(f . n) `2 = 7
; :: thesis: ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q )

( 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 CQC-WFF Al 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, Def4;

A30: i <= len f by A2, A26, XXREAL_0:2;

then A31: j <= len f by A28, XXREAL_0:2;

A32: i in Seg (len f) by A25, A30, FINSEQ_1:1;

A33: j in Seg (len f) by A27, A31, FINSEQ_1:1;

A34: i in dom f by A32, FINSEQ_1:def 3;

A35: j in dom f by A33, FINSEQ_1:def 3;

A36: f . i = (f ^ g) . i by A34, FINSEQ_1:def 7;

f . j = (f ^ g) . j by A35, FINSEQ_1:def 7;

hence ex i, j being Nat ex p, q being Element of CQC-WFF Al 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;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, Def4;

A30: i <= len f by A2, A26, XXREAL_0:2;

then A31: j <= len f by A28, XXREAL_0:2;

A32: i in Seg (len f) by A25, A30, FINSEQ_1:1;

A33: j in Seg (len f) by A27, A31, FINSEQ_1:1;

A34: i in dom f by A32, FINSEQ_1:def 3;

A35: j in dom f by A33, FINSEQ_1:def 3;

A36: f . i = (f ^ g) . i by A34, FINSEQ_1:def 7;

f . j = (f ^ g) . j by A35, FINSEQ_1:def 7;

hence ex i, j being Nat ex p, q being Element of CQC-WFF Al 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

case
(f . n) `2 = 8
; :: thesis: ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) )

( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) )

then consider i being Nat, r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that

A37: 1 <= i and

A38: i < n and

A39: ( ((f ^ g) . i) `1 = r => t & not x in still_not-bound_in r & ((f ^ g) . n) `1 = r => (All (x,t)) ) by A3, A24, Def4;

i <= len f by A2, A38, XXREAL_0:2;

then i in Seg (len f) by A37, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A3, A37, A38, A39; :: thesis: verum

end;A37: 1 <= i and

A38: i < n and

A39: ( ((f ^ g) . i) `1 = r => t & not x in still_not-bound_in r & ((f ^ g) . n) `1 = r => (All (x,t)) ) by A3, A24, Def4;

i <= len f by A2, A38, XXREAL_0:2;

then i in Seg (len f) by A37, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A3, A37, A38, A39; :: thesis: verum

case
(f . n) `2 = 9
; :: thesis: ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 )

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 )

then consider i being Nat, x, y being bound_QC-variable of Al, s being QC-formula of Al such that

A40: 1 <= i and

A41: i < n and

A42: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & ((f ^ g) . n) `1 = s . y ) by A3, A24, Def4;

i <= len f by A2, A41, XXREAL_0:2;

then i in Seg (len f) by A40, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A3, A40, A41, A42; :: thesis: verum

end;A40: 1 <= i and

A41: i < n and

A42: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & ((f ^ g) . n) `1 = s . y ) by A3, A24, Def4;

i <= len f by A2, A41, XXREAL_0:2;

then i in Seg (len f) by A40, FINSEQ_1:1;

then i in dom f by FINSEQ_1:def 3;

then f . i = (f ^ g) . i by FINSEQ_1:def 7;

hence ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A3, A40, A41, A42; :: thesis: verum