let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
let S be Element of QC-Sub-WFF A; :: thesis: ( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
thus ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) :: thesis: ( ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proof
assume S is A -Sub_VERUM ; :: thesis: ((@ (S `1)) . 1) `1 = 0
then ex e being Element of vSUB A st S = [(VERUM A),e] ;
then S `1 = VERUM A ;
hence ((@ (S `1)) . 1) `1 = [0,0] `1 by FINSEQ_1:def 8
.= 0 ;
:: thesis: verum
end;
thus ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) :: thesis: ( ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proof
assume S is Sub_atomic ; :: thesis: ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A
then consider k being Nat, P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that
A1: S = Sub_P (P,ll,e) ;
S = [(P ! ll),e] by A1, Th9;
then S `1 = P ! ll ;
then @ (S `1) = <*P*> ^ ll by QC_LANG1:8;
then (@ (S `1)) . 1 = P by FINSEQ_1:41;
hence ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ; :: thesis: verum
end;
thus ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) :: thesis: ( ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proof
assume S is Sub_negative ; :: thesis: ((@ (S `1)) . 1) `1 = 1
then consider S9 being Element of QC-Sub-WFF A such that
A2: S = Sub_not S9 ;
S `1 = 'not' (S9 `1) by A2;
then (@ (S `1)) . 1 = [1,0] by FINSEQ_1:41;
hence ((@ (S `1)) . 1) `1 = 1 ; :: thesis: verum
end;
thus ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) :: thesis: ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 )
proof
assume S is Sub_conjunctive ; :: thesis: ((@ (S `1)) . 1) `1 = 2
then consider S1, S2 being Element of QC-Sub-WFF A such that
A3: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) ;
S = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A3, Def21;
then S `1 = (S1 `1) '&' (S2 `1) ;
then @ (S `1) = <*[2,0]*> ^ ((@ (S1 `1)) ^ (@ (S2 `1))) by FINSEQ_1:32;
then (@ (S `1)) . 1 = [2,0] by FINSEQ_1:41;
hence ((@ (S `1)) . 1) `1 = 2 ; :: thesis: verum
end;
thus ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) :: thesis: verum
proof
assume S is Sub_universal ; :: thesis: ((@ (S `1)) . 1) `1 = 3
then consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that
A4: ( S = Sub_All (B,SQ) & B is quantifiable ) ;
S = [(All ((B `2),((B `1) `1))),SQ] by A4, Def24;
then S `1 = All ((B `2),((B `1) `1)) ;
then @ (S `1) = <*[3,0]*> ^ (<*(B `2)*> ^ (@ ((B `1) `1))) by FINSEQ_1:32;
then (@ (S `1)) . 1 = [3,0] by FINSEQ_1:41;
hence ((@ (S `1)) . 1) `1 = 3 ; :: thesis: verum
end;