:: by Grzegorz Bancerek

::

:: Received November 23, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

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 )

for p, q, p1, q1 being Element of QC-WFF A st p '&' q = p1 '&' q1 holds

( p = p1 & q = q1 )

proof end;

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)

for p being Element of QC-WFF A st p is conjunctive holds

p = (the_left_argument_of p) '&' (the_right_argument_of p)

proof end;

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 )

for p, q being Element of QC-WFF A holds

( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )

proof end;

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 )

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 )

proof end;

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))

for p being Element of QC-WFF A st p is universal holds

p = All ((bound_in p),(the_scope_of p))

proof end;

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 )

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 )

proof end;

definition

let A be QC-alphabet ;

correctness

coherence

'not' (VERUM A) is QC-formula of A;

;

let p, q be Element of QC-WFF A;

correctness

coherence

'not' (p '&' ('not' q)) is QC-formula of A;

;

correctness

coherence

'not' (('not' p) '&' ('not' q)) is QC-formula of A;

;

end;
correctness

coherence

'not' (VERUM A) is QC-formula of A;

;

let p, q be Element of QC-WFF A;

correctness

coherence

'not' (p '&' ('not' q)) is QC-formula of A;

;

correctness

coherence

'not' (('not' p) '&' ('not' q)) is QC-formula of A;

;

:: deftheorem defines FALSUM QC_LANG2:def 1 :

for A being QC-alphabet holds FALSUM A = 'not' (VERUM A);

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));

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));

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;

correctness

coherence

(p => q) '&' (q => p) is QC-formula of A;

;

end;
let p, q be Element of QC-WFF A;

correctness

coherence

(p => q) '&' (q => p) is QC-formula of A;

;

:: 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) '&' (q => p);

for A being QC-alphabet

for p, q being Element of QC-WFF A holds p <=> q = (p => q) '&' (q => p);

definition

let A be QC-alphabet ;

let x be bound_QC-variable of A;

let p be Element of QC-WFF A;

correctness

coherence

'not' (All (x,('not' p))) is QC-formula of A;

;

end;
let x be bound_QC-variable of A;

let p be Element of QC-WFF A;

correctness

coherence

'not' (All (x,('not' p))) is QC-formula of A;

;

:: 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)));

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 & the_argument_of (FALSUM A) = VERUM A ) by Th1, QC_LANG1:def 19;

( FALSUM A is negative & the_argument_of (FALSUM A) = VERUM A ) by Th1, QC_LANG1:def 19;

theorem :: QC_LANG2:9

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 & q = q1 )

for p, q, p1, q1 being Element of QC-WFF A st p 'or' q = p1 'or' q1 holds

( p = p1 & q = q1 )

proof end;

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 & q = q1 )

for p, q, p1, q1 being Element of QC-WFF A st p => q = p1 => q1 holds

( p = p1 & q = q1 )

proof end;

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 & q = q1 )

for p, q, p1, q1 being Element of QC-WFF A st p <=> q = p1 <=> q1 holds

( p = p1 & q = q1 )

proof end;

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 & p = q )

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 & p = q )

proof end;

definition

let A be QC-alphabet ;

let x, y be bound_QC-variable of A;

let p be Element of QC-WFF A;

correctness

coherence

All (x,(All (y,p))) is QC-formula of A;

;

correctness

coherence

Ex (x,(Ex (y,p))) is QC-formula of A;

;

end;
let x, y be bound_QC-variable of A;

let p be Element of QC-WFF A;

correctness

coherence

All (x,(All (y,p))) is QC-formula of A;

;

correctness

coherence

Ex (x,(Ex (y,p))) is QC-formula of A;

;

:: 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)));

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)));

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

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 & y1 = y2 & p1 = p2 )

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 & y1 = y2 & p1 = p2 )

proof end;

theorem :: QC_LANG2:16

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 & y1 = y2 & p1 = p2 )

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 & y1 = y2 & p1 = p2 )

proof end;

theorem :: QC_LANG2:18

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 & bound_in (All (x,y,p)) = x & the_scope_of (All (x,y,p)) = All (y,p) ) by Th7, QC_LANG1:def 21;

for x, y being bound_QC-variable of A

for p being Element of QC-WFF A holds

( All (x,y,p) is universal & bound_in (All (x,y,p)) = x & 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;

correctness

coherence

All (x,(All (y,z,p))) is QC-formula of A;

;

correctness

coherence

Ex (x,(Ex (y,z,p))) is QC-formula of A;

;

end;
let x, y, z be bound_QC-variable of A;

let p be Element of QC-WFF A;

correctness

coherence

All (x,(All (y,z,p))) is QC-formula of A;

;

correctness

coherence

Ex (x,(Ex (y,z,p))) is QC-formula of A;

;

:: 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)));

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)));

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

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 & y1 = y2 & z1 = z2 & p1 = p2 )

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 & y1 = y2 & z1 = z2 & p1 = p2 )

proof end;

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 & All (y,z,p) = q ) by Th5;

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 & 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 & y = s & All (z,p) = q )

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 & y = s & All (z,p) = q )

proof end;

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 & y1 = y2 & z1 = z2 & p1 = p2 )

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 & y1 = y2 & z1 = z2 & p1 = p2 )

proof end;

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 & Ex (y,z,p) = q ) by Th13;

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 & 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 & y = s & Ex (z,p) = q )

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 & y = s & Ex (z,p) = q )

proof end;

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 & bound_in (All (x,y,z,p)) = x & the_scope_of (All (x,y,z,p)) = All (y,z,p) ) by Th7, QC_LANG1:def 21;

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 & bound_in (All (x,y,z,p)) = x & 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;

end;
let H be Element of QC-WFF A;

attr H is conditional means :Def11: :: QC_LANG2:def 11

ex p, q being Element of QC-WFF A st H = p => q;

ex p, q being Element of QC-WFF A st H = p => q;

attr H 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);

ex x being bound_QC-variable of A ex p being Element of QC-WFF A st H = Ex (x,p);

:: 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 );

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 );

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 );

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) );

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 & Ex (x,y,z,p) is existential ) by Def13;

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 & Ex (x,y,z,p) is existential ) by Def13;

definition

let A be QC-alphabet ;

let H be Element of QC-WFF A;

coherence

the_argument_of (the_left_argument_of (the_argument_of H)) is QC-formula of A;

;

coherence

the_argument_of (the_right_argument_of (the_argument_of H)) is QC-formula of A;

;

coherence

the_left_argument_of (the_argument_of H) is QC-formula of A;

;

end;
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 the_argument_of (the_left_argument_of (the_argument_of H));

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 the_argument_of (the_right_argument_of (the_argument_of H));

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 the_left_argument_of (the_argument_of H);

coherence

the_left_argument_of (the_argument_of H) is QC-formula of A;

;

:: 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));

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));

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);

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;
let H be Element of QC-WFF A;

synonym the_consequent_of H for the_right_disjunct_of H;

definition

let A be QC-alphabet ;

let H be Element of QC-WFF A;

coherence

the_antecedent_of (the_left_argument_of H) is QC-formula of A;

;

coherence

the_consequent_of (the_left_argument_of H) is QC-formula of A;

;

end;
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 the_antecedent_of (the_left_argument_of H);

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 the_consequent_of (the_left_argument_of H);

coherence

the_consequent_of (the_left_argument_of H) is QC-formula of A;

;

:: 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);

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);

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 & the_right_disjunct_of (F 'or' G) = G & the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) )

for F, G being Element of QC-WFF A holds

( the_left_disjunct_of (F 'or' G) = F & the_right_disjunct_of (F 'or' G) = G & the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) )

proof end;

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 & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )

for F, G being Element of QC-WFF A holds

( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )

proof end;

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 & the_right_side_of (F <=> G) = G & the_left_argument_of (F <=> G) = F => G & the_right_argument_of (F <=> G) = G => F )

for F, G being Element of QC-WFF A holds

( the_left_side_of (F <=> G) = F & the_right_side_of (F <=> G) = G & the_left_argument_of (F <=> G) = F => G & the_right_argument_of (F <=> G) = G => F )

proof end;

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;

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 & H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )

for H being Element of QC-WFF A st H is disjunctive holds

( H is conditional & H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )

proof end;

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 & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )

for H being Element of QC-WFF A st H is conditional holds

( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )

proof end;

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 & the_left_argument_of H is conditional & the_right_argument_of H is conditional )

for H being Element of QC-WFF A st H is biconditional holds

( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )

proof end;

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 & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )

for H being Element of QC-WFF A st H is existential holds

( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )

proof end;

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)

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)

proof end;

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)

for H being Element of QC-WFF A st H is conditional holds

H = (the_antecedent_of H) => (the_consequent_of H)

proof end;

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)

for H being Element of QC-WFF A st H is biconditional holds

H = (the_left_side_of H) <=> (the_right_side_of H)

proof end;

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))))

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))))

proof end;

definition

let A be QC-alphabet ;

let G, H be Element of QC-WFF A;

end;
let G, H be Element of QC-WFF A;

pred G 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 '&' F or H = F '&' G ) or ex x being bound_QC-variable of A st H = All (x,G) );

( H = 'not' G or ex F being Element of QC-WFF A st

( H = G '&' F or H = F '&' G ) or ex x being bound_QC-variable of A st H = All (x,G) );

:: 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 '&' F or H = F '&' G ) or ex x being bound_QC-variable of A st H = All (x,G) ) );

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 '&' F or H = F '&' 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

for H being Element of QC-WFF A holds not H is_immediate_constituent_of VERUM A

proof end;

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

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

proof end;

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 )

for F, H being Element of QC-WFF A holds

( F is_immediate_constituent_of 'not' H iff F = H )

proof end;

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;

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 '&' H iff ( F = G or F = H ) )

for F, G, H being Element of QC-WFF A holds

( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )

proof end;

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 )

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 )

proof end;

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

for H, F being Element of QC-WFF A st H is atomic holds

not F is_immediate_constituent_of H

proof end;

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 )

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 )

proof end;

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 ) )

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 ) )

proof end;

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 )

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 )

proof end;

definition

let A be QC-alphabet ;

let G, H be Element of QC-WFF A;

for G being Element of QC-WFF A ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = G & L . n = G & ( for k being Element of NAT st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF A st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )

end;
let G, H be Element of QC-WFF A;

pred G is_subformula_of H means :Def20: :: QC_LANG2:def 20

ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF A st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) );

reflexivity ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF A st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) );

for G being Element of QC-WFF A ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = G & L . n = G & ( for k being Element of NAT st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF A st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )

proof 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 & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF A st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );

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 & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF A st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );

definition

let A be QC-alphabet ;

let H, F be Element of QC-WFF A;

irreflexivity

for H being Element of QC-WFF A holds

( not H is_subformula_of H or not H <> H ) ;

end;
let H, F be Element of QC-WFF A;

irreflexivity

for H being Element of QC-WFF A holds

( not H is_subformula_of H or not H <> H ) ;

:: 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 & H <> F ) );

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 & 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)

for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds

len (@ H) < len (@ F)

proof end;

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

for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds

H is_subformula_of F

proof end;

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

for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds

H is_proper_subformula_of F

proof end;

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)

for H, F being Element of QC-WFF A st H is_proper_subformula_of F holds

len (@ H) < len (@ F)

proof end;

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

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

proof end;

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 & G is_proper_subformula_of H holds

F is_proper_subformula_of H

for F, G, H being Element of QC-WFF A st F is_proper_subformula_of G & G is_proper_subformula_of H holds

F is_proper_subformula_of H

proof end;

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 & G is_subformula_of H holds

F is_subformula_of H

for F, G, H being Element of QC-WFF A st F is_subformula_of G & G is_subformula_of H holds

F is_subformula_of H

proof end;

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 & H is_subformula_of G holds

G = H

for G, H being Element of QC-WFF A st G is_subformula_of H & H is_subformula_of G holds

G = H

proof end;

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 )

for G, H being Element of QC-WFF A holds

( not G is_proper_subformula_of H or not H is_subformula_of G )

proof end;

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 )

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 )

proof end;

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;

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 )

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 )

proof end;

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 & G is_subformula_of H ) or ( F is_subformula_of G & G is_proper_subformula_of H ) or ( F is_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_subformula_of H ) or ( F is_proper_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_proper_subformula_of H ) ) holds

F is_proper_subformula_of H

for F, G, H being Element of QC-WFF A st ( ( F is_proper_subformula_of G & G is_subformula_of H ) or ( F is_subformula_of G & G is_proper_subformula_of H ) or ( F is_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_subformula_of H ) or ( F is_proper_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_proper_subformula_of H ) ) holds

F is_proper_subformula_of H

proof end;

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

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

proof end;

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 )

for F, H being Element of QC-WFF A holds

( F is_subformula_of H iff F is_proper_subformula_of 'not' H )

proof end;

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

for F, H being Element of QC-WFF A st 'not' F is_subformula_of H holds

F is_proper_subformula_of H

proof end;

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;

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 '&' H )

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 '&' H )

proof end;

theorem :: QC_LANG2:70

for A being QC-alphabet

for F, G, H being Element of QC-WFF A st F '&' G is_subformula_of H holds

( F is_proper_subformula_of H & G is_proper_subformula_of H )

for F, G, H being Element of QC-WFF A st F '&' G is_subformula_of H holds

( F is_proper_subformula_of H & G is_proper_subformula_of H )

proof end;

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) )

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) )

proof end;

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

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

proof end;

theorem :: QC_LANG2:73

for A being QC-alphabet

for F, G being Element of QC-WFF A holds

( F '&' ('not' G) is_proper_subformula_of F => G & F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )

for F, G being Element of QC-WFF A holds

( F '&' ('not' G) is_proper_subformula_of F => G & F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )

proof end;

theorem :: QC_LANG2:74

for A being QC-alphabet

for F, G being Element of QC-WFF A holds

( ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )

for F, G being Element of QC-WFF A holds

( ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )

proof end;

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

for H, F being Element of QC-WFF A st H is atomic holds

not F is_proper_subformula_of H

proof end;

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

for H being Element of QC-WFF A st H is negative holds

the_argument_of H is_proper_subformula_of H

proof end;

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 & the_right_argument_of H is_proper_subformula_of H )

for H being Element of QC-WFF A st H is conjunctive holds

( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )

proof end;

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

for H being Element of QC-WFF A st H is universal holds

the_scope_of H is_proper_subformula_of H

proof end;

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 )

for H being Element of QC-WFF A holds

( H is_subformula_of VERUM A iff H = VERUM A )

proof end;

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 )

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 )

proof end;

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 ) )

for H being Element of QC-WFF A holds

( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )

proof end;

::

:: Set of subformulae of QC-formulae

::

:: Set of subformulae of QC-formulae

::

definition

let A be QC-alphabet ;

let H be Element of QC-WFF A;

ex b_{1} being set st

for a being set holds

( a in b_{1} iff ex F being Element of QC-WFF A st

( F = a & F is_subformula_of H ) )

for b_{1}, b_{2} being set st ( for a being set holds

( a in b_{1} iff ex F being Element of QC-WFF A st

( F = a & F is_subformula_of H ) ) ) & ( for a being set holds

( a in b_{2} iff ex F being Element of QC-WFF A st

( F = a & F is_subformula_of H ) ) ) holds

b_{1} = b_{2}

end;
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 & F is_subformula_of H ) );

existence for a being set holds

( a in it iff ex F being Element of QC-WFF A st

( F = a & F is_subformula_of H ) );

ex b

for a being set holds

( a in b

( F = a & F is_subformula_of H ) )

proof end;

uniqueness for b

( a in b

( F = a & F is_subformula_of H ) ) ) & ( for a being set holds

( a in b

( F = a & F is_subformula_of H ) ) ) holds

b

proof end;

:: deftheorem Def22 defines Subformulae QC_LANG2:def 22 :

for A being QC-alphabet

for H being Element of QC-WFF A

for b_{3} being set holds

( b_{3} = Subformulae H iff for a being set holds

( a in b_{3} iff ex F being Element of QC-WFF A st

( F = a & F is_subformula_of H ) ) );

for A being QC-alphabet

for H being Element of QC-WFF A

for b

( b

( a in b

( F = a & 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

for G, H being Element of QC-WFF A st G in Subformulae H holds

G is_subformula_of H

proof end;

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

for F, H being Element of QC-WFF A st F is_subformula_of H holds

Subformulae F c= Subformulae H

proof end;

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;

for G, H being Element of QC-WFF A st G in Subformulae H holds

Subformulae G c= Subformulae H by Th82, Th83;

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)}

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)}

proof end;

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)}

for H being Element of QC-WFF A holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}

proof end;

theorem Th89: :: QC_LANG2:89

for A being QC-alphabet

for H, F being Element of QC-WFF A holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}

for H, F being Element of QC-WFF A holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}

proof end;

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))}

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))}

proof end;

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 '&' ('not' G)),(F => G)}

for F, G being Element of QC-WFF A holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}

proof end;

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) '&' ('not' G)),(F 'or' G)}

for F, G being Element of QC-WFF A holds Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}

proof end;

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 '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}

for F, G being Element of QC-WFF A holds Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}

proof end;

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} )

for H being Element of QC-WFF A holds

( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )

proof end;

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}

for H being Element of QC-WFF A st H is negative holds

Subformulae H = (Subformulae (the_argument_of H)) \/ {H}

proof end;

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}

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}

proof end;

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}

for H being Element of QC-WFF A st H is universal holds

Subformulae H = (Subformulae (the_scope_of H)) \/ {H}

proof end;

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 ) & G in Subformulae F holds

H in Subformulae F

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 ) & G in Subformulae F holds

H in Subformulae F

proof end;

:: Immediate constituents of QC-formulae

::