:: QC_LANG3 semantic presentation

scheme :: QC_LANG3:sch 1
s1{ F₁() -> non empty set , F₂() -> Function of QC-WFF ,F₁(), F₃() -> Function of QC-WFF ,F₁(), F₄() -> Element of F₁(), F₅( set ) -> Element of F₁(), F₆( set ) -> Element of F₁(), F₇( set , set ) -> Element of F₁(), F₈( set , set ) -> Element of F₁() } :

F₂() = F₃()

provided

E1: for b₁ being Element of QC-WFF
for b₂, b₃ being Element of F₁() holds
( ( b₁ = VERUM implies F₂() . b₁ = F₄() ) & ( b₁ is atomic implies F₂() . b₁ = F₅(b₁) ) & ( b₁ is negative & b₂ = F₂() . (the_argument_of b₁) implies F₂() . b₁ = F₆(b₂) ) & ( b₁ is conjunctive & b₂ = F₂() . (the_left_argument_of b₁) & b₃ = F₂() . (the_right_argument_of b₁) implies F₂() . b₁ = F₇(b₂,b₃) ) & ( b₁ is universal & b₂ = F₂() . (the_scope_of b₁) implies F₂() . b₁ = F₈(b₁,b₂) ) ) and
E2: for b₁ being Element of QC-WFF
for b₂, b₃ being Element of F₁() holds
( ( b₁ = VERUM implies F₃() . b₁ = F₄() ) & ( b₁ is atomic implies F₃() . b₁ = F₅(b₁) ) & ( b₁ is negative & b₂ = F₃() . (the_argument_of b₁) implies F₃() . b₁ = F₆(b₂) ) & ( b₁ is conjunctive & b₂ = F₃() . (the_left_argument_of b₁) & b₃ = F₃() . (the_right_argument_of b₁) implies F₃() . b₁ = F₇(b₂,b₃) ) & ( b₁ is universal & b₂ = F₃() . (the_scope_of b₁) implies F₃() . b₁ = F₈(b₁,b₂) ) )

proof end;

scheme :: QC_LANG3:sch 2
s2{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of QC-WFF , F₄( Element of QC-WFF ) -> Element of F₁(), F₅( Element of F₁()) -> Element of F₁(), F₆( Element of F₁(), Element of F₁()) -> Element of F₁(), F₇( Element of QC-WFF , Element of F₁()) -> Element of F₁() } :

( ex b₁ being Element of F₁()ex b₂ being Function of QC-WFF ,F₁() st
( b₁ = b₂ . F₃() & ( for b₃ being Element of QC-WFF
for b₄, b₅ being Element of F₁() holds
( ( b₃ = VERUM implies b₂ . b₃ = F₂() ) & ( b₃ is atomic implies b₂ . b₃ = F₄(b₃) ) & ( b₃ is negative & b₄ = b₂ . (the_argument_of b₃) implies b₂ . b₃ = F₅(b₄) ) & ( b₃ is conjunctive & b₄ = b₂ . (the_left_argument_of b₃) & b₅ = b₂ . (the_right_argument_of b₃) implies b₂ . b₃ = F₆(b₄,b₅) ) & ( b₃ is universal & b₄ = b₂ . (the_scope_of b₃) implies b₂ . b₃ = F₇(b₃,b₄) ) ) ) ) & ( for b₁, b₂ being Element of F₁() st ex b₃ being Function of QC-WFF ,F₁() st
( b₁ = b₃ . F₃() & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Element of F₁() holds
( ( b₄ = VERUM implies b₃ . b₄ = F₂() ) & ( b₄ is atomic implies b₃ . b₄ = F₄(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = F₅(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = F₆(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = F₇(b₄,b₅) ) ) ) ) & ex b₃ being Function of QC-WFF ,F₁() st
( b₂ = b₃ . F₃() & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Element of F₁() holds
( ( b₄ = VERUM implies b₃ . b₄ = F₂() ) & ( b₄ is atomic implies b₃ . b₄ = F₄(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = F₅(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = F₆(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = F₇(b₄,b₅) ) ) ) ) holds
b₁ = b₂ ) )

proof end;

scheme :: QC_LANG3:sch 3
s3{ F₁() -> non empty set , F₂( Element of QC-WFF ) -> Element of F₁(), F₃() -> Element of F₁(), F₄( Element of QC-WFF ) -> Element of F₁(), F₅( Element of F₁()) -> Element of F₁(), F₆( Element of F₁(), Element of F₁()) -> Element of F₁(), F₇( Element of QC-WFF , Element of F₁()) -> Element of F₁() } :

F₂(VERUM ) = F₃()

provided

E1: for b₁ being QC-formula
for b₂ being Element of F₁() holds
( b₂ = F₂(b₁) iff ex b₃ being Function of QC-WFF ,F₁() st
( b₂ = b₃ . b₁ & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Element of F₁() holds
( ( b₄ = VERUM implies b₃ . b₄ = F₃() ) & ( b₄ is atomic implies b₃ . b₄ = F₄(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = F₅(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = F₆(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = F₇(b₄,b₅) ) ) ) ) )

proof end;

scheme :: QC_LANG3:sch 4
s4{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( Element of QC-WFF ) -> Element of F₁(), F₄() -> QC-formula, F₅( Element of QC-WFF ) -> Element of F₁(), F₆( Element of F₁()) -> Element of F₁(), F₇( Element of F₁(), Element of F₁()) -> Element of F₁(), F₈( Element of QC-WFF , Element of F₁()) -> Element of F₁() } :

F₃(F₄()) = F₅(F₄())

provided

E1: for b₁ being QC-formula
for b₂ being Element of F₁() holds
( b₂ = F₃(b₁) iff ex b₃ being Function of QC-WFF ,F₁() st
( b₂ = b₃ . b₁ & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Element of F₁() holds
( ( b₄ = VERUM implies b₃ . b₄ = F₂() ) & ( b₄ is atomic implies b₃ . b₄ = F₅(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = F₆(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = F₇(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = F₈(b₄,b₅) ) ) ) ) ) and
E2: F₄() is atomic

proof end;

scheme :: QC_LANG3:sch 5
s5{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> QC-formula, F₄( Element of QC-WFF ) -> Element of F₁(), F₅( Element of F₁()) -> Element of F₁(), F₆( Element of F₁(), Element of F₁()) -> Element of F₁(), F₇( Element of QC-WFF , Element of F₁()) -> Element of F₁(), F₈( Element of QC-WFF ) -> Element of F₁() } :

F₈(F₃()) = F₅(F₈((the_argument_of F₃())))

provided

E1: for b₁ being QC-formula
for b₂ being Element of F₁() holds
( b₂ = F₈(b₁) iff ex b₃ being Function of QC-WFF ,F₁() st
( b₂ = b₃ . b₁ & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Element of F₁() holds
( ( b₄ = VERUM implies b₃ . b₄ = F₂() ) & ( b₄ is atomic implies b₃ . b₄ = F₄(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = F₅(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = F₆(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = F₇(b₄,b₅) ) ) ) ) ) and
E2: F₃() is negative

proof end;

scheme :: QC_LANG3:sch 6
s6{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( Element of QC-WFF ) -> Element of F₁(), F₄( Element of F₁()) -> Element of F₁(), F₅( Element of F₁(), Element of F₁()) -> Element of F₁(), F₆( Element of QC-WFF , Element of F₁()) -> Element of F₁(), F₇( Element of QC-WFF ) -> Element of F₁(), F₈() -> QC-formula } :

for b₁, b₂ being Element of F₁() st b₁ = F₇((the_left_argument_of F₈())) & b₂ = F₇((the_right_argument_of F₈())) holds
F₇(F₈()) = F₅(b₁,b₂)

provided

E1: for b₁ being QC-formula
for b₂ being Element of F₁() holds
( b₂ = F₇(b₁) iff ex b₃ being Function of QC-WFF ,F₁() st
( b₂ = b₃ . b₁ & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Element of F₁() holds
( ( b₄ = VERUM implies b₃ . b₄ = F₂() ) & ( b₄ is atomic implies b₃ . b₄ = F₃(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = F₄(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = F₅(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = F₆(b₄,b₅) ) ) ) ) ) and
E2: F₈() is conjunctive

proof end;

scheme :: QC_LANG3:sch 7
s7{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> QC-formula, F₄( Element of QC-WFF ) -> Element of F₁(), F₅( Element of F₁()) -> Element of F₁(), F₆( Element of F₁(), Element of F₁()) -> Element of F₁(), F₇( Element of QC-WFF , Element of F₁()) -> Element of F₁(), F₈( Element of QC-WFF ) -> Element of F₁() } :

F₈(F₃()) = F₇(F₃(),F₈((the_scope_of F₃())))

provided

proof end;

theorem Th1: :: QC_LANG3:1

canceled;

theorem Th2: :: QC_LANG3:2

canceled;

theorem Th3: :: QC_LANG3:3

for b₁ being QC-pred_symbol holds b₁ is QC-pred_symbol of (the_arity_of b₁)

proof end;

definition

let c₁ be FinSequence of QC-variables ;
let c₂ be non empty Subset of QC-variables ;
canceled;
func variables_in c₁,c₂ -> Subset of a₂ equals :: QC_LANG3:def 2
{ (a₁ . b₁) where B is Nat : ( 1 <= b₁ & b₁ <= len a₁ & a₁ . b₁ in a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 QC_LANG3:def 1 :

:: deftheorem Def2 defines variables_in QC_LANG3:def 2 :

theorem Th4: :: QC_LANG3:4

canceled;

theorem Th5: :: QC_LANG3:5

canceled;

theorem Th6: :: QC_LANG3:6

for b₁ being FinSequence of QC-variables holds still_not-bound_in b₁ = variables_in b₁,bound_QC-variables ;

deffunc H₁( Element of QC-WFF ) -> Element of bool bound_QC-variables = still_not-bound_in a₁;

deffunc H₂( Element of QC-WFF ) -> Element of bool bound_QC-variables = still_not-bound_in (the_arguments_of a₁);

deffunc H₃( Subset of bound_QC-variables ) -> Subset of bound_QC-variables = a₁;

deffunc H₄( Subset of bound_QC-variables , Subset of bound_QC-variables ) -> Element of bool bound_QC-variables = a₁ \/ a₂;

deffunc H₅( Element of QC-WFF , Subset of bound_QC-variables ) -> Element of bool bound_QC-variables = a₂ \ {(bound_in a₁)};

Lemma1: for b₁ being QC-formula
for b₂ being Subset of bound_QC-variables holds
( b₂ = H₁(b₁) iff ex b₃ being Function of QC-WFF , bool bound_QC-variables st
( b₂ = b₃ . b₁ & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Subset of bound_QC-variables holds
( ( b₄ = VERUM implies b₃ . b₄ = {} bound_QC-variables ) & ( b₄ is atomic implies b₃ . b₄ = H₂(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = H₃(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = H₄(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = H₅(b₄,b₅) ) ) ) ) )

proof end;

theorem Th7: :: QC_LANG3:7

still_not-bound_in VERUM = {}

proof end;

theorem Th8: :: QC_LANG3:8

for b₁ being QC-formula st b₁ is atomic holds
still_not-bound_in b₁ = still_not-bound_in (the_arguments_of b₁)

proof end;

theorem Th9: :: QC_LANG3:9

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁ holds still_not-bound_in (b₂ ! b₃) = still_not-bound_in b₃

proof end;

theorem Th10: :: QC_LANG3:10

for b₁ being QC-formula st b₁ is negative holds
still_not-bound_in b₁ = still_not-bound_in (the_argument_of b₁)

proof end;

theorem Th11: :: QC_LANG3:11

for b₁ being QC-formula holds still_not-bound_in ('not' b₁) = still_not-bound_in b₁

proof end;

theorem Th12: :: QC_LANG3:12

still_not-bound_in FALSUM = {} by Th7, Th11, QC_LANG2:def 1;

theorem Th13: :: QC_LANG3:13

for b₁ being QC-formula st b₁ is conjunctive holds
still_not-bound_in b₁ = (still_not-bound_in (the_left_argument_of b₁)) \/ (still_not-bound_in (the_right_argument_of b₁))

proof end;

theorem Th14: :: QC_LANG3:14

for b₁, b₂ being QC-formula holds still_not-bound_in (b₁ '&' b₂) = (still_not-bound_in b₁) \/ (still_not-bound_in b₂)

proof end;

theorem Th15: :: QC_LANG3:15

for b₁ being QC-formula st b₁ is universal holds
still_not-bound_in b₁ = (still_not-bound_in (the_scope_of b₁)) \ {(bound_in b₁)}

proof end;

theorem Th16: :: QC_LANG3:16

for b₁ being bound_QC-variable
for b₂ being QC-formula holds still_not-bound_in (All b₁,b₂) = (still_not-bound_in b₂) \ {b₁}

proof end;

theorem Th17: :: QC_LANG3:17

for b₁ being QC-formula st b₁ is disjunctive holds
still_not-bound_in b₁ = (still_not-bound_in (the_left_disjunct_of b₁)) \/ (still_not-bound_in (the_right_disjunct_of b₁))

proof end;

theorem Th18: :: QC_LANG3:18

for b₁, b₂ being QC-formula holds still_not-bound_in (b₁ 'or' b₂) = (still_not-bound_in b₁) \/ (still_not-bound_in b₂)

proof end;

theorem Th19: :: QC_LANG3:19

for b₁ being QC-formula st b₁ is conditional holds
still_not-bound_in b₁ = (still_not-bound_in (the_antecedent_of b₁)) \/ (still_not-bound_in (the_consequent_of b₁))

proof end;

theorem Th20: :: QC_LANG3:20

for b₁, b₂ being QC-formula holds still_not-bound_in (b₁ => b₂) = (still_not-bound_in b₁) \/ (still_not-bound_in b₂)

proof end;

theorem Th21: :: QC_LANG3:21

for b₁ being QC-formula st b₁ is biconditional holds
still_not-bound_in b₁ = (still_not-bound_in (the_left_side_of b₁)) \/ (still_not-bound_in (the_right_side_of b₁))

proof end;

theorem Th22: :: QC_LANG3:22

for b₁, b₂ being QC-formula holds still_not-bound_in (b₁ <=> b₂) = (still_not-bound_in b₁) \/ (still_not-bound_in b₂)

proof end;

theorem Th23: :: QC_LANG3:23

for b₁ being bound_QC-variable
for b₂ being QC-formula holds still_not-bound_in (Ex b₁,b₂) = (still_not-bound_in b₂) \ {b₁}

proof end;

theorem Th24: :: QC_LANG3:24

( VERUM is closed & FALSUM is closed ) by Th7, Th12, QC_LANG1:def 30;

theorem Th25: :: QC_LANG3:25

for b₁ being QC-formula holds
( b₁ is closed iff 'not' b₁ is closed )

proof end;

theorem Th26: :: QC_LANG3:26

for b₁, b₂ being QC-formula holds
( ( b₁ is closed & b₂ is closed ) iff b₁ '&' b₂ is closed )

proof end;

theorem Th27: :: QC_LANG3:27

for b₁ being bound_QC-variable
for b₂ being QC-formula holds
( All b₁,b₂ is closed iff still_not-bound_in b₂ c= {b₁} )

proof end;

theorem Th28: :: QC_LANG3:28

for b₁ being bound_QC-variable
for b₂ being QC-formula st b₂ is closed holds
All b₁,b₂ is closed

proof end;

theorem Th29: :: QC_LANG3:29

for b₁, b₂ being QC-formula holds
( ( b₁ is closed & b₂ is closed ) iff b₁ 'or' b₂ is closed )

proof end;

theorem Th30: :: QC_LANG3:30

for b₁, b₂ being QC-formula holds
( ( b₁ is closed & b₂ is closed ) iff b₁ => b₂ is closed )

proof end;

theorem Th31: :: QC_LANG3:31

for b₁, b₂ being QC-formula holds
( ( b₁ is closed & b₂ is closed ) iff b₁ <=> b₂ is closed )

proof end;

theorem Th32: :: QC_LANG3:32

for b₁ being bound_QC-variable
for b₂ being QC-formula holds
( Ex b₁,b₂ is closed iff still_not-bound_in b₂ c= {b₁} )

proof end;

theorem Th33: :: QC_LANG3:33

for b₁ being bound_QC-variable
for b₂ being QC-formula st b₂ is closed holds
Ex b₁,b₂ is closed

proof end;

definition

let c₁ be Nat;
func x. c₁ -> bound_QC-variable equals :: QC_LANG3:def 3
[4,a₁];
coherence

proof end;

end;

:: deftheorem Def3 defines x. QC_LANG3:def 3 :

theorem Th34: :: QC_LANG3:34

canceled;

theorem Th35: :: QC_LANG3:35

for b₁, b₂ being Nat st x. b₁ = x. b₂ holds
b₁ = b₂ by ZFMISC_1:33;

theorem Th36: :: QC_LANG3:36

for b₁ being bound_QC-variable ex b₂ being Nat st x. b₂ = b₁

proof end;

definition

let c₁ be Nat;
func a. c₁ -> free_QC-variable equals :: QC_LANG3:def 4
[6,a₁];
coherence

proof end;

end;

:: deftheorem Def4 defines a. QC_LANG3:def 4 :

theorem Th37: :: QC_LANG3:37

canceled;

theorem Th38: :: QC_LANG3:38

for b₁, b₂ being Nat st a. b₁ = a. b₂ holds
b₁ = b₂ by ZFMISC_1:33;

theorem Th39: :: QC_LANG3:39

for b₁ being free_QC-variable ex b₂ being Nat st a. b₂ = b₁

proof end;

theorem Th40: :: QC_LANG3:40

for b₁ being Element of fixed_QC-variables
for b₂ being Element of free_QC-variables holds b₁ <> b₂

proof end;

theorem Th41: :: QC_LANG3:41

for b₁ being Element of fixed_QC-variables
for b₂ being Element of bound_QC-variables holds b₁ <> b₂

proof end;

theorem Th42: :: QC_LANG3:42

for b₁ being Element of free_QC-variables
for b₂ being Element of bound_QC-variables holds b₁ <> b₂

proof end;

definition

let c₁ be non empty Subset of QC-variables ;
let c₂ be Element of QC-WFF ;
func Vars c₂,c₁ -> Subset of a₁ means :Def5: :: QC_LANG3:def 5
ex b₁ being Function of QC-WFF , bool a₁ st
( a₃ = b₁ . a₂ & ( for b₂ being Element of QC-WFF
for b₃, b₄ being Subset of a₁ holds
( ( b₂ = VERUM implies b₁ . b₂ = {} a₁ ) & ( b₂ is atomic implies b₁ . b₂ = variables_in (the_arguments_of b₂),a₁ ) & ( b₂ is negative & b₃ = b₁ . (the_argument_of b₂) implies b₁ . b₂ = b₃ ) & ( b₂ is conjunctive & b₃ = b₁ . (the_left_argument_of b₂) & b₄ = b₁ . (the_right_argument_of b₂) implies b₁ . b₂ = b₃ \/ b₄ ) & ( b₂ is universal & b₃ = b₁ . (the_scope_of b₂) implies b₁ . b₂ = b₃ ) ) ) );
correctness

proof end;

end;

:: deftheorem Def5 defines Vars QC_LANG3:def 5 :

E22: now

let c₁ be non empty Subset of QC-variables ;
deffunc H₆( Element of QC-WFF ) -> Subset of c₁ = Vars a₁,c₁;
deffunc H₇( Element of QC-WFF ) -> Subset of c₁ = variables_in (the_arguments_of a₁),c₁;
deffunc H₈( Subset of c₁) -> Subset of c₁ = a₁;
deffunc H₉( Subset of c₁, Subset of c₁) -> Element of bool c₁ = a₁ \/ a₂;
deffunc H₁₀( Element of QC-WFF , Subset of c₁) -> Subset of c₁ = a₂;
E23: for b₁ being Element of QC-WFF
for b₂ being Subset of c₁ holds
( b₂ = H₆(b₁) iff ex b₃ being Function of QC-WFF , bool c₁ st
( b₂ = b₃ . b₁ & ( for b₄ being Element of QC-WFF
for b₅, b₆ being Subset of c₁ holds
( ( b₄ = VERUM implies b₃ . b₄ = {} c₁ ) & ( b₄ is atomic implies b₃ . b₄ = H₇(b₄) ) & ( b₄ is negative & b₅ = b₃ . (the_argument_of b₄) implies b₃ . b₄ = H₈(b₅) ) & ( b₄ is conjunctive & b₅ = b₃ . (the_left_argument_of b₄) & b₆ = b₃ . (the_right_argument_of b₄) implies b₃ . b₄ = H₉(b₅,b₆) ) & ( b₄ is universal & b₅ = b₃ . (the_scope_of b₄) implies b₃ . b₄ = H₁₀(b₄,b₅) ) ) ) ) ) by Def5;
thus H₆( VERUM ) = {} c₁ from QC_LANG3:sch 3(E23)
.= {} ;
thus for b₁ being Element of QC-WFF st b₁ is atomic holds
Vars b₁,c₁ = variables_in (the_arguments_of b₁),c₁

proof

let c₂ be Element of QC-WFF ;
assume E24: c₂ is atomic ;
thus H₆(c₂) = H₇(c₂) from QC_LANG3:sch 4(E23, E24);

end;

thus for b₁ being Element of QC-WFF st b₁ is negative holds
Vars b₁,c₁ = Vars (the_argument_of b₁),c₁

proof

let c₂ be Element of QC-WFF ;
assume E24: c₂ is negative ;
thus H₆(c₂) = H₈(H₆( the_argument_of c₂)) from QC_LANG3:sch 5(E23, E24);

end;

thus for b₁ being Element of QC-WFF st b₁ is conjunctive holds
Vars b₁,c₁ = (Vars (the_left_argument_of b₁),c₁) \/ (Vars (the_right_argument_of b₁),c₁)

proof

let c₂ be Element of QC-WFF ;
assume E24: c₂ is conjunctive ;
for b₁, b₂ being Subset of c₁ st b₁ = H₆( the_left_argument_of c₂) & b₂ = H₆( the_right_argument_of c₂) holds
H₆(c₂) = H₉(b₁,b₂) from QC_LANG3:sch 6(E23, E24);
hence Vars c₂,c₁ = (Vars (the_left_argument_of c₂),c₁) \/ (Vars (the_right_argument_of c₂),c₁) ;

end;

thus for b₁ being Element of QC-WFF st b₁ is universal holds
Vars b₁,c₁ = Vars (the_scope_of b₁),c₁

proof

let c₂ be Element of QC-WFF ;
assume E24: c₂ is universal ;
thus H₆(c₂) = H₁₀(c₂,H₆( the_scope_of c₂)) from QC_LANG3:sch 7(E23, E24);

end;

theorem Th43: :: QC_LANG3:43

canceled;

theorem Th44: :: QC_LANG3:44

canceled;

theorem Th45: :: QC_LANG3:45

canceled;

theorem Th46: :: QC_LANG3:46

for b₁ being non empty Subset of QC-variables holds Vars VERUM ,b₁ = {} by Lemma22;

theorem Th47: :: QC_LANG3:47

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is atomic holds
( Vars b₁,b₂ = variables_in (the_arguments_of b₁),b₂ & Vars b₁,b₂ = { ((the_arguments_of b₁) . b₃) where B is Nat : ( 1 <= b₃ & b₃ <= len (the_arguments_of b₁) & (the_arguments_of b₁) . b₃ in b₂ ) } )

proof end;

theorem Th48: :: QC_LANG3:48

for b₁ being Nat
for b₂ being non empty Subset of QC-variables
for b₃ being QC-pred_symbol of b₁
for b₄ being QC-variable_list of b₁ holds
( Vars (b₃ ! b₄),b₂ = variables_in b₄,b₂ & Vars (b₃ ! b₄),b₂ = { (b₄ . b₅) where B is Nat : ( 1 <= b₅ & b₅ <= len b₄ & b₄ . b₅ in b₂ ) } )

proof end;

theorem Th49: :: QC_LANG3:49

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is negative holds
Vars b₁,b₂ = Vars (the_argument_of b₁),b₂ by Lemma22;

theorem Th50: :: QC_LANG3:50

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables holds Vars ('not' b₁),b₂ = Vars b₁,b₂

proof end;

theorem Th51: :: QC_LANG3:51

for b₁ being non empty Subset of QC-variables holds Vars FALSUM ,b₁ = {}

proof end;

theorem Th52: :: QC_LANG3:52

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is conjunctive holds
Vars b₁,b₂ = (Vars (the_left_argument_of b₁),b₂) \/ (Vars (the_right_argument_of b₁),b₂) by Lemma22;

theorem Th53: :: QC_LANG3:53

for b₁, b₂ being Element of QC-WFF
for b₃ being non empty Subset of QC-variables holds Vars (b₁ '&' b₂),b₃ = (Vars b₁,b₃) \/ (Vars b₂,b₃)

proof end;

theorem Th54: :: QC_LANG3:54

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is universal holds
Vars b₁,b₂ = Vars (the_scope_of b₁),b₂ by Lemma22;

theorem Th55: :: QC_LANG3:55

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF
for b₃ being non empty Subset of QC-variables holds Vars (All b₁,b₂),b₃ = Vars b₂,b₃

proof end;

theorem Th56: :: QC_LANG3:56

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is disjunctive holds
Vars b₁,b₂ = (Vars (the_left_disjunct_of b₁),b₂) \/ (Vars (the_right_disjunct_of b₁),b₂)

proof end;

theorem Th57: :: QC_LANG3:57

for b₁, b₂ being Element of QC-WFF
for b₃ being non empty Subset of QC-variables holds Vars (b₁ 'or' b₂),b₃ = (Vars b₁,b₃) \/ (Vars b₂,b₃)

proof end;

theorem Th58: :: QC_LANG3:58

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is conditional holds
Vars b₁,b₂ = (Vars (the_antecedent_of b₁),b₂) \/ (Vars (the_consequent_of b₁),b₂)

proof end;

theorem Th59: :: QC_LANG3:59

for b₁, b₂ being Element of QC-WFF
for b₃ being non empty Subset of QC-variables holds Vars (b₁ => b₂),b₃ = (Vars b₁,b₃) \/ (Vars b₂,b₃)

proof end;

theorem Th60: :: QC_LANG3:60

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is biconditional holds
Vars b₁,b₂ = (Vars (the_left_side_of b₁),b₂) \/ (Vars (the_right_side_of b₁),b₂)

proof end;

theorem Th61: :: QC_LANG3:61

for b₁, b₂ being Element of QC-WFF
for b₃ being non empty Subset of QC-variables holds Vars (b₁ <=> b₂),b₃ = (Vars b₁,b₃) \/ (Vars b₂,b₃)

proof end;

theorem Th62: :: QC_LANG3:62

for b₁ being Element of QC-WFF
for b₂ being non empty Subset of QC-variables st b₁ is existential holds
Vars b₁,b₂ = Vars (the_argument_of (the_scope_of (the_argument_of b₁))),b₂

proof end;

theorem Th63: :: QC_LANG3:63

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF
for b₃ being non empty Subset of QC-variables holds Vars (Ex b₁,b₂),b₃ = Vars b₂,b₃

proof end;

definition

let c₁ be Element of QC-WFF ;
func Free c₁ -> Subset of free_QC-variables equals :: QC_LANG3:def 6
Vars a₁,free_QC-variables ;
correctness ;

end;

:: deftheorem Def6 defines Free QC_LANG3:def 6 :

theorem Th64: :: QC_LANG3:64

canceled;

theorem Th65: :: QC_LANG3:65

Free VERUM = {} by Lemma22;

theorem Th66: :: QC_LANG3:66

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁ holds Free (b₂ ! b₃) = { (b₃ . b₄) where B is Nat : ( 1 <= b₄ & b₄ <= len b₃ & b₃ . b₄ in free_QC-variables ) } by Th48;

theorem Th67: :: QC_LANG3:67

for b₁ being Element of QC-WFF holds Free ('not' b₁) = Free b₁ by Th50;

theorem Th68: :: QC_LANG3:68

Free FALSUM = {} by Th51;

theorem Th69: :: QC_LANG3:69

for b₁, b₂ being Element of QC-WFF holds Free (b₁ '&' b₂) = (Free b₁) \/ (Free b₂) by Th53;

theorem Th70: :: QC_LANG3:70

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF holds Free (All b₁,b₂) = Free b₂ by Th55;

theorem Th71: :: QC_LANG3:71

for b₁, b₂ being Element of QC-WFF holds Free (b₁ 'or' b₂) = (Free b₁) \/ (Free b₂)

proof end;

theorem Th72: :: QC_LANG3:72

for b₁, b₂ being Element of QC-WFF holds Free (b₁ => b₂) = (Free b₁) \/ (Free b₂)

proof end;

theorem Th73: :: QC_LANG3:73

for b₁, b₂ being Element of QC-WFF holds Free (b₁ <=> b₂) = (Free b₁) \/ (Free b₂)

proof end;

theorem Th74: :: QC_LANG3:74

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF holds Free (Ex b₁,b₂) = Free b₂

proof end;

definition

let c₁ be Element of QC-WFF ;
func Fixed c₁ -> Subset of fixed_QC-variables equals :: QC_LANG3:def 7
Vars a₁,fixed_QC-variables ;
correctness ;

end;

:: deftheorem Def7 defines Fixed QC_LANG3:def 7 :

theorem Th75: :: QC_LANG3:75

canceled;

theorem Th76: :: QC_LANG3:76

Fixed VERUM = {} by Lemma22;

theorem Th77: :: QC_LANG3:77

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁ holds Fixed (b₂ ! b₃) = { (b₃ . b₄) where B is Nat : ( 1 <= b₄ & b₄ <= len b₃ & b₃ . b₄ in fixed_QC-variables ) } by Th48;

theorem Th78: :: QC_LANG3:78

for b₁ being Element of QC-WFF holds Fixed ('not' b₁) = Fixed b₁ by Th50;

theorem Th79: :: QC_LANG3:79

Fixed FALSUM = {} by Th76, Th78, QC_LANG2:def 1;

theorem Th80: :: QC_LANG3:80

for b₁, b₂ being Element of QC-WFF holds Fixed (b₁ '&' b₂) = (Fixed b₁) \/ (Fixed b₂) by Th53;

theorem Th81: :: QC_LANG3:81

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF holds Fixed (All b₁,b₂) = Fixed b₂ by Th55;

theorem Th82: :: QC_LANG3:82

for b₁, b₂ being Element of QC-WFF holds Fixed (b₁ 'or' b₂) = (Fixed b₁) \/ (Fixed b₂)

proof end;

theorem Th83: :: QC_LANG3:83

for b₁, b₂ being Element of QC-WFF holds Fixed (b₁ => b₂) = (Fixed b₁) \/ (Fixed b₂)

proof end;

theorem Th84: :: QC_LANG3:84

for b₁, b₂ being Element of QC-WFF holds Fixed (b₁ <=> b₂) = (Fixed b₁) \/ (Fixed b₂)

proof end;

theorem Th85: :: QC_LANG3:85

for b₁ being bound_QC-variable
for b₂ being Element of QC-WFF holds Fixed (Ex b₁,b₂) = Fixed b₂

proof end;