:: by Czes{\l}aw Byli\'nski and Grzegorz Bancerek

::

:: Received November 23, 1989

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

begin

scheme :: QC_LANG3:sch 1

QCFuncUniq{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Function of (QC-WFF F_{1}()),F_{2}(), F_{4}() -> Function of (QC-WFF F_{1}()),F_{2}(), F_{5}() -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}(), F_{7}( set ) -> Element of F_{2}(), F_{8}( set , set ) -> Element of F_{2}(), F_{9}( set , set ) -> Element of F_{2}() } :

provided

QCFuncUniq{ F

provided

A1:
for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F_{3}() . p = F_{5}() ) & ( p is atomic implies F_{3}() . p = F_{6}(p) ) & ( p is negative & d1 = F_{3}() . (the_argument_of p) implies F_{3}() . p = F_{7}(d1) ) & ( p is conjunctive & d1 = F_{3}() . (the_left_argument_of p) & d2 = F_{3}() . (the_right_argument_of p) implies F_{3}() . p = F_{8}(d1,d2) ) & ( p is universal & d1 = F_{3}() . (the_scope_of p) implies F_{3}() . p = F_{9}(p,d1) ) )
and

A2: for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F_{4}() . p = F_{5}() ) & ( p is atomic implies F_{4}() . p = F_{6}(p) ) & ( p is negative & d1 = F_{4}() . (the_argument_of p) implies F_{4}() . p = F_{7}(d1) ) & ( p is conjunctive & d1 = F_{4}() . (the_left_argument_of p) & d2 = F_{4}() . (the_right_argument_of p) implies F_{4}() . p = F_{8}(d1,d2) ) & ( p is universal & d1 = F_{4}() . (the_scope_of p) implies F_{4}() . p = F_{9}(p,d1) ) )

for d1, d2 being Element of F

( ( p = VERUM F

A2: for p being Element of QC-WFF F

for d1, d2 being Element of F

( ( p = VERUM F

proof end;

scheme :: QC_LANG3:sch 2

QCDefD{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}() -> Element of QC-WFF F_{1}(), F_{5}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{6}( Element of F_{2}()) -> Element of F_{2}(), F_{7}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{8}( Element of QC-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}() } :

QCDefD{ F

( ex d being Element of F_{2}() ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( d = F . F_{4}() & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{3}() ) & ( p is atomic implies F . p = F_{5}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{6}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{7}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{8}(p,d1) ) ) ) ) & ( for x1, x2 being Element of F_{2}() st ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( x1 = F . F_{4}() & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{3}() ) & ( p is atomic implies F . p = F_{5}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{6}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{7}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{8}(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( x2 = F . F_{4}() & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{3}() ) & ( p is atomic implies F . p = F_{5}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{6}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{7}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{8}(p,d1) ) ) ) ) holds

x1 = x2 ) )

( d = F . F

for d1, d2 being Element of F

( ( p = VERUM F

( x1 = F . F

for d1, d2 being Element of F

( ( p = VERUM F

( x2 = F . F

for d1, d2 being Element of F

( ( p = VERUM F

x1 = x2 ) )

proof end;

scheme :: QC_LANG3:sch 3

QCDResult9VERUM{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{4}() -> Element of F_{2}(), F_{5}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{6}( Element of F_{2}()) -> Element of F_{2}(), F_{7}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{8}( Element of QC-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}() } :

provided

QCDResult9VERUM{ F

provided

A1:
for p being QC-formula of F_{1}()

for d being Element of F_{2}() holds

( d = F_{3}(p) iff ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( d = F . p & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{4}() ) & ( p is atomic implies F . p = F_{5}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{6}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{7}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{8}(p,d1) ) ) ) ) )

for d being Element of F

( d = F

( d = F . p & ( for p being Element of QC-WFF F

for d1, d2 being Element of F

( ( p = VERUM F

proof end;

scheme :: QC_LANG3:sch 4

QCDResult9atomic{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{5}() -> QC-formula of F_{1}(), F_{6}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{7}( Element of F_{2}()) -> Element of F_{2}(), F_{8}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{9}( Element of QC-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}() } :

provided

QCDResult9atomic{ F

provided

A1:
for p being QC-formula of F_{1}()

for d being Element of F_{2}() holds

( d = F_{4}(p) iff ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( d = F . p & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{3}() ) & ( p is atomic implies F . p = F_{6}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{7}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{8}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{9}(p,d1) ) ) ) ) )
and

A2: F_{5}() is atomic

for d being Element of F

( d = F

( d = F . p & ( for p being Element of QC-WFF F

for d1, d2 being Element of F

( ( p = VERUM F

A2: F

proof end;

scheme :: QC_LANG3:sch 5

QCDResult9negative{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}() -> QC-formula of F_{1}(), F_{5}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{6}( Element of F_{2}()) -> Element of F_{2}(), F_{7}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{8}( Element of QC-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}(), F_{9}( Element of QC-WFF F_{1}()) -> Element of F_{2}() } :

provided

QCDResult9negative{ F

provided

A1:
for p being QC-formula of F_{1}()

for d being Element of F_{2}() holds

( d = F_{9}(p) iff ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( d = F . p & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{3}() ) & ( p is atomic implies F . p = F_{5}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{6}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{7}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{8}(p,d1) ) ) ) ) )
and

A2: F_{4}() is negative

for d being Element of F

( d = F

( d = F . p & ( for p being Element of QC-WFF F

for d1, d2 being Element of F

( ( p = VERUM F

A2: F

proof end;

scheme :: QC_LANG3:sch 6

QCDResult9conjunctive{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{5}( Element of F_{2}()) -> Element of F_{2}(), F_{6}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{7}( Element of QC-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}(), F_{8}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{9}() -> QC-formula of F_{1}() } :

QCDResult9conjunctive{ F

for d1, d2 being Element of F_{2}() st d1 = F_{8}((the_left_argument_of F_{9}())) & d2 = F_{8}((the_right_argument_of F_{9}())) holds

F_{8}(F_{9}()) = F_{6}(d1,d2)

providedF

A1:
for p being QC-formula of F_{1}()

for d being Element of F_{2}() holds

( d = F_{8}(p) iff ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( d = F . p & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{3}() ) & ( p is atomic implies F . p = F_{4}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{5}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{6}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{7}(p,d1) ) ) ) ) )
and

A2: F_{9}() is conjunctive

for d being Element of F

( d = F

( d = F . p & ( for p being Element of QC-WFF F

for d1, d2 being Element of F

( ( p = VERUM F

A2: F

proof end;

scheme :: QC_LANG3:sch 7

QCDResult9universal{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}() -> QC-formula of F_{1}(), F_{5}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{6}( Element of F_{2}()) -> Element of F_{2}(), F_{7}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{8}( Element of QC-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}(), F_{9}( Element of QC-WFF F_{1}()) -> Element of F_{2}() } :

provided

QCDResult9universal{ F

provided

A1:
for p being QC-formula of F_{1}()

for d being Element of F_{2}() holds

( d = F_{9}(p) iff ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( d = F . p & ( for p being Element of QC-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( p = VERUM F_{1}() implies F . p = F_{3}() ) & ( p is atomic implies F . p = F_{5}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F_{6}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F_{7}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F_{8}(p,d1) ) ) ) ) )
and

A2: F_{4}() is universal

for d being Element of F

( d = F

( d = F . p & ( for p being Element of QC-WFF F

for d1, d2 being Element of F

( ( p = VERUM F

A2: F

proof end;

theorem :: QC_LANG3:1

for A being QC-alphabet

for P being QC-pred_symbol of A holds P is QC-pred_symbol of (the_arity_of P),A

for P being QC-pred_symbol of A holds P is QC-pred_symbol of (the_arity_of P),A

proof end;

definition

let A be QC-alphabet ;

let l be FinSequence of QC-variables A;

let V be non empty Subset of (QC-variables A);

{ (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } is Subset of V

end;
let l be FinSequence of QC-variables A;

let V be non empty Subset of (QC-variables A);

func variables_in (l,V) -> Subset of V equals :: QC_LANG3:def 1

{ (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } ;

coherence { (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } ;

{ (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } is Subset of V

proof end;

:: deftheorem defines variables_in QC_LANG3:def 1 :

for A being QC-alphabet

for l being FinSequence of QC-variables A

for V being non empty Subset of (QC-variables A) holds variables_in (l,V) = { (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } ;

for A being QC-alphabet

for l being FinSequence of QC-variables A

for V being non empty Subset of (QC-variables A) holds variables_in (l,V) = { (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } ;

theorem :: QC_LANG3:2

for A being QC-alphabet

for l being FinSequence of QC-variables A holds still_not-bound_in l = variables_in (l,(bound_QC-variables A)) ;

for l being FinSequence of QC-variables A holds still_not-bound_in l = variables_in (l,(bound_QC-variables A)) ;

Lm1: now :: thesis: for A being QC-alphabet

for p being QC-formula of A

for d being Subset of (bound_QC-variables A) holds

( d = H_{1}(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H_{2}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H_{4}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H_{5}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H_{3}(p,d1) ) ) ) ) )

for p being QC-formula of A

for d being Subset of (bound_QC-variables A) holds

( d = H

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H

let A be QC-alphabet ; :: thesis: for p being QC-formula of A

for d being Subset of (bound_QC-variables A) holds

( d = H_{1}(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H_{2}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H_{4}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H_{5}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H_{3}(p,d1) ) ) ) ) )

deffunc H_{1}( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in $1;

deffunc H_{2}( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);

deffunc H_{3}( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};

deffunc H_{4}( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1;

deffunc H_{5}( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2;

thus for p being QC-formula of A

for d being Subset of (bound_QC-variables A) holds

( d = H_{1}(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H_{2}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H_{4}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H_{5}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H_{3}(p,d1) ) ) ) ) )
:: thesis: verum

end;
for d being Subset of (bound_QC-variables A) holds

( d = H

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H

deffunc H

deffunc H

deffunc H

deffunc H

deffunc H

thus for p being QC-formula of A

for d being Subset of (bound_QC-variables A) holds

( d = H

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H

proof

let p be QC-formula of A; :: thesis: for d being Subset of (bound_QC-variables A) holds

( d = H_{1}(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H_{2}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H_{4}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H_{5}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H_{3}(p,d1) ) ) ) ) )

let d be Subset of (bound_QC-variables A); :: thesis: ( d = H_{1}(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H_{2}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H_{4}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H_{5}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H_{3}(p,d1) ) ) ) ) )

thus ( d = still_not-bound_in p implies ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) ) ) :: thesis: ( ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H_{2}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H_{4}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H_{5}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H_{3}(p,d1) ) ) ) ) implies d = H_{1}(p) )

A3: for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ; :: thesis: d = H_{1}(p)

_{1}(p)
by A2, QC_LANG1:def 30; :: thesis: verum

end;
( d = H

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H

let d be Subset of (bound_QC-variables A); :: thesis: ( d = H

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H

thus ( d = still_not-bound_in p implies ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) ) ) :: thesis: ( ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H

proof

given F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A2:
d = F . p
and
assume
d = still_not-bound_in p
; :: thesis: ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )

then consider F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that

A1: ( d = F . p & ( for p being Element of QC-WFF A holds

( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) by QC_LANG1:def 30;

take F ; :: thesis: ( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )

thus d = F . p by A1; :: thesis: for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

let p be Element of QC-WFF A; :: thesis: for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

let d1, d2 be Subset of (bound_QC-variables A); :: thesis: ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

thus ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) ) by A1; :: thesis: ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

thus ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) by A1; :: thesis: verum

end;
( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )

then consider F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that

A1: ( d = F . p & ( for p being Element of QC-WFF A holds

( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) by QC_LANG1:def 30;

take F ; :: thesis: ( d = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )

thus d = F . p by A1; :: thesis: for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

let p be Element of QC-WFF A; :: thesis: for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

let d1, d2 be Subset of (bound_QC-variables A); :: thesis: ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

thus ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) ) by A1; :: thesis: ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )

thus ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) by A1; :: thesis: verum

A3: for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ; :: thesis: d = H

now :: thesis: for p being Element of QC-WFF A holds

( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

hence
d = H( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

let p be Element of QC-WFF A; :: thesis: ( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

thus F . (VERUM A) = {} by A3; :: thesis: ( ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

thus ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) :: thesis: ( ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

thus ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) by A3; :: thesis: ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} )

assume p is universal ; :: thesis: F . p = (F . (the_scope_of p)) \ {(bound_in p)}

hence F . p = (F . (the_scope_of p)) \ {(bound_in p)} by A3; :: thesis: verum

end;
thus F . (VERUM A) = {} by A3; :: thesis: ( ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

thus ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) :: thesis: ( ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

proof

thus
( p is negative implies F . p = F . (the_argument_of p) )
by A3; :: thesis: ( ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
assume
p is atomic
; :: thesis: F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) }

then F . p = still_not-bound_in (the_arguments_of p) by A3;

hence F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ; :: thesis: verum

end;
then F . p = still_not-bound_in (the_arguments_of p) by A3;

hence F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ; :: thesis: verum

thus ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) by A3; :: thesis: ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} )

assume p is universal ; :: thesis: F . p = (F . (the_scope_of p)) \ {(bound_in p)}

hence F . p = (F . (the_scope_of p)) \ {(bound_in p)} by A3; :: thesis: verum

theorem Th4: :: QC_LANG3:4

for A being QC-alphabet

for p being QC-formula of A st p is atomic holds

still_not-bound_in p = still_not-bound_in (the_arguments_of p)

for p being QC-formula of A st p is atomic holds

still_not-bound_in p = still_not-bound_in (the_arguments_of p)

proof end;

theorem :: QC_LANG3:5

for k being Element of NAT

for A being QC-alphabet

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l

for A being QC-alphabet

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l

proof end;

theorem Th6: :: QC_LANG3:6

for A being QC-alphabet

for p being QC-formula of A st p is negative holds

still_not-bound_in p = still_not-bound_in (the_argument_of p)

for p being QC-formula of A st p is negative holds

still_not-bound_in p = still_not-bound_in (the_argument_of p)

proof end;

theorem Th7: :: QC_LANG3:7

for A being QC-alphabet

for p being QC-formula of A holds still_not-bound_in ('not' p) = still_not-bound_in p

for p being QC-formula of A holds still_not-bound_in ('not' p) = still_not-bound_in p

proof end;

theorem Th9: :: QC_LANG3:9

for A being QC-alphabet

for p being QC-formula of A st p is conjunctive holds

still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))

for p being QC-formula of A st p is conjunctive holds

still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))

proof end;

theorem Th10: :: QC_LANG3:10

for A being QC-alphabet

for p, q being QC-formula of A holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)

for p, q being QC-formula of A holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)

proof end;

theorem Th11: :: QC_LANG3:11

for A being QC-alphabet

for p being QC-formula of A st p is universal holds

still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}

for p being QC-formula of A st p is universal holds

still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}

proof end;

theorem Th12: :: QC_LANG3:12

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A holds still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x}

for x being bound_QC-variable of A

for p being QC-formula of A holds still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x}

proof end;

theorem Th13: :: QC_LANG3:13

for A being QC-alphabet

for p being QC-formula of A st p is disjunctive holds

still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p))

for p being QC-formula of A st p is disjunctive holds

still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p))

proof end;

theorem :: QC_LANG3:14

for A being QC-alphabet

for p, q being QC-formula of A holds still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q)

for p, q being QC-formula of A holds still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q)

proof end;

theorem Th15: :: QC_LANG3:15

for A being QC-alphabet

for p being QC-formula of A st p is conditional holds

still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p))

for p being QC-formula of A st p is conditional holds

still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p))

proof end;

theorem Th16: :: QC_LANG3:16

for A being QC-alphabet

for p, q being QC-formula of A holds still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q)

for p, q being QC-formula of A holds still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q)

proof end;

theorem Th17: :: QC_LANG3:17

for A being QC-alphabet

for p being QC-formula of A st p is biconditional holds

still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))

for p being QC-formula of A st p is biconditional holds

still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))

proof end;

theorem :: QC_LANG3:18

for A being QC-alphabet

for p, q being QC-formula of A holds still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q)

for p, q being QC-formula of A holds still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q)

proof end;

theorem Th19: :: QC_LANG3:19

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}

for x being bound_QC-variable of A

for p being QC-formula of A holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}

proof end;

theorem Th22: :: QC_LANG3:22

for A being QC-alphabet

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p '&' q is closed )

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p '&' q is closed )

proof end;

theorem Th23: :: QC_LANG3:23

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A holds

( All (x,p) is closed iff still_not-bound_in p c= {x} )

for x being bound_QC-variable of A

for p being QC-formula of A holds

( All (x,p) is closed iff still_not-bound_in p c= {x} )

proof end;

theorem :: QC_LANG3:24

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A st p is closed holds

All (x,p) is closed

for x being bound_QC-variable of A

for p being QC-formula of A st p is closed holds

All (x,p) is closed

proof end;

theorem :: QC_LANG3:25

for A being QC-alphabet

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p 'or' q is closed )

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p 'or' q is closed )

proof end;

theorem Th26: :: QC_LANG3:26

for A being QC-alphabet

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p => q is closed )

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p => q is closed )

proof end;

theorem :: QC_LANG3:27

for A being QC-alphabet

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p <=> q is closed )

for p, q being QC-formula of A holds

( ( p is closed & q is closed ) iff p <=> q is closed )

proof end;

theorem Th28: :: QC_LANG3:28

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A holds

( Ex (x,p) is closed iff still_not-bound_in p c= {x} )

for x being bound_QC-variable of A

for p being QC-formula of A holds

( Ex (x,p) is closed iff still_not-bound_in p c= {x} )

proof end;

theorem :: QC_LANG3:29

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A st p is closed holds

Ex (x,p) is closed

for x being bound_QC-variable of A

for p being QC-formula of A st p is closed holds

Ex (x,p) is closed

proof end;

definition
end;

:: deftheorem defines x. QC_LANG3:def 2 :

for A being QC-alphabet

for s being QC-symbol of A holds x. s = [4,s];

for A being QC-alphabet

for s being QC-symbol of A holds x. s = [4,s];

definition
end;

:: deftheorem defines a. QC_LANG3:def 3 :

for A being QC-alphabet

for k being Element of NAT holds A a. k = [6,k];

for A being QC-alphabet

for k being Element of NAT holds A a. k = [6,k];

theorem :: QC_LANG3:32

for A being QC-alphabet

for c being Element of fixed_QC-variables A

for a being Element of free_QC-variables A holds c <> a

for c being Element of fixed_QC-variables A

for a being Element of free_QC-variables A holds c <> a

proof end;

theorem :: QC_LANG3:33

for A being QC-alphabet

for c being Element of fixed_QC-variables A

for x being Element of bound_QC-variables A holds c <> x

for c being Element of fixed_QC-variables A

for x being Element of bound_QC-variables A holds c <> x

proof end;

theorem :: QC_LANG3:34

for A being QC-alphabet

for a being Element of free_QC-variables A

for x being Element of bound_QC-variables A holds a <> x

for a being Element of free_QC-variables A

for x being Element of bound_QC-variables A holds a <> x

proof end;

definition

let A be QC-alphabet ;

let V be non empty Subset of (QC-variables A);

let p be Element of QC-WFF A;

existence

ex b_{1} being Subset of V ex F being Function of (QC-WFF A),(bool V) st

( b_{1} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) );

uniqueness

for b_{1}, b_{2} being Subset of V st ex F being Function of (QC-WFF A),(bool V) st

( b_{1} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) & ex F being Function of (QC-WFF A),(bool V) st

( b_{2} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) holds

b_{1} = b_{2};

end;
let V be non empty Subset of (QC-variables A);

let p be Element of QC-WFF A;

func Vars (p,V) -> Subset of V means :Def4: :: QC_LANG3:def 4

ex F being Function of (QC-WFF A),(bool V) st

( it = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) );

correctness ex F being Function of (QC-WFF A),(bool V) st

( it = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) );

existence

ex b

( b

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) );

uniqueness

for b

( b

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) & ex F being Function of (QC-WFF A),(bool V) st

( b

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines Vars QC_LANG3:def 4 :

for A being QC-alphabet

for V being non empty Subset of (QC-variables A)

for p being Element of QC-WFF A

for b_{4} being Subset of V holds

( b_{4} = Vars (p,V) iff ex F being Function of (QC-WFF A),(bool V) st

( b_{4} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) );

for A being QC-alphabet

for V being non empty Subset of (QC-variables A)

for p being Element of QC-WFF A

for b

( b

( b

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) );

Lm2: now :: thesis: for A being QC-alphabet

for V being non empty Subset of (QC-variables A) holds

( H_{1}( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

for V being non empty Subset of (QC-variables A) holds

( H

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

let A be QC-alphabet ; :: thesis: for V being non empty Subset of (QC-variables A) holds

( H_{1}( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

let V be non empty Subset of (QC-variables A); :: thesis: ( H_{1}( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

deffunc H_{1}( Element of QC-WFF A) -> Subset of V = Vars ($1,V);

deffunc H_{2}( Element of QC-WFF A) -> Subset of V = variables_in ((the_arguments_of $1),V);

deffunc H_{3}( Subset of V) -> Subset of V = $1;

deffunc H_{4}( Subset of V, Subset of V) -> Element of bool V = $1 \/ $2;

deffunc H_{5}( Element of QC-WFF A, Subset of V) -> Subset of V = $2;

A1: for p being Element of QC-WFF A

for X being Subset of V holds

( X = H_{1}(p) iff ex F being Function of (QC-WFF A),(bool V) st

( X = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = H_{2}(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H_{3}(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H_{4}(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H_{5}(p,d1) ) ) ) ) )
by Def4;

thus H_{1}( VERUM A) =
{} V
from QC_LANG3:sch 3(A1)

.= {} ; :: thesis: ( ( for p being Element of QC-WFF A st p is atomic holds

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

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

Vars (p,V) = variables_in ((the_arguments_of p),V) :: thesis: ( ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

Vars (p,V) = Vars ((the_argument_of p),V) :: thesis: ( ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) :: thesis: for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V)

Vars (p,V) = Vars ((the_scope_of p),V) :: thesis: verum

end;
( H

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

let V be non empty Subset of (QC-variables A); :: thesis: ( H

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

deffunc H

deffunc H

deffunc H

deffunc H

deffunc H

A1: for p being Element of QC-WFF A

for X being Subset of V holds

( X = H

( X = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of V holds

( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = H

thus H

.= {} ; :: thesis: ( ( for p being Element of QC-WFF A st p is atomic holds

Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

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

Vars (p,V) = variables_in ((the_arguments_of p),V) :: thesis: ( ( for p being Element of QC-WFF A st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

proof

thus
for p being Element of QC-WFF A st p is negative holds
let p be Element of QC-WFF A; :: thesis: ( p is atomic implies Vars (p,V) = variables_in ((the_arguments_of p),V) )

assume A2: p is atomic ; :: thesis: Vars (p,V) = variables_in ((the_arguments_of p),V)

thus H_{1}(p) = H_{2}(p)
from QC_LANG3:sch 4(A1, A2); :: thesis: verum

end;
assume A2: p is atomic ; :: thesis: Vars (p,V) = variables_in ((the_arguments_of p),V)

thus H

Vars (p,V) = Vars ((the_argument_of p),V) :: thesis: ( ( for p being Element of QC-WFF A st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) ) )

proof

thus
for p being Element of QC-WFF A st p is conjunctive holds
let p be Element of QC-WFF A; :: thesis: ( p is negative implies Vars (p,V) = Vars ((the_argument_of p),V) )

assume A3: p is negative ; :: thesis: Vars (p,V) = Vars ((the_argument_of p),V)

thus H_{1}(p) = H_{3}(H_{1}( the_argument_of p))
from QC_LANG3:sch 5(A1, A3); :: thesis: verum

end;
assume A3: p is negative ; :: thesis: Vars (p,V) = Vars ((the_argument_of p),V)

thus H

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) :: thesis: for p being Element of QC-WFF A st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V)

proof

thus
for p being Element of QC-WFF A st p is universal holds
let p be Element of QC-WFF A; :: thesis: ( p is conjunctive implies Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) )

assume A4: p is conjunctive ; :: thesis: Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V))

for d1, d2 being Subset of V st d1 = H_{1}( the_left_argument_of p) & d2 = H_{1}( the_right_argument_of p) holds

H_{1}(p) = H_{4}(d1,d2)
from QC_LANG3:sch 6(A1, A4);

hence Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ; :: thesis: verum

end;
assume A4: p is conjunctive ; :: thesis: Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V))

for d1, d2 being Subset of V st d1 = H

H

hence Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ; :: thesis: verum

Vars (p,V) = Vars ((the_scope_of p),V) :: thesis: verum

proof

let p be Element of QC-WFF A; :: thesis: ( p is universal implies Vars (p,V) = Vars ((the_scope_of p),V) )

assume A5: p is universal ; :: thesis: Vars (p,V) = Vars ((the_scope_of p),V)

thus H_{1}(p) = H_{5}(p,H_{1}( the_scope_of p))
from QC_LANG3:sch 7(A1, A5); :: thesis: verum

end;
assume A5: p is universal ; :: thesis: Vars (p,V) = Vars ((the_scope_of p),V)

thus H

theorem :: QC_LANG3:35

for A being QC-alphabet

for V being non empty Subset of (QC-variables A) holds Vars ((VERUM A),V) = {} by Lm2;

for V being non empty Subset of (QC-variables A) holds Vars ((VERUM A),V) = {} by Lm2;

theorem Th36: :: QC_LANG3:36

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is atomic holds

( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is atomic holds

( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )

proof end;

theorem Th37: :: QC_LANG3:37

for k being Element of NAT

for A being QC-alphabet

for V being non empty Subset of (QC-variables A)

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds

( Vars ((P ! l),V) = variables_in (l,V) & Vars ((P ! l),V) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } )

for A being QC-alphabet

for V being non empty Subset of (QC-variables A)

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds

( Vars ((P ! l),V) = variables_in (l,V) & Vars ((P ! l),V) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } )

proof end;

theorem :: QC_LANG3:38

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) by Lm2;

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is negative holds

Vars (p,V) = Vars ((the_argument_of p),V) by Lm2;

theorem Th39: :: QC_LANG3:39

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars (('not' p),V) = Vars (p,V)

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars (('not' p),V) = Vars (p,V)

proof end;

theorem Th40: :: QC_LANG3:40

for A being QC-alphabet

for V being non empty Subset of (QC-variables A) holds Vars ((FALSUM A),V) = {}

for V being non empty Subset of (QC-variables A) holds Vars ((FALSUM A),V) = {}

proof end;

theorem :: QC_LANG3:41

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) by Lm2;

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is conjunctive holds

Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) by Lm2;

theorem Th42: :: QC_LANG3:42

for A being QC-alphabet

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V))

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V))

proof end;

theorem :: QC_LANG3:43

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) by Lm2;

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is universal holds

Vars (p,V) = Vars ((the_scope_of p),V) by Lm2;

theorem Th44: :: QC_LANG3:44

for A being QC-alphabet

for x being bound_QC-variable of A

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((All (x,p)),V) = Vars (p,V)

for x being bound_QC-variable of A

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((All (x,p)),V) = Vars (p,V)

proof end;

theorem Th45: :: QC_LANG3:45

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is disjunctive holds

Vars (p,V) = (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V))

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is disjunctive holds

Vars (p,V) = (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V))

proof end;

theorem :: QC_LANG3:46

for A being QC-alphabet

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))

proof end;

theorem Th47: :: QC_LANG3:47

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is conditional holds

Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V))

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is conditional holds

Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V))

proof end;

theorem Th48: :: QC_LANG3:48

for A being QC-alphabet

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p => q),V) = (Vars (p,V)) \/ (Vars (q,V))

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p => q),V) = (Vars (p,V)) \/ (Vars (q,V))

proof end;

theorem Th49: :: QC_LANG3:49

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is biconditional holds

Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is biconditional holds

Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))

proof end;

theorem :: QC_LANG3:50

for A being QC-alphabet

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))

for p, q being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))

proof end;

theorem :: QC_LANG3:51

for A being QC-alphabet

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is existential holds

Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) st p is existential holds

Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)

proof end;

theorem :: QC_LANG3:52

for A being QC-alphabet

for x being bound_QC-variable of A

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V)

for x being bound_QC-variable of A

for p being Element of QC-WFF A

for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V)

proof end;

definition

let A be QC-alphabet ;

let p be Element of QC-WFF A;

coherence

Vars (p,(free_QC-variables A)) is Subset of (free_QC-variables A);

;

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

func Free p -> Subset of (free_QC-variables A) equals :: QC_LANG3:def 5

Vars (p,(free_QC-variables A));

correctness Vars (p,(free_QC-variables A));

coherence

Vars (p,(free_QC-variables A)) is Subset of (free_QC-variables A);

;

:: deftheorem defines Free QC_LANG3:def 5 :

for A being QC-alphabet

for p being Element of QC-WFF A holds Free p = Vars (p,(free_QC-variables A));

for A being QC-alphabet

for p being Element of QC-WFF A holds Free p = Vars (p,(free_QC-variables A));

theorem :: QC_LANG3:54

for k being Element of NAT

for A being QC-alphabet

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds Free (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by Th37;

for A being QC-alphabet

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds Free (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by Th37;

theorem :: QC_LANG3:55

theorem :: QC_LANG3:57

theorem :: QC_LANG3:58

for A being QC-alphabet

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Free (All (x,p)) = Free p by Th44;

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Free (All (x,p)) = Free p by Th44;

theorem :: QC_LANG3:59

for A being QC-alphabet

for p, q being Element of QC-WFF A holds Free (p 'or' q) = (Free p) \/ (Free q)

for p, q being Element of QC-WFF A holds Free (p 'or' q) = (Free p) \/ (Free q)

proof end;

theorem Th60: :: QC_LANG3:60

for A being QC-alphabet

for p, q being Element of QC-WFF A holds Free (p => q) = (Free p) \/ (Free q)

for p, q being Element of QC-WFF A holds Free (p => q) = (Free p) \/ (Free q)

proof end;

theorem :: QC_LANG3:61

for A being QC-alphabet

for p, q being Element of QC-WFF A holds Free (p <=> q) = (Free p) \/ (Free q)

for p, q being Element of QC-WFF A holds Free (p <=> q) = (Free p) \/ (Free q)

proof end;

theorem :: QC_LANG3:62

for A being QC-alphabet

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p

proof end;

definition

let A be QC-alphabet ;

let p be Element of QC-WFF A;

coherence

Vars (p,(fixed_QC-variables A)) is Subset of (fixed_QC-variables A);

;

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

func Fixed p -> Subset of (fixed_QC-variables A) equals :: QC_LANG3:def 6

Vars (p,(fixed_QC-variables A));

correctness Vars (p,(fixed_QC-variables A));

coherence

Vars (p,(fixed_QC-variables A)) is Subset of (fixed_QC-variables A);

;

:: deftheorem defines Fixed QC_LANG3:def 6 :

for A being QC-alphabet

for p being Element of QC-WFF A holds Fixed p = Vars (p,(fixed_QC-variables A));

for A being QC-alphabet

for p being Element of QC-WFF A holds Fixed p = Vars (p,(fixed_QC-variables A));

theorem :: QC_LANG3:64

for k being Element of NAT

for A being QC-alphabet

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds Fixed (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by Th37;

for A being QC-alphabet

for P being QC-pred_symbol of k,A

for l being QC-variable_list of k,A holds Fixed (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by Th37;

theorem :: QC_LANG3:65

theorem :: QC_LANG3:67

theorem :: QC_LANG3:68

for A being QC-alphabet

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Fixed (All (x,p)) = Fixed p by Th44;

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Fixed (All (x,p)) = Fixed p by Th44;

theorem :: QC_LANG3:69

for A being QC-alphabet

for p, q being Element of QC-WFF A holds Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)

for p, q being Element of QC-WFF A holds Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)

proof end;

theorem Th70: :: QC_LANG3:70

for A being QC-alphabet

for p, q being Element of QC-WFF A holds Fixed (p => q) = (Fixed p) \/ (Fixed q)

for p, q being Element of QC-WFF A holds Fixed (p => q) = (Fixed p) \/ (Fixed q)

proof end;

theorem :: QC_LANG3:71

for A being QC-alphabet

for p, q being Element of QC-WFF A holds Fixed (p <=> q) = (Fixed p) \/ (Fixed q)

for p, q being Element of QC-WFF A holds Fixed (p <=> q) = (Fixed p) \/ (Fixed q)

proof end;

theorem :: QC_LANG3:72

for A being QC-alphabet

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Fixed (Ex (x,p)) = Fixed p

for x being bound_QC-variable of A

for p being Element of QC-WFF A holds Fixed (Ex (x,p)) = Fixed p

proof end;