let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A
for s being FinSequence st @ F = (@ G) ^ s holds
@ F = @ G
let F, G be Element of QC-WFF A; :: thesis: for s being FinSequence st @ F = (@ G) ^ s holds
@ F = @ G
let s be FinSequence; :: thesis: ( @ F = (@ G) ^ s implies @ F = @ G )
defpred S1[ set ] means for F, G being Element of QC-WFF A
for s being FinSequence st len (@ F) = $1 & @ F = (@ G) ^ s holds
@ F = @ G;
A1: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A2: for k being Nat st k < n holds
for F, G being Element of QC-WFF A
for s being FinSequence st len (@ F) = k & @ F = (@ G) ^ s holds
@ F = @ G ; :: thesis: S1[n]
let F, G be Element of QC-WFF A; :: thesis: for s being FinSequence st len (@ F) = n & @ F = (@ G) ^ s holds
@ F = @ G
let s be FinSequence; :: thesis: ( len (@ F) = n & @ F = (@ G) ^ s implies @ F = @ G )
assume that
A3: len (@ F) = n and
A4: @ F = (@ G) ^ s ; :: thesis: @ F = @ G
( dom (@ G) = Seg (len (@ G)) & 1 <= len (@ G) ) by Th10, FINSEQ_1:def 3;
then 1 in dom (@ G) ;
then A5: (@ F) . 1 = (@ G) . 1 by A4, FINSEQ_1:def 7;
A6: len ((@ G) ^ s) = (len (@ G)) + (len s) by FINSEQ_1:22;
now :: thesis: @ F = @ G
per cases ( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal ) by Th9;
suppose F is atomic ; :: thesis: @ F = @ G
then consider k being Nat, P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A10: F = P ! ll ;
A11: @ F = <*P*> ^ ll by A10, Th8;
then A12: (@ G) . 1 = P by A5, FINSEQ_1:41;
then G is atomic by Th12;
then consider k9 being Nat, P9 being QC-pred_symbol of k9,A, ll9 being QC-variable_list of k9,A such that
A13: G = P9 ! ll9 ;
A14: @ G = <*P9*> ^ ll9 by A13, Th8;
then A15: (@ G) . 1 = P9 by FINSEQ_1:41;
then <*P*> ^ ll = <*P*> ^ (ll9 ^ s) by A4, A11, A12, A14, FINSEQ_1:32;
then ll = ll9 ^ s by FINSEQ_1:33;
then A16: (len ll) + 0 = (len ll9) + (len s) by FINSEQ_1:22;
len ll9 = k9 by CARD_1:def 7
.= the_arity_of P by A12, A15, Th11
.= k by Th11
.= len ll by CARD_1:def 7 ;
then s = {} by A16;
hence @ F = @ G by A4, FINSEQ_1:34; :: thesis: verum
end;
suppose F is negative ; :: thesis: @ F = @ G
then consider p being Element of QC-WFF A such that
A17: F = 'not' p ;
(@ F) . 1 = [1,0] by A17, FINSEQ_1:41;
then ((@ G) . 1) `1 = 1 by A5;
then G is negative by Th12;
then consider p9 being Element of QC-WFF A such that
A18: G = 'not' p9 ;
<*[1,0]*> ^ (@ p) = <*[1,0]*> ^ ((@ p9) ^ s) by A4, A17, A18, FINSEQ_1:32;
then A19: @ p = (@ p9) ^ s by FINSEQ_1:33;
len (@ F) = (len (@ p)) + (len <*[1,0]*>) by A17, FINSEQ_1:22
.= (len (@ p)) + 1 by FINSEQ_1:40 ;
then len (@ p) < len (@ F) by NAT_1:13;
then @ p = @ p9 by A2, A3, A19;
then (@ p9) ^ {} = (@ p9) ^ s by A19, FINSEQ_1:34;
then s = {} by FINSEQ_1:33;
hence @ F = @ G by A4, FINSEQ_1:34; :: thesis: verum
end;
suppose F is conjunctive ; :: thesis: @ F = @ G
then consider p, q being Element of QC-WFF A such that
A20: F = p '&' q ;
A21: @ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A20, FINSEQ_1:32;
then A22: len (@ F) = (len ((@ p) ^ (@ q))) + (len <*[2,0]*>) by FINSEQ_1:22
.= (len ((@ p) ^ (@ q))) + 1 by FINSEQ_1:40 ;
then A23: len (@ F) = ((len (@ p)) + (len (@ q))) + 1 by FINSEQ_1:22;
(@ F) . 1 = [2,0] by A21, FINSEQ_1:41;
then ((@ G) . 1) `1 = 2 by A5;
then G is conjunctive by Th12;
then consider p9, q9 being Element of QC-WFF A such that
A24: G = p9 '&' q9 ;
A25: len (@ p9) <= (len (@ p9)) + (len ((@ q9) ^ s)) by NAT_1:11;
A26: @ G = <*[2,0]*> ^ ((@ p9) ^ (@ q9)) by A24, FINSEQ_1:32;
then <*[2,0]*> ^ ((@ p) ^ (@ q)) = <*[2,0]*> ^ (((@ p9) ^ (@ q9)) ^ s) by A4, A21, FINSEQ_1:32;
then A27: (@ p) ^ (@ q) = ((@ p9) ^ (@ q9)) ^ s by FINSEQ_1:33
.= (@ p9) ^ ((@ q9) ^ s) by FINSEQ_1:32 ;
then len (@ F) = ((len (@ p9)) + (len ((@ q9) ^ s))) + 1 by A22, FINSEQ_1:22;
then A28: len (@ p9) < len (@ F) by A25, NAT_1:13;
len (@ q) <= (len (@ p)) + (len (@ q)) by NAT_1:11;
then A29: len (@ q) < len (@ F) by A23, NAT_1:13;
len (@ p) <= (len (@ p)) + (len (@ q)) by NAT_1:11;
then A30: len (@ p) < len (@ F) by A23, NAT_1:13;
( len (@ p) <= len (@ p9) or len (@ p9) <= len (@ p) ) ;
then consider a, b, c, d being FinSequence such that
A31: ( ( a = @ p & b = @ p9 ) or ( a = @ p9 & b = @ p ) ) and
A32: ( len a <= len b & a ^ c = b ^ d ) by A27;
ex t being FinSequence st a ^ t = b by A32, FINSEQ_1:47;
then A33: @ p = @ p9 by A2, A3, A31, A30, A28;
then @ q = (@ q9) ^ s by A27, FINSEQ_1:33;
hence @ F = @ G by A2, A3, A21, A26, A33, A29; :: thesis: verum
end;
suppose F is universal ; :: thesis: @ F = @ G
then consider x being bound_QC-variable of A, p being Element of QC-WFF A such that
A34: F = All (x,p) ;
A35: @ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A34, FINSEQ_1:32;
then len (@ F) = (len (<*x*> ^ (@ p))) + (len <*[3,0]*>) by FINSEQ_1:22
.= (len (<*x*> ^ (@ p))) + 1 by FINSEQ_1:40
.= ((len <*x*>) + (len (@ p))) + 1 by FINSEQ_1:22
.= (1 + (len (@ p))) + 1 by FINSEQ_1:40 ;
then (len (@ p)) + 1 <= len (@ F) by NAT_1:13;
then A36: len (@ p) < len (@ F) by NAT_1:13;
(@ F) . 1 = [3,0] by A35, FINSEQ_1:41;
then ((@ G) . 1) `1 = 3 by A5;
then G is universal by Th12;
then consider x9 being bound_QC-variable of A, p9 being Element of QC-WFF A such that
A37: G = All (x9,p9) ;
(<*[3,0]*> ^ <*x*>) ^ (@ p) = (<*[3,0]*> ^ (<*x9*> ^ (@ p9))) ^ s by A4, A34, A37, FINSEQ_1:32
.= <*[3,0]*> ^ ((<*x9*> ^ (@ p9)) ^ s) by FINSEQ_1:32 ;
then A38: <*x*> ^ (@ p) = (<*x9*> ^ (@ p9)) ^ s by A34, A35, FINSEQ_1:33
.= <*x9*> ^ ((@ p9) ^ s) by FINSEQ_1:32 ;
then A39: x = (<*x9*> ^ ((@ p9) ^ s)) . 1 by FINSEQ_1:41
.= x9 by FINSEQ_1:41 ;
then @ p = (@ p9) ^ s by A38, FINSEQ_1:33;
hence @ F = @ G by A2, A3, A34, A37, A39, A36; :: thesis: verum
end;
end;
end;
hence @ F = @ G ; :: thesis: verum
end;
A40: for n being Nat holds S1[n] from NAT_1:sch 4(A1);
 thus ( @ F = (@ G) ^ s implies @ F = @ G ) by A40; :: thesis: verum