:: Connectives and Subformulae of the First Order Language
:: by Grzegorz Bancerek
::
:: Received November 23, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: QC_LANG2:1
for A being QC-alphabet
for p being Element of QC-WFF A holds the_argument_of ('not' p) = p
proofend;

theorem Th2: :: QC_LANG2:2
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p '&' q = p1 '&' q1 holds
( p = p1 & q = q1 )
proofend;

theorem Th3: :: QC_LANG2:3
for A being QC-alphabet
for p being Element of QC-WFF A st p is conjunctive holds
p = (the_left_argument_of p) '&' (the_right_argument_of p)
proofend;

theorem Th4: :: QC_LANG2:4
for A being QC-alphabet
for p, q being Element of QC-WFF A holds
( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
proofend;

theorem Th5: :: QC_LANG2:5
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st All (x,p) = All (y,q) holds
( x = y & p = q )
proofend;

theorem Th6: :: QC_LANG2:6
for A being QC-alphabet
for p being Element of QC-WFF A st p is universal holds
p = All ((bound_in p),(the_scope_of p))
proofend;

theorem Th7: :: QC_LANG2:7
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds
( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )
proofend;

definition
let A be QC-alphabet ;
func FALSUM A ->  QC-formula of A equals :: QC_LANG2:def 1
 'not' (VERUM A);
correctness
coherence
'not' (VERUM A) is QC-formula of A;
;
let p, q be Element of QC-WFF A;
funcp => q ->  QC-formula of A equals :: QC_LANG2:def 2
 'not' (p '&' ('not' q));
correctness
coherence
'not' (p '&' ('not' q)) is QC-formula of A;
;
funcp 'or' q ->  QC-formula of A equals :: QC_LANG2:def 3
 'not' (('not' p) '&' ('not' q));
correctness
coherence
'not' (('not' p) '&' ('not' q)) is QC-formula of A;
;
end;

:: deftheorem  defines FALSUM QC_LANG2:def_1_:_
 for A being QC-alphabet holds FALSUM A = 'not' (VERUM A);

:: deftheorem  defines => QC_LANG2:def_2_:_
 for A being QC-alphabet
for p, q being Element of QC-WFF A holds p => q = 'not' (p '&' ('not' q));

:: deftheorem  defines 'or' QC_LANG2:def_3_:_
 for A being QC-alphabet
for p, q being Element of QC-WFF A holds p 'or' q = 'not' (('not' p) '&' ('not' q));

definition
let A be QC-alphabet ;
let p, q be Element of QC-WFF A;
funcp <=> q ->  QC-formula of A equals :: QC_LANG2:def 4
(p => q) '&amp;' (q => p);
correctness
coherence
(p => q) '&amp;' (q => p) is QC-formula of A;
;
end;

:: deftheorem  defines <=> QC_LANG2:def_4_:_
 for A being QC-alphabet
for p, q being Element of QC-WFF A holds p <=> q = (p => q) '&amp;' (q => p);

definition
let A be QC-alphabet ;
let x be bound_QC-variable of A;
let p be Element of QC-WFF A;
func Ex (x,p) ->  QC-formula of A equals :: QC_LANG2:def 5
 'not' (All (x,('not' p)));
correctness
coherence
'not' (All (x,('not' p))) is QC-formula of A;
;
end;

:: deftheorem  defines Ex QC_LANG2:def_5_:_
 for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Ex (x,p) = 'not' (All (x,('not' p)));

theorem :: QC_LANG2:8
for A being QC-alphabet holds
( FALSUM A is negative &amp; the_argument_of (FALSUM A) = VERUM A ) by Th1, QC_LANG1:def_19;

theorem :: QC_LANG2:9
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p 'or' q = ('not' p) => q ;

theorem :: QC_LANG2:10
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p 'or' q = p1 'or' q1 holds
( p = p1 &amp; q = q1 )
proofend;

theorem Th11: :: QC_LANG2:11
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p => q = p1 => q1 holds
( p = p1 &amp; q = q1 )
proofend;

theorem :: QC_LANG2:12
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p <=> q = p1 <=> q1 holds
( p = p1 &amp; q = q1 )
proofend;

theorem Th13: :: QC_LANG2:13
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st Ex (x,p) = Ex (y,q) holds
( x = y &amp; p = q )
proofend;

definition
let A be QC-alphabet ;
let x, y be bound_QC-variable of A;
let p be Element of QC-WFF A;
func All (x,y,p) ->  QC-formula of A equals :: QC_LANG2:def 6
 All (x,(All (y,p)));
correctness
coherence
All (x,(All (y,p))) is QC-formula of A;
;
func Ex (x,y,p) ->  QC-formula of A equals :: QC_LANG2:def 7
 Ex (x,(Ex (y,p)));
correctness
coherence
Ex (x,(Ex (y,p))) is QC-formula of A;
;
end;

:: deftheorem  defines All QC_LANG2:def_6_:_
 for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds All (x,y,p) = All (x,(All (y,p)));

:: deftheorem  defines Ex QC_LANG2:def_7_:_
 for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds Ex (x,y,p) = Ex (x,(Ex (y,p)));

theorem :: QC_LANG2:14
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,y,p) = All (x,(All (y,p))) &amp; Ex (x,y,p) = Ex (x,(Ex (y,p))) ) ;

theorem Th15: :: QC_LANG2:15
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2 being bound_QC-variable of A st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; p1 = p2 )
proofend;

theorem :: QC_LANG2:16
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A st All (x,y,p) = All (z,q) holds
( x = z &amp; All (y,p) = q ) by Th5;

theorem Th17: :: QC_LANG2:17
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2 being bound_QC-variable of A st Ex (x1,y1,p1) = Ex (x2,y2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; p1 = p2 )
proofend;

theorem :: QC_LANG2:18
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A st Ex (x,y,p) = Ex (z,q) holds
( x = z &amp; Ex (y,p) = q ) by Th13;

theorem :: QC_LANG2:19
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,y,p) is universal &amp; bound_in (All (x,y,p)) = x &amp; the_scope_of (All (x,y,p)) = All (y,p) ) by Th7, QC_LANG1:def_21;

definition
let A be QC-alphabet ;
let x, y, z be bound_QC-variable of A;
let p be Element of QC-WFF A;
func All (x,y,z,p) ->  QC-formula of A equals :: QC_LANG2:def 8
 All (x,(All (y,z,p)));
correctness
coherence
All (x,(All (y,z,p))) is QC-formula of A;
;
func Ex (x,y,z,p) ->  QC-formula of A equals :: QC_LANG2:def 9
 Ex (x,(Ex (y,z,p)));
correctness
coherence
Ex (x,(Ex (y,z,p))) is QC-formula of A;
;
end;

:: deftheorem  defines All QC_LANG2:def_8_:_
 for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds All (x,y,z,p) = All (x,(All (y,z,p)));

:: deftheorem  defines Ex QC_LANG2:def_9_:_
 for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds Ex (x,y,z,p) = Ex (x,(Ex (y,z,p)));

theorem :: QC_LANG2:20
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,y,z,p) = All (x,(All (y,z,p))) &amp; Ex (x,y,z,p) = Ex (x,(Ex (y,z,p))) ) ;

theorem :: QC_LANG2:21
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st All (x1,y1,z1,p1) = All (x2,y2,z2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; z1 = z2 &amp; p1 = p2 )
proofend;

theorem :: QC_LANG2:22
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t being bound_QC-variable of A st All (x,y,z,p) = All (t,q) holds
( x = t &amp; All (y,z,p) = q ) by Th5;

theorem :: QC_LANG2:23
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st All (x,y,z,p) = All (t,s,q) holds
( x = t &amp; y = s &amp; All (z,p) = q )
proofend;

theorem :: QC_LANG2:24
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; z1 = z2 &amp; p1 = p2 )
proofend;

theorem :: QC_LANG2:25
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,q) holds
( x = t &amp; Ex (y,z,p) = q ) by Th13;

theorem :: QC_LANG2:26
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t &amp; y = s &amp; Ex (z,p) = q )
proofend;

theorem :: QC_LANG2:27
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,y,z,p) is universal &amp; bound_in (All (x,y,z,p)) = x &amp; the_scope_of (All (x,y,z,p)) = All (y,z,p) ) by Th7, QC_LANG1:def_21;

definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
attrH is disjunctive  means :: QC_LANG2:def 10
 ex p, q being Element of QC-WFF A st H = p 'or' q;
attrH is conditional  means :Def11: :: QC_LANG2:def 11
 ex p, q being Element of QC-WFF A st H = p => q;
attrH is biconditional  means :: QC_LANG2:def 12
 ex p, q being Element of QC-WFF A st H = p <=> q;
attrH is existential  means :Def13: :: QC_LANG2:def 13
 ex x being bound_QC-variable of A ex p being Element of QC-WFF A st H = Ex (x,p);
end;

:: deftheorem  defines disjunctive QC_LANG2:def_10_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is disjunctive iff ex p, q being Element of QC-WFF A st H = p 'or' q );

:: deftheorem Def11 defines conditional QC_LANG2:def_11_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is conditional iff ex p, q being Element of QC-WFF A st H = p => q );

:: deftheorem  defines biconditional QC_LANG2:def_12_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is biconditional iff ex p, q being Element of QC-WFF A st H = p <=> q );

:: deftheorem Def13 defines existential QC_LANG2:def_13_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is existential iff ex x being bound_QC-variable of A ex p being Element of QC-WFF A st H = Ex (x,p) );

theorem :: QC_LANG2:28
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds
( Ex (x,y,p) is existential &amp; Ex (x,y,z,p) is existential ) by Def13;

definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
func the_left_disjunct_of H ->  QC-formula of A equals :: QC_LANG2:def 14
 the_argument_of (the_left_argument_of (the_argument_of H));
correctness
coherence
the_argument_of (the_left_argument_of (the_argument_of H)) is QC-formula of A;
;
func the_right_disjunct_of H ->  QC-formula of A equals :: QC_LANG2:def 15
 the_argument_of (the_right_argument_of (the_argument_of H));
correctness
coherence
the_argument_of (the_right_argument_of (the_argument_of H)) is QC-formula of A;
;
func the_antecedent_of H ->  QC-formula of A equals :: QC_LANG2:def 16
 the_left_argument_of (the_argument_of H);
correctness
coherence
the_left_argument_of (the_argument_of H) is QC-formula of A;
;
end;

:: deftheorem  defines the_left_disjunct_of QC_LANG2:def_14_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds the_left_disjunct_of H = the_argument_of (the_left_argument_of (the_argument_of H));

:: deftheorem  defines the_right_disjunct_of QC_LANG2:def_15_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds the_right_disjunct_of H = the_argument_of (the_right_argument_of (the_argument_of H));

:: deftheorem  defines the_antecedent_of QC_LANG2:def_16_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds the_antecedent_of H = the_left_argument_of (the_argument_of H);

notation
let A be QC-alphabet ;
let H be Element of QC-WFF A;
synonym  the_consequent_of H for  the_right_disjunct_of H;
end;

definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
func the_left_side_of H ->  QC-formula of A equals :: QC_LANG2:def 17
 the_antecedent_of (the_left_argument_of H);
correctness
coherence
the_antecedent_of (the_left_argument_of H) is QC-formula of A;
;
func the_right_side_of H ->  QC-formula of A equals :: QC_LANG2:def 18
 the_consequent_of (the_left_argument_of H);
correctness
coherence
the_consequent_of (the_left_argument_of H) is QC-formula of A;
;
end;

:: deftheorem  defines the_left_side_of QC_LANG2:def_17_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds the_left_side_of H = the_antecedent_of (the_left_argument_of H);

:: deftheorem  defines the_right_side_of QC_LANG2:def_18_:_
 for A being QC-alphabet
for H being Element of QC-WFF A holds the_right_side_of H = the_consequent_of (the_left_argument_of H);

theorem Th29: :: QC_LANG2:29
for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( the_left_disjunct_of (F 'or' G) = F &amp; the_right_disjunct_of (F 'or' G) = G &amp; the_argument_of (F 'or' G) = ('not' F) '&amp;' ('not' G) )
proofend;

theorem Th30: :: QC_LANG2:30
for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( the_antecedent_of (F => G) = F &amp; the_consequent_of (F => G) = G &amp; the_argument_of (F => G) = F '&amp;' ('not' G) )
proofend;

theorem Th31: :: QC_LANG2:31
for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( the_left_side_of (F <=> G) = F &amp; the_right_side_of (F <=> G) = G &amp; the_left_argument_of (F <=> G) = F => G &amp; the_right_argument_of (F <=> G) = G => F )
proofend;

theorem :: QC_LANG2:32
for A being QC-alphabet
for x being bound_QC-variable of A
for H being Element of QC-WFF A holds the_argument_of (Ex (x,H)) = All (x,('not' H)) by Th1;

theorem :: QC_LANG2:33
for A being QC-alphabet
for H being Element of QC-WFF A st H is disjunctive holds
( H is conditional &amp; H is negative &amp; the_argument_of H is conjunctive &amp; the_left_argument_of (the_argument_of H) is negative &amp; the_right_argument_of (the_argument_of H) is negative )
proofend;

theorem :: QC_LANG2:34
for A being QC-alphabet
for H being Element of QC-WFF A st H is conditional holds
( H is negative &amp; the_argument_of H is conjunctive &amp; the_right_argument_of (the_argument_of H) is negative )
proofend;

theorem :: QC_LANG2:35
for A being QC-alphabet
for H being Element of QC-WFF A st H is biconditional holds
( H is conjunctive &amp; the_left_argument_of H is conditional &amp; the_right_argument_of H is conditional )
proofend;

theorem :: QC_LANG2:36
for A being QC-alphabet
for H being Element of QC-WFF A st H is existential holds
( H is negative &amp; the_argument_of H is universal &amp; the_scope_of (the_argument_of H) is negative )
proofend;

theorem :: QC_LANG2:37
for A being QC-alphabet
for H being Element of QC-WFF A st H is disjunctive holds
H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)
proofend;

theorem :: QC_LANG2:38
for A being QC-alphabet
for H being Element of QC-WFF A st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)
proofend;

theorem :: QC_LANG2:39
for A being QC-alphabet
for H being Element of QC-WFF A st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)
proofend;

theorem :: QC_LANG2:40
for A being QC-alphabet
for H being Element of QC-WFF A st H is existential holds
H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))))
proofend;

::
:: Immediate constituents of QC-formulae
::
definition
let A be QC-alphabet ;
let G, H be Element of QC-WFF A;
predG is_immediate_constituent_of H means :Def19: :: QC_LANG2:def 19
( H = 'not' G or ex F being Element of QC-WFF A st
( H = G '&amp;' F or H = F '&amp;' G ) or ex x being bound_QC-variable of A st H = All (x,G) );
end;

:: deftheorem Def19 defines is_immediate_constituent_of QC_LANG2:def_19_:_
 for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( G is_immediate_constituent_of H iff ( H = 'not' G or ex F being Element of QC-WFF A st
( H = G '&amp;' F or H = F '&amp;' G ) or ex x being bound_QC-variable of A st H = All (x,G) ) );

theorem Th41: :: QC_LANG2:41
for A being QC-alphabet
for H being Element of QC-WFF A holds not H is_immediate_constituent_of VERUM A
proofend;

theorem Th42: :: QC_LANG2:42
for A being QC-alphabet
for H being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
proofend;

theorem Th43: :: QC_LANG2:43
for A being QC-alphabet
for F, H being Element of QC-WFF A holds
( F is_immediate_constituent_of 'not' H iff F = H )
proofend;

theorem :: QC_LANG2:44
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_immediate_constituent_of FALSUM A iff H = VERUM A ) by Th43;

theorem Th45: :: QC_LANG2:45
for A being QC-alphabet
for F, G, H being Element of QC-WFF A holds
( F is_immediate_constituent_of G '&amp;' H iff ( F = G or F = H ) )
proofend;

theorem Th46: :: QC_LANG2:46
for A being QC-alphabet
for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_immediate_constituent_of All (x,H) iff F = H )
proofend;

theorem Th47: :: QC_LANG2:47
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is atomic holds
not F is_immediate_constituent_of H
proofend;

theorem Th48: :: QC_LANG2:48
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )
proofend;

theorem Th49: :: QC_LANG2:49
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is conjunctive holds
( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )
proofend;

theorem Th50: :: QC_LANG2:50
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )
proofend;

definition
let A be QC-alphabet ;
let G, H be Element of QC-WFF A;
predG is_subformula_of H means :Def20: :: QC_LANG2:def 20
 ex n being Element of NAT ex L being FinSequence st
( 1 <= n &amp; len L = n &amp; L . 1 = G &amp; L . n = H &amp; ( for k being Element of NAT st 1 <= k &amp; k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 &amp; L . (k + 1) = H1 &amp; G1 is_immediate_constituent_of H1 ) ) );
reflexivity
 for G being Element of QC-WFF A ex n being Element of NAT ex L being FinSequence st
( 1 <= n &amp; len L = n &amp; L . 1 = G &amp; L . n = G &amp; ( for k being Element of NAT st 1 <= k &amp; k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 &amp; L . (k + 1) = H1 &amp; G1 is_immediate_constituent_of H1 ) ) )
proofend;
end;

:: deftheorem Def20 defines is_subformula_of QC_LANG2:def_20_:_
 for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( G is_subformula_of H iff ex n being Element of NAT ex L being FinSequence st
( 1 <= n &amp; len L = n &amp; L . 1 = G &amp; L . n = H &amp; ( for k being Element of NAT st 1 <= k &amp; k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 &amp; L . (k + 1) = H1 &amp; G1 is_immediate_constituent_of H1 ) ) ) );

definition
let A be QC-alphabet ;
let H, F be Element of QC-WFF A;
predH is_proper_subformula_of F means :Def21: :: QC_LANG2:def 21
( H is_subformula_of F &amp; H <> F );
irreflexivity
 for H being Element of QC-WFF A holds
( not H is_subformula_of H or not H <> H ) ;
end;

:: deftheorem Def21 defines is_proper_subformula_of QC_LANG2:def_21_:_
 for A being QC-alphabet
for H, F being Element of QC-WFF A holds
( H is_proper_subformula_of F iff ( H is_subformula_of F &amp; H <> F ) );

theorem Th51: :: QC_LANG2:51
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
len (@ H) < len (@ F)
proofend;

theorem Th52: :: QC_LANG2:52
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_subformula_of F
proofend;

theorem Th53: :: QC_LANG2:53
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
proofend;

theorem Th54: :: QC_LANG2:54
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_proper_subformula_of F holds
len (@ H) < len (@ F)
proofend;

theorem Th55: :: QC_LANG2:55
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_proper_subformula_of F holds
ex G being Element of QC-WFF A st G is_immediate_constituent_of F
proofend;

theorem Th56: :: QC_LANG2:56
for A being QC-alphabet
for F, G, H being Element of QC-WFF A st F is_proper_subformula_of G &amp; G is_proper_subformula_of H holds
F is_proper_subformula_of H
proofend;

theorem Th57: :: QC_LANG2:57
for A being QC-alphabet
for F, G, H being Element of QC-WFF A st F is_subformula_of G &amp; G is_subformula_of H holds
F is_subformula_of H
proofend;

theorem Th58: :: QC_LANG2:58
for A being QC-alphabet
for G, H being Element of QC-WFF A st G is_subformula_of H &amp; H is_subformula_of G holds
G = H
proofend;

theorem Th59: :: QC_LANG2:59
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_subformula_of G )
proofend;

theorem :: QC_LANG2:60
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
proofend;

theorem Th61: :: QC_LANG2:61
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_subformula_of H or not H is_immediate_constituent_of G ) by Th53, Th59;

theorem Th62: :: QC_LANG2:62
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
proofend;

theorem Th63: :: QC_LANG2:63
for A being QC-alphabet
for F, G, H being Element of QC-WFF A st ( ( F is_proper_subformula_of G &amp; G is_subformula_of H ) or ( F is_subformula_of G &amp; G is_proper_subformula_of H ) or ( F is_subformula_of G &amp; G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G &amp; G is_subformula_of H ) or ( F is_proper_subformula_of G &amp; G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G &amp; G is_proper_subformula_of H ) ) holds
F is_proper_subformula_of H
proofend;

theorem Th64: :: QC_LANG2:64
for A being QC-alphabet
for F being Element of QC-WFF A holds not F is_proper_subformula_of VERUM A
proofend;

theorem Th65: :: QC_LANG2:65
for A being QC-alphabet
for F being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
proofend;

theorem Th66: :: QC_LANG2:66
for A being QC-alphabet
for F, H being Element of QC-WFF A holds
( F is_subformula_of H iff F is_proper_subformula_of 'not' H )
proofend;

theorem :: QC_LANG2:67
for A being QC-alphabet
for F, H being Element of QC-WFF A st 'not' F is_subformula_of H holds
F is_proper_subformula_of H
proofend;

theorem :: QC_LANG2:68
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is_proper_subformula_of FALSUM A iff F is_subformula_of VERUM A ) by Th66;

theorem Th69: :: QC_LANG2:69
for A being QC-alphabet
for F, G, H being Element of QC-WFF A holds
( ( F is_subformula_of G or F is_subformula_of H ) iff F is_proper_subformula_of G '&amp;' H )
proofend;

theorem :: QC_LANG2:70
for A being QC-alphabet
for F, G, H being Element of QC-WFF A st F '&amp;' G is_subformula_of H holds
( F is_proper_subformula_of H &amp; G is_proper_subformula_of H )
proofend;

theorem Th71: :: QC_LANG2:71
for A being QC-alphabet
for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_subformula_of H iff F is_proper_subformula_of All (x,H) )
proofend;

theorem :: QC_LANG2:72
for A being QC-alphabet
for H, F being Element of QC-WFF A
for x being bound_QC-variable of A st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
proofend;

theorem :: QC_LANG2:73
for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( F '&amp;' ('not' G) is_proper_subformula_of F => G &amp; F is_proper_subformula_of F => G &amp; 'not' G is_proper_subformula_of F => G &amp; G is_proper_subformula_of F => G )
proofend;

theorem :: QC_LANG2:74
for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( ('not' F) '&amp;' ('not' G) is_proper_subformula_of F 'or' G &amp; 'not' F is_proper_subformula_of F 'or' G &amp; 'not' G is_proper_subformula_of F 'or' G &amp; F is_proper_subformula_of F 'or' G &amp; G is_proper_subformula_of F 'or' G )
proofend;

theorem :: QC_LANG2:75
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is atomic holds
not F is_proper_subformula_of H
proofend;

theorem :: QC_LANG2:76
for A being QC-alphabet
for H being Element of QC-WFF A st H is negative holds
the_argument_of H is_proper_subformula_of H
proofend;

theorem :: QC_LANG2:77
for A being QC-alphabet
for H being Element of QC-WFF A st H is conjunctive holds
( the_left_argument_of H is_proper_subformula_of H &amp; the_right_argument_of H is_proper_subformula_of H )
proofend;

theorem :: QC_LANG2:78
for A being QC-alphabet
for H being Element of QC-WFF A st H is universal holds
the_scope_of H is_proper_subformula_of H
proofend;

theorem Th79: :: QC_LANG2:79
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_subformula_of VERUM A iff H = VERUM A )
proofend;

theorem Th80: :: QC_LANG2:80
for A being QC-alphabet
for H being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
proofend;

theorem Th81: :: QC_LANG2:81
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )
proofend;

::
:: Set of subformulae of QC-formulae
::
definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
func Subformulae H ->  set  means :Def22: :: QC_LANG2:def 22
 for a being set holds
( a in it iff ex F being Element of QC-WFF A st
( F = a &amp; F is_subformula_of H ) );
existence
 ex b1 being set st
for a being set holds
( a in b1 iff ex F being Element of QC-WFF A st
( F = a &amp; F is_subformula_of H ) )
proofend;
uniqueness
 for b1, b2 being set st ( for a being set holds
( a in b1 iff ex F being Element of QC-WFF A st
( F = a &amp; F is_subformula_of H ) ) ) &amp; ( for a being set holds
( a in b2 iff ex F being Element of QC-WFF A st
( F = a &amp; F is_subformula_of H ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines Subformulae QC_LANG2:def_22_:_
 for A being QC-alphabet
for H being Element of QC-WFF A
for b3 being set holds
( b3 = Subformulae H iff for a being set holds
( a in b3 iff ex F being Element of QC-WFF A st
( F = a &amp; F is_subformula_of H ) ) );

theorem Th82: :: QC_LANG2:82
for A being QC-alphabet
for G, H being Element of QC-WFF A st G in Subformulae H holds
G is_subformula_of H
proofend;

theorem Th83: :: QC_LANG2:83
for A being QC-alphabet
for F, H being Element of QC-WFF A st F is_subformula_of H holds
Subformulae F c= Subformulae H
proofend;

theorem :: QC_LANG2:84
for A being QC-alphabet
for G, H being Element of QC-WFF A st G in Subformulae H holds
Subformulae G c= Subformulae H by Th82, Th83;

theorem Th85: :: QC_LANG2:85
for A being QC-alphabet holds Subformulae (VERUM A) = {(VERUM A)}
proofend;

theorem Th86: :: QC_LANG2:86
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(P ! V)}
proofend;

theorem :: QC_LANG2:87
for A being QC-alphabet holds Subformulae (FALSUM A) = {(VERUM A),(FALSUM A)}
proofend;

theorem Th88: :: QC_LANG2:88
for A being QC-alphabet
for H being Element of QC-WFF A holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
proofend;

theorem Th89: :: QC_LANG2:89
for A being QC-alphabet
for H, F being Element of QC-WFF A holds Subformulae (H '&amp;' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&amp;' F)}
proofend;

theorem Th90: :: QC_LANG2:90
for A being QC-alphabet
for H being Element of QC-WFF A
for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
proofend;

theorem Th91: :: QC_LANG2:91
for A being QC-alphabet
for F, G being Element of QC-WFF A holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&amp;' ('not' G)),(F => G)}
proofend;

theorem :: QC_LANG2:92
for A being QC-alphabet
for F, G being Element of QC-WFF A holds Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&amp;' ('not' G)),(F 'or' G)}
proofend;

theorem :: QC_LANG2:93
for A being QC-alphabet
for F, G being Element of QC-WFF A holds Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&amp;' ('not' G)),(F => G),('not' F),(G '&amp;' ('not' F)),(G => F),(F <=> G)}
proofend;

theorem :: QC_LANG2:94
for A being QC-alphabet
for H being Element of QC-WFF A holds
( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )
proofend;

theorem :: QC_LANG2:95
for A being QC-alphabet
for H being Element of QC-WFF A st H is negative holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
proofend;

theorem :: QC_LANG2:96
for A being QC-alphabet
for H being Element of QC-WFF A st H is conjunctive holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
proofend;

theorem :: QC_LANG2:97
for A being QC-alphabet
for H being Element of QC-WFF A st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
proofend;

theorem :: QC_LANG2:98
for A being QC-alphabet
for H, G, F being Element of QC-WFF A st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) &amp; G in Subformulae F holds
H in Subformulae F
proofend;