let F, G be Element of QC-WFF ; :: 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
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
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 ; :: 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 Th34, 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:35;
now
per cases ( F = VERUM or F is atomic or F is negative or F is conjunctive or F is universal ) by Th33;
suppose F is atomic ; :: thesis: @ F = @ G
then consider k being Element of NAT , P being QC-pred_symbol of k, ll being QC-variable_list of k such that
A10: F = P ! ll by Def17;
A11: @ F = <*P*> ^ ll by A10, Th23;
then A12: (@ G) . 1 = P by A5, FINSEQ_1:58;
then G is atomic by Th36;
then consider k9 being Element of NAT , P9 being QC-pred_symbol of k9, ll9 being QC-variable_list of k9 such that
A13: G = P9 ! ll9 by Def17;
A14: @ G = <*P9*> ^ ll9 by A13, Th23;
then A15: (@ G) . 1 = P9 by FINSEQ_1:58;
then <*P*> ^ ll = <*P*> ^ (ll9 ^ s) by A4, A11, A12, A14, FINSEQ_1:45;
then ll = ll9 ^ s by FINSEQ_1:46;
then A16: (len ll) + 0 = (len ll9) + (len s) by FINSEQ_1:35;
len ll9 = k9 by FINSEQ_1:def 18
.= the_arity_of P by A12, A15, Th35
.= k by Th35
.= len ll by FINSEQ_1:def 18 ;
then s = {} by A16;
hence @ F = @ G by A4, FINSEQ_1:47; :: thesis: verum
end;
suppose F is negative ; :: thesis: @ F = @ G
then consider p being Element of QC-WFF such that
A17: F = 'not' p by Def18;
(@ F) . 1 = [1,0 ] by A17, FINSEQ_1:58;
then ((@ G) . 1) `1 = 1 by A5, MCART_1:7;
then G is negative by Th36;
then consider p9 being Element of QC-WFF such that
A18: G = 'not' p9 by Def18;
<*[1,0 ]*> ^ (@ p) = <*[1,0 ]*> ^ ((@ p9) ^ s) by A4, A17, A18, FINSEQ_1:45;
then A19: @ p = (@ p9) ^ s by FINSEQ_1:46;
len (@ F) = (len (@ p)) + (len <*[1,0 ]*>) by A17, FINSEQ_1:35
.= (len (@ p)) + 1 by FINSEQ_1:57 ;
then len (@ p) < len (@ F) by NAT_1:13;
then @ p = @ p9 by A2, A3, A19;
then (@ p9) ^ {} = (@ p9) ^ s by A19, FINSEQ_1:47;
then s = {} by FINSEQ_1:46;
hence @ F = @ G by A4, FINSEQ_1:47; :: thesis: verum
end;
suppose F is conjunctive ; :: thesis: @ F = @ G
then consider p, q being Element of QC-WFF such that
A20: F = p '&' q by Def19;
A21: @ F = <*[2,0 ]*> ^ ((@ p) ^ (@ q)) by A20, FINSEQ_1:45;
then A22: len (@ F) = (len ((@ p) ^ (@ q))) + (len <*[2,0 ]*>) by FINSEQ_1:35
.= (len ((@ p) ^ (@ q))) + 1 by FINSEQ_1:57 ;
then A23: len (@ F) = ((len (@ p)) + (len (@ q))) + 1 by FINSEQ_1:35;
(@ F) . 1 = [2,0 ] by A21, FINSEQ_1:58;
then ((@ G) . 1) `1 = 2 by A5, MCART_1:7;
then G is conjunctive by Th36;
then consider p9, q9 being Element of QC-WFF such that
A24: G = p9 '&' q9 by Def19;
A25: len (@ p9) <= (len (@ p9)) + (len ((@ q9) ^ s)) by NAT_1:11;
A26: @ G = <*[2,0 ]*> ^ ((@ p9) ^ (@ q9)) by A24, FINSEQ_1:45;
then <*[2,0 ]*> ^ ((@ p) ^ (@ q)) = <*[2,0 ]*> ^ (((@ p9) ^ (@ q9)) ^ s) by A4, A21, FINSEQ_1:45;
then A27: (@ p) ^ (@ q) = ((@ p9) ^ (@ q9)) ^ s by FINSEQ_1:46
.= (@ p9) ^ ((@ q9) ^ s) by FINSEQ_1:45 ;
then len (@ F) = ((len (@ p9)) + (len ((@ q9) ^ s))) + 1 by A22, FINSEQ_1:35;
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:64;
then A33: @ p = @ p9 by A2, A3, A31, A30, A28;
then @ q = (@ q9) ^ s by A27, FINSEQ_1:46;
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, p being Element of QC-WFF such that
A34: F = All x,p by Def20;
A35: @ F = <*[3,0 ]*> ^ (<*x*> ^ (@ p)) by A34, FINSEQ_1:45;
then len (@ F) = (len (<*x*> ^ (@ p))) + (len <*[3,0 ]*>) by FINSEQ_1:35
.= (len (<*x*> ^ (@ p))) + 1 by FINSEQ_1:57
.= ((len <*x*>) + (len (@ p))) + 1 by FINSEQ_1:35
.= (1 + (len (@ p))) + 1 by FINSEQ_1:57 ;
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:58;
then ((@ G) . 1) `1 = 3 by A5, MCART_1:7;
then G is universal by Th36;
then consider x9 being bound_QC-variable, p9 being Element of QC-WFF such that
A37: G = All x9,p9 by Def20;
(<*[3,0 ]*> ^ <*x*>) ^ (@ p) = (<*[3,0 ]*> ^ (<*x9*> ^ (@ p9))) ^ s by A4, A34, A37, FINSEQ_1:45
.= <*[3,0 ]*> ^ ((<*x9*> ^ (@ p9)) ^ s) by FINSEQ_1:45 ;
then A38: <*x*> ^ (@ p) = (<*x9*> ^ (@ p9)) ^ s by A34, A35, FINSEQ_1:46
.= <*x9*> ^ ((@ p9) ^ s) by FINSEQ_1:45 ;
then A39: x = (<*x9*> ^ ((@ p9) ^ s)) . 1 by FINSEQ_1:58
.= x9 by FINSEQ_1:58 ;
then @ p = (@ p9) ^ s by A38, FINSEQ_1:46;
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);
 len (@ F) = len (@ F) ;
hence ( @ F = (@ G) ^ s implies @ F = @ G ) by A40; :: thesis: verum