let F be Element of QC-WFF ; :: thesis: ( ( ((@ F) . 1) `1 = 0 implies F = VERUM ) & ( ((@ F) . 1) `1 = 1 implies F is negative ) & ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) & ( ((@ F) . 1) `1 = 3 implies F is universal ) & ( ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k implies F is atomic ) )
A1: now
per cases ( F is atomic or F = VERUM or F is negative or F is conjunctive or F is universal ) by Th33;
case F is atomic ; :: thesis: ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k
then consider k being Element of NAT , P being QC-pred_symbol of k, ll being QC-variable_list of k such that
A2: F = P ! ll by Def17;
@ F = <*P*> ^ ll by A2, Th23;
then (@ F) . 1 = P by FINSEQ_1:41;
hence ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k ; :: thesis: verum
end;
case F = VERUM ; :: thesis: ((@ F) . 1) `1 = 0
hence ((@ F) . 1) `1 = [0,0] `1 by FINSEQ_1:def 8
.= 0 by MCART_1:7 ;
:: thesis: verum
end;
case F is conjunctive ; :: thesis: ((@ F) . 1) `1 = 2
then consider p, q being Element of QC-WFF such that
A3: F = p '&' q by Def19;
@ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A3, FINSEQ_1:32;
then (@ F) . 1 = [2,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 2 by MCART_1:7; :: thesis: verum
end;
case F is universal ; :: thesis: ((@ F) . 1) `1 = 3
then consider x being bound_QC-variable, p being Element of QC-WFF such that
A4: F = All (x,p) by Def20;
@ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A4, FINSEQ_1:32;
then (@ F) . 1 = [3,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 3 by MCART_1:7; :: thesis: verum
end;
end;
end;
now
let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
let P be QC-pred_symbol of k; :: thesis: ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
reconsider P9 = P as QC-pred_symbol ;
P9 `1 = 7 + (the_arity_of P9) by Def6;
hence ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 ) by NAT_1:11; :: thesis: verum
end;
hence ( ( ((@ F) . 1) `1 = 0 implies F = VERUM ) & ( ((@ F) . 1) `1 = 1 implies F is negative ) & ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) & ( ((@ F) . 1) `1 = 3 implies F is universal ) & ( ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k implies F is atomic ) ) by A1; :: thesis: verum