:: QC_LANG2 semantic presentation

theorem Th1: :: QC_LANG2:1

for b₁, b₂ being Element of QC-WFF st 'not' b₁ = 'not' b₂ holds
b₁ = b₂ by FINSEQ_1:46;

theorem Th2: :: QC_LANG2:2

for b₁ being Element of QC-WFF holds the_argument_of ('not' b₁) = b₁

proof end;

theorem Th3: :: QC_LANG2:3

for b₁, b₂, b₃, b₄ being Element of QC-WFF st b₁ '&' b₂ = b₃ '&' b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th4: :: QC_LANG2:4

for b₁ being Element of QC-WFF st b₁ is conjunctive holds
b₁ = (the_left_argument_of b₁) '&' (the_right_argument_of b₁)

proof end;

theorem Th5: :: QC_LANG2:5

for b₁, b₂ being Element of QC-WFF holds
( the_left_argument_of (b₁ '&' b₂) = b₁ & the_right_argument_of (b₁ '&' b₂) = b₂ )

proof end;

theorem Th6: :: QC_LANG2:6

for b₁, b₂ being bound_QC-variable
for b₃, b₄ being Element of QC-WFF st All b₁,b₃ = All b₂,b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th7: :: QC_LANG2:7

for b₁ being Element of QC-WFF st b₁ is universal holds
b₁ = All (bound_in b₁),(the_scope_of b₁)

proof end;

theorem Th8: :: QC_LANG2:8

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF holds
( bound_in (All b₁,b₂) = b₁ & the_scope_of (All b₁,b₂) = b₂ )

proof end;

definition

func FALSUM -> QC-formula equals :: QC_LANG2:def 1
'not' VERUM ;
correctness ;
let c₁, c₂ be Element of QC-WFF ;
func c₁ => c₂ -> QC-formula equals :: QC_LANG2:def 2
'not' (a₁ '&' ('not' a₂));
correctness ;
func c₁ 'or' c₂ -> QC-formula equals :: QC_LANG2:def 3
'not' (('not' a₁) '&' ('not' a₂));
correctness ;

end;

:: deftheorem Def1 defines FALSUM QC_LANG2:def 1 :

:: deftheorem Def2 defines => QC_LANG2:def 2 :

:: deftheorem Def3 defines 'or' QC_LANG2:def 3 :

definition

let c₁, c₂ be Element of QC-WFF ;
func c₁ <=> c₂ -> QC-formula equals :: QC_LANG2:def 4
(a₁ => a₂) '&' (a₂ => a₁);
correctness ;

end;

:: deftheorem Def4 defines <=> QC_LANG2:def 4 :

definition

let c₁ be bound_QC-variable;
let c₂ be Element of QC-WFF ;
func Ex c₁,c₂ -> QC-formula equals :: QC_LANG2:def 5
'not' (All a₁,('not' a₂));
correctness ;

end;

:: deftheorem Def5 defines Ex QC_LANG2:def 5 :

theorem Th9: :: QC_LANG2:9

canceled;

theorem Th10: :: QC_LANG2:10

canceled;

theorem Th11: :: QC_LANG2:11

canceled;

theorem Th12: :: QC_LANG2:12

canceled;

theorem Th13: :: QC_LANG2:13

( FALSUM is negative & the_argument_of FALSUM = VERUM ) by Th2, QC_LANG1:def 18;

theorem Th14: :: QC_LANG2:14

for b₁, b₂ being Element of QC-WFF holds b₁ 'or' b₂ = ('not' b₁) => b₂ ;

theorem Th15: :: QC_LANG2:15

canceled;

theorem Th16: :: QC_LANG2:16

for b₁, b₂, b₃, b₄ being Element of QC-WFF st b₁ 'or' b₂ = b₃ 'or' b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th17: :: QC_LANG2:17

for b₁, b₂, b₃, b₄ being Element of QC-WFF st b₁ => b₂ = b₃ => b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th18: :: QC_LANG2:18

for b₁, b₂, b₃, b₄ being Element of QC-WFF st b₁ <=> b₂ = b₃ <=> b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th19: :: QC_LANG2:19

for b₁, b₂ being bound_QC-variable
for b₃, b₄ being Element of QC-WFF st Ex b₁,b₃ = Ex b₂,b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

definition

let c₁, c₂ be bound_QC-variable;
let c₃ be Element of QC-WFF ;
func All c₁,c₂,c₃ -> QC-formula equals :: QC_LANG2:def 6
All a₁,(All a₂,a₃);
correctness ;
func Ex c₁,c₂,c₃ -> QC-formula equals :: QC_LANG2:def 7
Ex a₁,(Ex a₂,a₃);
correctness ;

end;

:: deftheorem Def6 defines All QC_LANG2:def 6 :

:: deftheorem Def7 defines Ex QC_LANG2:def 7 :

theorem Th20: :: QC_LANG2:20

for b₁, b₂ being bound_QC-variable
for b₃ being Element of QC-WFF holds
( All b₁,b₂,b₃ = All b₁,(All b₂,b₃) & Ex b₁,b₂,b₃ = Ex b₁,(Ex b₂,b₃) ) ;

theorem Th21: :: QC_LANG2:21

for b₁, b₂ being Element of QC-WFF
for b₃, b₄, b₅, b₆ being bound_QC-variable st All b₃,b₅,b₁ = All b₄,b₆,b₂ holds
( b₃ = b₄ & b₅ = b₆ & b₁ = b₂ )

proof end;

theorem Th22: :: QC_LANG2:22

for b₁, b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of QC-WFF st All b₁,b₂,b₄ = All b₃,b₅ holds
( b₁ = b₃ & All b₂,b₄ = b₅ ) by Th6;

theorem Th23: :: QC_LANG2:23

for b₁, b₂ being Element of QC-WFF
for b₃, b₄, b₅, b₆ being bound_QC-variable st Ex b₃,b₅,b₁ = Ex b₄,b₆,b₂ holds
( b₃ = b₄ & b₅ = b₆ & b₁ = b₂ )

proof end;

theorem Th24: :: QC_LANG2:24

for b₁, b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of QC-WFF st Ex b₁,b₂,b₄ = Ex b₃,b₅ holds
( b₁ = b₃ & Ex b₂,b₄ = b₅ ) by Th19;

theorem Th25: :: QC_LANG2:25

for b₁, b₂ being bound_QC-variable
for b₃ being Element of QC-WFF holds
( All b₁,b₂,b₃ is universal & bound_in (All b₁,b₂,b₃) = b₁ & the_scope_of (All b₁,b₂,b₃) = All b₂,b₃ ) by Th8, QC_LANG1:def 20;

definition

let c₁, c₂, c₃ be bound_QC-variable;
let c₄ be Element of QC-WFF ;
func All c₁,c₂,c₃,c₄ -> QC-formula equals :: QC_LANG2:def 8
All a₁,(All a₂,a₃,a₄);
correctness ;
func Ex c₁,c₂,c₃,c₄ -> QC-formula equals :: QC_LANG2:def 9
Ex a₁,(Ex a₂,a₃,a₄);
correctness ;

end;

:: deftheorem Def8 defines All QC_LANG2:def 8 :

:: deftheorem Def9 defines Ex QC_LANG2:def 9 :

theorem Th26: :: QC_LANG2:26

for b₁, b₂, b₃ being bound_QC-variable
for b₄ being Element of QC-WFF holds
( All b₁,b₂,b₃,b₄ = All b₁,(All b₂,b₃,b₄) & Ex b₁,b₂,b₃,b₄ = Ex b₁,(Ex b₂,b₃,b₄) ) ;

theorem Th27: :: QC_LANG2:27

for b₁, b₂ being Element of QC-WFF
for b₃, b₄, b₅, b₆, b₇, b₈ being bound_QC-variable st All b₃,b₅,b₇,b₁ = All b₄,b₆,b₈,b₂ holds
( b₃ = b₄ & b₅ = b₆ & b₇ = b₈ & b₁ = b₂ )

proof end;

theorem Th28: :: QC_LANG2:28

for b₁, b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of QC-WFF
for b₆ being bound_QC-variable st All b₁,b₂,b₃,b₄ = All b₆,b₅ holds
( b₁ = b₆ & All b₂,b₃,b₄ = b₅ ) by Th6;

theorem Th29: :: QC_LANG2:29

for b₁, b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of QC-WFF
for b₆, b₇ being bound_QC-variable st All b₁,b₂,b₃,b₄ = All b₆,b₇,b₅ holds
( b₁ = b₆ & b₂ = b₇ & All b₃,b₄ = b₅ )

proof end;

theorem Th30: :: QC_LANG2:30

for b₁, b₂ being Element of QC-WFF
for b₃, b₄, b₅, b₆, b₇, b₈ being bound_QC-variable st Ex b₃,b₅,b₇,b₁ = Ex b₄,b₆,b₈,b₂ holds
( b₃ = b₄ & b₅ = b₆ & b₇ = b₈ & b₁ = b₂ )

proof end;

theorem Th31: :: QC_LANG2:31

for b₁, b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of QC-WFF
for b₆ being bound_QC-variable st Ex b₁,b₂,b₃,b₄ = Ex b₆,b₅ holds
( b₁ = b₆ & Ex b₂,b₃,b₄ = b₅ ) by Th19;

theorem Th32: :: QC_LANG2:32

for b₁, b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of QC-WFF
for b₆, b₇ being bound_QC-variable st Ex b₁,b₂,b₃,b₄ = Ex b₆,b₇,b₅ holds
( b₁ = b₆ & b₂ = b₇ & Ex b₃,b₄ = b₅ )

proof end;

theorem Th33: :: QC_LANG2:33

for b₁, b₂, b₃ being bound_QC-variable
for b₄ being Element of QC-WFF holds
( All b₁,b₂,b₃,b₄ is universal & bound_in (All b₁,b₂,b₃,b₄) = b₁ & the_scope_of (All b₁,b₂,b₃,b₄) = All b₂,b₃,b₄ ) by Th8, QC_LANG1:def 20;

definition

let c₁ be Element of QC-WFF ;
attr a₁ is disjunctive means :: QC_LANG2:def 10
ex b₁, b₂ being Element of QC-WFF st a₁ = b₁ 'or' b₂;
attr a₁ is conditional means :Def11: :: QC_LANG2:def 11
ex b₁, b₂ being Element of QC-WFF st a₁ = b₁ => b₂;
attr a₁ is biconditional means :: QC_LANG2:def 12
ex b₁, b₂ being Element of QC-WFF st a₁ = b₁ <=> b₂;
attr a₁ is existential means :Def13: :: QC_LANG2:def 13
ex b₁ being bound_QC-variableex b₂ being Element of QC-WFF st a₁ = Ex b₁,b₂;

end;

:: deftheorem Def10 defines disjunctive QC_LANG2:def 10 :

:: deftheorem Def11 defines conditional QC_LANG2:def 11 :

:: deftheorem Def12 defines biconditional QC_LANG2:def 12 :

:: deftheorem Def13 defines existential QC_LANG2:def 13 :

theorem Th34: :: QC_LANG2:34

canceled;

theorem Th35: :: QC_LANG2:35

canceled;

theorem Th36: :: QC_LANG2:36

canceled;

theorem Th37: :: QC_LANG2:37

canceled;

theorem Th38: :: QC_LANG2:38

for b₁, b₂, b₃ being bound_QC-variable
for b₄ being Element of QC-WFF holds
( Ex b₁,b₂,b₄ is existential & Ex b₁,b₂,b₃,b₄ is existential ) by Def13;

definition

let c₁ be Element of QC-WFF ;
func the_left_disjunct_of c₁ -> QC-formula equals :: QC_LANG2:def 14
the_argument_of (the_left_argument_of (the_argument_of a₁));
correctness ;
func the_right_disjunct_of c₁ -> QC-formula equals :: QC_LANG2:def 15
the_argument_of (the_right_argument_of (the_argument_of a₁));
correctness ;
func the_antecedent_of c₁ -> QC-formula equals :: QC_LANG2:def 16
the_left_argument_of (the_argument_of a₁);
correctness ;

end;

:: deftheorem Def14 defines the_left_disjunct_of QC_LANG2:def 14 :

:: deftheorem Def15 defines the_right_disjunct_of QC_LANG2:def 15 :

:: deftheorem Def16 defines the_antecedent_of QC_LANG2:def 16 :

notation

let c₁ be Element of QC-WFF ;
synonym the_consequent_of c₁ for the_right_disjunct_of c₁;

end;

definition

let c₁ be Element of QC-WFF ;
canceled;
func the_left_side_of c₁ -> QC-formula equals :: QC_LANG2:def 18
the_antecedent_of (the_left_argument_of a₁);
correctness ;
func the_right_side_of c₁ -> QC-formula equals :: QC_LANG2:def 19
the_consequent_of (the_left_argument_of a₁);
correctness ;

end;

:: deftheorem Def17 QC_LANG2:def 17 :

:: deftheorem Def18 defines the_left_side_of QC_LANG2:def 18 :

:: deftheorem Def19 defines the_right_side_of QC_LANG2:def 19 :

theorem Th39: :: QC_LANG2:39

canceled;

theorem Th40: :: QC_LANG2:40

canceled;

theorem Th41: :: QC_LANG2:41

canceled;

theorem Th42: :: QC_LANG2:42

canceled;

theorem Th43: :: QC_LANG2:43

canceled;

theorem Th44: :: QC_LANG2:44

canceled;

theorem Th45: :: QC_LANG2:45

for b₁, b₂ being Element of QC-WFF holds
( the_left_disjunct_of (b₁ 'or' b₂) = b₁ & the_right_disjunct_of (b₁ 'or' b₂) = b₂ & the_argument_of (b₁ 'or' b₂) = ('not' b₁) '&' ('not' b₂) )

proof end;

theorem Th46: :: QC_LANG2:46

for b₁, b₂ being Element of QC-WFF holds
( the_antecedent_of (b₁ => b₂) = b₁ & the_consequent_of (b₁ => b₂) = b₂ & the_argument_of (b₁ => b₂) = b₁ '&' ('not' b₂) )

proof end;

theorem Th47: :: QC_LANG2:47

for b₁, b₂ being Element of QC-WFF holds
( the_left_side_of (b₁ <=> b₂) = b₁ & the_right_side_of (b₁ <=> b₂) = b₂ & the_left_argument_of (b₁ <=> b₂) = b₁ => b₂ & the_right_argument_of (b₁ <=> b₂) = b₂ => b₁ )

proof end;

theorem Th48: :: QC_LANG2:48

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF holds the_argument_of (Ex b₁,b₂) = All b₁,('not' b₂) by Th2;

theorem Th49: :: QC_LANG2:49

for b₁ being Element of QC-WFF st b₁ is disjunctive holds
( b₁ is conditional & b₁ is negative & the_argument_of b₁ is conjunctive & the_left_argument_of (the_argument_of b₁) is negative & the_right_argument_of (the_argument_of b₁) is negative )

proof end;

theorem Th50: :: QC_LANG2:50

for b₁ being Element of QC-WFF st b₁ is conditional holds
( b₁ is negative & the_argument_of b₁ is conjunctive & the_right_argument_of (the_argument_of b₁) is negative )

proof end;

theorem Th51: :: QC_LANG2:51

for b₁ being Element of QC-WFF st b₁ is biconditional holds
( b₁ is conjunctive & the_left_argument_of b₁ is conditional & the_right_argument_of b₁ is conditional )

proof end;

theorem Th52: :: QC_LANG2:52

for b₁ being Element of QC-WFF st b₁ is existential holds
( b₁ is negative & the_argument_of b₁ is universal & the_scope_of (the_argument_of b₁) is negative )

proof end;

theorem Th53: :: QC_LANG2:53

for b₁ being Element of QC-WFF st b₁ is disjunctive holds
b₁ = (the_left_disjunct_of b₁) 'or' (the_right_disjunct_of b₁)

proof end;

theorem Th54: :: QC_LANG2:54

for b₁ being Element of QC-WFF st b₁ is conditional holds
b₁ = (the_antecedent_of b₁) => (the_consequent_of b₁)

proof end;

theorem Th55: :: QC_LANG2:55

for b₁ being Element of QC-WFF st b₁ is biconditional holds
b₁ = (the_left_side_of b₁) <=> (the_right_side_of b₁)

proof end;

theorem Th56: :: QC_LANG2:56

for b₁ being Element of QC-WFF st b₁ is existential holds
b₁ = Ex (bound_in (the_argument_of b₁)),(the_argument_of (the_scope_of (the_argument_of b₁)))

proof end;

definition

let c₁, c₂ be Element of QC-WFF ;
pred c₁ is_immediate_constituent_of c₂ means :Def20: :: QC_LANG2:def 20
( a₂ = 'not' a₁ or ex b₁ being Element of QC-WFF st
( a₂ = a₁ '&' b₁ or a₂ = b₁ '&' a₁ ) or ex b₁ being bound_QC-variable st a₂ = All b₁,a₁ );

end;

:: deftheorem Def20 defines is_immediate_constituent_of QC_LANG2:def 20 :

theorem Th57: :: QC_LANG2:57

canceled;

theorem Th58: :: QC_LANG2:58

for b₁ being Element of QC-WFF holds not b₁ is_immediate_constituent_of VERUM

proof end;

theorem Th59: :: QC_LANG2:59

for b₁ being Element of QC-WFF
for b₂ being Nat
for b₃ being QC-pred_symbol of b₂
for b₄ being QC-variable_list of b₂ holds not b₁ is_immediate_constituent_of b₃ ! b₄

proof end;

theorem Th60: :: QC_LANG2:60

for b₁, b₂ being Element of QC-WFF holds
( b₁ is_immediate_constituent_of 'not' b₂ iff b₁ = b₂ )

proof end;

theorem Th61: :: QC_LANG2:61

for b₁ being Element of QC-WFF holds
( b₁ is_immediate_constituent_of FALSUM iff b₁ = VERUM ) by Th60;

theorem Th62: :: QC_LANG2:62

for b₁, b₂, b₃ being Element of QC-WFF holds
( b₁ is_immediate_constituent_of b₂ '&' b₃ iff ( b₁ = b₂ or b₁ = b₃ ) )

proof end;

theorem Th63: :: QC_LANG2:63

for b₁, b₂ being Element of QC-WFF
for b₃ being bound_QC-variable holds
( b₁ is_immediate_constituent_of All b₃,b₂ iff b₁ = b₂ )

proof end;

theorem Th64: :: QC_LANG2:64

for b₁, b₂ being Element of QC-WFF st b₁ is atomic holds
not b₂ is_immediate_constituent_of b₁

proof end;

theorem Th65: :: QC_LANG2:65

for b₁, b₂ being Element of QC-WFF st b₁ is negative holds
( b₂ is_immediate_constituent_of b₁ iff b₂ = the_argument_of b₁ )

proof end;

theorem Th66: :: QC_LANG2:66

for b₁, b₂ being Element of QC-WFF st b₁ is conjunctive holds
( b₂ is_immediate_constituent_of b₁ iff ( b₂ = the_left_argument_of b₁ or b₂ = the_right_argument_of b₁ ) )

proof end;

theorem Th67: :: QC_LANG2:67

for b₁, b₂ being Element of QC-WFF st b₁ is universal holds
( b₂ is_immediate_constituent_of b₁ iff b₂ = the_scope_of b₁ )

proof end;

definition

let c₁, c₂ be Element of QC-WFF ;
pred c₁ is_subformula_of c₂ means :Def21: :: QC_LANG2:def 21
ex b₁ being Natex b₂ being FinSequence st
( 1 <= b₁ & len b₂ = b₁ & b₂ . 1 = a₁ & b₂ . b₁ = a₂ & ( for b₃ being Nat st 1 <= b₃ & b₃ < b₁ holds
ex b₄, b₅ being Element of QC-WFF st
( b₂ . b₃ = b₄ & b₂ . (b₃ + 1) = b₅ & b₄ is_immediate_constituent_of b₅ ) ) );
reflexivity

proof end;

end;

:: deftheorem Def21 defines is_subformula_of QC_LANG2:def 21 :

definition

let c₁, c₂ be Element of QC-WFF ;
pred c₁ is_proper_subformula_of c₂ means :Def22: :: QC_LANG2:def 22
( a₁ is_subformula_of a₂ & a₁ <> a₂ );
irreflexivity ;

end;

:: deftheorem Def22 defines is_proper_subformula_of QC_LANG2:def 22 :

theorem Th68: :: QC_LANG2:68

canceled;

theorem Th69: :: QC_LANG2:69

canceled;

theorem Th70: :: QC_LANG2:70

canceled;

theorem Th71: :: QC_LANG2:71

for b₁, b₂ being Element of QC-WFF st b₁ is_immediate_constituent_of b₂ holds
len (@ b₁) < len (@ b₂)

proof end;

theorem Th72: :: QC_LANG2:72

for b₁, b₂ being Element of QC-WFF st b₁ is_immediate_constituent_of b₂ holds
b₁ is_subformula_of b₂

proof end;

theorem Th73: :: QC_LANG2:73

for b₁, b₂ being Element of QC-WFF st b₁ is_immediate_constituent_of b₂ holds
b₁ is_proper_subformula_of b₂

proof end;

theorem Th74: :: QC_LANG2:74

for b₁, b₂ being Element of QC-WFF st b₁ is_proper_subformula_of b₂ holds
len (@ b₁) < len (@ b₂)

proof end;

theorem Th75: :: QC_LANG2:75

for b₁, b₂ being Element of QC-WFF st b₁ is_proper_subformula_of b₂ holds
ex b₃ being Element of QC-WFF st b₃ is_immediate_constituent_of b₂

proof end;

theorem Th76: :: QC_LANG2:76

for b₁, b₂, b₃ being Element of QC-WFF st b₁ is_proper_subformula_of b₂ & b₂ is_proper_subformula_of b₃ holds
b₁ is_proper_subformula_of b₃

proof end;

theorem Th77: :: QC_LANG2:77

for b₁, b₂, b₃ being Element of QC-WFF st b₁ is_subformula_of b₂ & b₂ is_subformula_of b₃ holds
b₁ is_subformula_of b₃

proof end;

theorem Th78: :: QC_LANG2:78

for b₁, b₂ being Element of QC-WFF st b₁ is_subformula_of b₂ & b₂ is_subformula_of b₁ holds
b₁ = b₂

proof end;

theorem Th79: :: QC_LANG2:79

for b₁, b₂ being Element of QC-WFF holds
( not b₁ is_proper_subformula_of b₂ or not b₂ is_subformula_of b₁ )

proof end;

theorem Th80: :: QC_LANG2:80

for b₁, b₂ being Element of QC-WFF holds
( not b₁ is_proper_subformula_of b₂ or not b₂ is_proper_subformula_of b₁ )

proof end;

theorem Th81: :: QC_LANG2:81

for b₁, b₂ being Element of QC-WFF holds
( not b₁ is_subformula_of b₂ or not b₂ is_immediate_constituent_of b₁ )

proof end;

theorem Th82: :: QC_LANG2:82

for b₁, b₂ being Element of QC-WFF holds
( not b₁ is_proper_subformula_of b₂ or not b₂ is_immediate_constituent_of b₁ )

proof end;

theorem Th83: :: QC_LANG2:83

for b₁, b₂, b₃ being Element of QC-WFF st ( ( b₁ is_proper_subformula_of b₂ & b₂ is_subformula_of b₃ ) or ( b₁ is_subformula_of b₂ & b₂ is_proper_subformula_of b₃ ) or ( b₁ is_subformula_of b₂ & b₂ is_immediate_constituent_of b₃ ) or ( b₁ is_immediate_constituent_of b₂ & b₂ is_subformula_of b₃ ) or ( b₁ is_proper_subformula_of b₂ & b₂ is_immediate_constituent_of b₃ ) or ( b₁ is_immediate_constituent_of b₂ & b₂ is_proper_subformula_of b₃ ) ) holds
b₁ is_proper_subformula_of b₃

proof end;

theorem Th84: :: QC_LANG2:84

for b₁ being Element of QC-WFF holds not b₁ is_proper_subformula_of VERUM by Th58, Th75;

theorem Th85: :: QC_LANG2:85

for b₁ being Element of QC-WFF
for b₂ being Nat
for b₃ being QC-pred_symbol of b₂
for b₄ being QC-variable_list of b₂ holds not b₁ is_proper_subformula_of b₃ ! b₄

proof end;

theorem Th86: :: QC_LANG2:86

for b₁, b₂ being Element of QC-WFF holds
( b₁ is_subformula_of b₂ iff b₁ is_proper_subformula_of 'not' b₂ )

proof end;

theorem Th87: :: QC_LANG2:87

for b₁, b₂ being Element of QC-WFF st 'not' b₁ is_subformula_of b₂ holds
b₁ is_proper_subformula_of b₂

proof end;

theorem Th88: :: QC_LANG2:88

for b₁ being Element of QC-WFF holds
( b₁ is_proper_subformula_of FALSUM iff b₁ is_subformula_of VERUM ) by Th86;

theorem Th89: :: QC_LANG2:89

for b₁, b₂, b₃ being Element of QC-WFF holds
( ( b₁ is_subformula_of b₂ or b₁ is_subformula_of b₃ ) iff b₁ is_proper_subformula_of b₂ '&' b₃ )

proof end;

theorem Th90: :: QC_LANG2:90

for b₁, b₂, b₃ being Element of QC-WFF st b₁ '&' b₂ is_subformula_of b₃ holds
( b₁ is_proper_subformula_of b₃ & b₂ is_proper_subformula_of b₃ )

proof end;

theorem Th91: :: QC_LANG2:91

for b₁, b₂ being Element of QC-WFF
for b₃ being bound_QC-variable holds
( b₁ is_subformula_of b₂ iff b₁ is_proper_subformula_of All b₃,b₂ )

proof end;

theorem Th92: :: QC_LANG2:92

for b₁, b₂ being Element of QC-WFF
for b₃ being bound_QC-variable st All b₃,b₁ is_subformula_of b₂ holds
b₁ is_proper_subformula_of b₂

proof end;

theorem Th93: :: QC_LANG2:93

for b₁, b₂ being Element of QC-WFF holds
( b₁ '&' ('not' b₂) is_proper_subformula_of b₁ => b₂ & b₁ is_proper_subformula_of b₁ => b₂ & 'not' b₂ is_proper_subformula_of b₁ => b₂ & b₂ is_proper_subformula_of b₁ => b₂ )

proof end;

theorem Th94: :: QC_LANG2:94

for b₁, b₂ being Element of QC-WFF holds
( ('not' b₁) '&' ('not' b₂) is_proper_subformula_of b₁ 'or' b₂ & 'not' b₁ is_proper_subformula_of b₁ 'or' b₂ & 'not' b₂ is_proper_subformula_of b₁ 'or' b₂ & b₁ is_proper_subformula_of b₁ 'or' b₂ & b₂ is_proper_subformula_of b₁ 'or' b₂ )

proof end;

theorem Th95: :: QC_LANG2:95

for b₁, b₂ being Element of QC-WFF st b₁ is atomic holds
not b₂ is_proper_subformula_of b₁

proof end;

theorem Th96: :: QC_LANG2:96

for b₁ being Element of QC-WFF st b₁ is negative holds
the_argument_of b₁ is_proper_subformula_of b₁

proof end;

theorem Th97: :: QC_LANG2:97

for b₁ being Element of QC-WFF st b₁ is conjunctive holds
( the_left_argument_of b₁ is_proper_subformula_of b₁ & the_right_argument_of b₁ is_proper_subformula_of b₁ )

proof end;

theorem Th98: :: QC_LANG2:98

for b₁ being Element of QC-WFF st b₁ is universal holds
the_scope_of b₁ is_proper_subformula_of b₁

proof end;

theorem Th99: :: QC_LANG2:99

for b₁ being Element of QC-WFF holds
( b₁ is_subformula_of VERUM iff b₁ = VERUM )

proof end;

theorem Th100: :: QC_LANG2:100

for b₁ being Element of QC-WFF
for b₂ being Nat
for b₃ being QC-pred_symbol of b₂
for b₄ being QC-variable_list of b₂ holds
( b₁ is_subformula_of b₃ ! b₄ iff b₁ = b₃ ! b₄ )

proof end;

theorem Th101: :: QC_LANG2:101

for b₁ being Element of QC-WFF holds
( b₁ is_subformula_of FALSUM iff ( b₁ = FALSUM or b₁ = VERUM ) )

proof end;

definition

let c₁ be Element of QC-WFF ;
func Subformulae c₁ -> set means :Def23: :: QC_LANG2:def 23
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being Element of QC-WFF st
( b₂ = b₁ & b₂ is_subformula_of a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines Subformulae QC_LANG2:def 23 :

theorem Th102: :: QC_LANG2:102

canceled;

theorem Th103: :: QC_LANG2:103

for b₁, b₂ being Element of QC-WFF st b₁ in Subformulae b₂ holds
b₁ is_subformula_of b₂

proof end;

theorem Th104: :: QC_LANG2:104

for b₁, b₂ being Element of QC-WFF st b₁ is_subformula_of b₂ holds
Subformulae b₁ c= Subformulae b₂

proof end;

theorem Th105: :: QC_LANG2:105

for b₁, b₂ being Element of QC-WFF st b₁ in Subformulae b₂ holds
Subformulae b₁ c= Subformulae b₂

proof end;

theorem Th106: :: QC_LANG2:106

canceled;

theorem Th107: :: QC_LANG2:107

Subformulae VERUM = {VERUM }

proof end;

theorem Th108: :: QC_LANG2:108

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁ holds Subformulae (b₂ ! b₃) = {(b₂ ! b₃)}

proof end;

theorem Th109: :: QC_LANG2:109

Subformulae FALSUM = {VERUM ,FALSUM }

proof end;

theorem Th110: :: QC_LANG2:110

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

proof end;

theorem Th111: :: QC_LANG2:111

for b₁, b₂ being Element of QC-WFF holds Subformulae (b₁ '&' b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {(b₁ '&' b₂)}

proof end;

theorem Th112: :: QC_LANG2:112

for b₁ being Element of QC-WFF
for b₂ being bound_QC-variable holds Subformulae (All b₂,b₁) = (Subformulae b₁) \/ {(All b₂,b₁)}

proof end;

theorem Th113: :: QC_LANG2:113

for b₁, b₂ being Element of QC-WFF holds Subformulae (b₁ => b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {('not' b₂),(b₁ '&' ('not' b₂)),(b₁ => b₂)}

proof end;

theorem Th114: :: QC_LANG2:114

for b₁, b₂ being Element of QC-WFF holds Subformulae (b₁ 'or' b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {('not' b₂),('not' b₁),(('not' b₁) '&' ('not' b₂)),(b₁ 'or' b₂)}

proof end;

theorem Th115: :: QC_LANG2:115

for b₁, b₂ being Element of QC-WFF holds Subformulae (b₁ <=> b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {('not' b₂),(b₁ '&' ('not' b₂)),(b₁ => b₂),('not' b₁),(b₂ '&' ('not' b₁)),(b₂ => b₁),(b₁ <=> b₂)}

proof end;

theorem Th116: :: QC_LANG2:116

for b₁ being Element of QC-WFF holds
( ( b₁ = VERUM or b₁ is atomic ) iff Subformulae b₁ = {b₁} )

proof end;

theorem Th117: :: QC_LANG2:117

for b₁ being Element of QC-WFF st b₁ is negative holds
Subformulae b₁ = (Subformulae (the_argument_of b₁)) \/ {b₁}

proof end;

theorem Th118: :: QC_LANG2:118

for b₁ being Element of QC-WFF st b₁ is conjunctive holds
Subformulae b₁ = ((Subformulae (the_left_argument_of b₁)) \/ (Subformulae (the_right_argument_of b₁))) \/ {b₁}

proof end;

theorem Th119: :: QC_LANG2:119

for b₁ being Element of QC-WFF st b₁ is universal holds
Subformulae b₁ = (Subformulae (the_scope_of b₁)) \/ {b₁}

proof end;

theorem Th120: :: QC_LANG2:120

for b₁, b₂, b₃ being Element of QC-WFF st ( b₁ is_immediate_constituent_of b₂ or b₁ is_proper_subformula_of b₂ or b₁ is_subformula_of b₂ ) & b₂ in Subformulae b₃ holds
b₁ in Subformulae b₃

proof end;