:: QC_LANG3 semantic presentation

begin


scheme :: QC_LANG3:sch 1
QCFuncUniq{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Function of (QC-WFF F1()),F2(), F4() ->  Function of (QC-WFF F1()),F2(), F5() ->  Element of F2(), F6( set ) ->  Element of F2(), F7( set ) ->  Element of F2(), F8( set , set ) ->  Element of F2(), F9( set , set ) ->  Element of F2() } :
 F3() = F4()
provided
A1: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F3() . p = F5() ) & ( p is atomic implies F3() . p = F6(p) ) & ( p is negative & d1 = F3() . (the_argument_of p) implies F3() . p = F7(d1) ) & ( p is conjunctive & d1 = F3() . (the_left_argument_of p) & d2 = F3() . (the_right_argument_of p) implies F3() . p = F8(d1,d2) ) & ( p is universal & d1 = F3() . (the_scope_of p) implies F3() . p = F9(p,d1) ) ) and
A2: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F4() . p = F5() ) & ( p is atomic implies F4() . p = F6(p) ) & ( p is negative & d1 = F4() . (the_argument_of p) implies F4() . p = F7(d1) ) & ( p is conjunctive & d1 = F4() . (the_left_argument_of p) & d2 = F4() . (the_right_argument_of p) implies F4() . p = F8(d1,d2) ) & ( p is universal & d1 = F4() . (the_scope_of p) implies F4() . p = F9(p,d1) ) )
proof
defpred S1[ Element of QC-WFF F1()] means F3() . $1 = F4() . $1;
A3: for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1() holds S1[P ! l]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1() holds S1[P ! l]
let P be QC-pred_symbol of k,F1(); ::_thesis: for l being QC-variable_list of k,F1() holds S1[P ! l]
let l be QC-variable_list of k,F1(); ::_thesis: S1[P ! l]
A4: P ! l is atomic by QC_LANG1:def_18;
hence F3() . (P ! l) = F6((P ! l)) by A1
.= F4() . (P ! l) by A2, A4 ;
::_thesis: verum
end;
A5: for x being bound_QC-variable of F1()
for p being Element of QC-WFF F1() st S1[p] holds
S1[ All (x,p)]
proof
let x be bound_QC-variable of F1(); ::_thesis: for p being Element of QC-WFF F1() st S1[p] holds
S1[ All (x,p)]
let p be Element of QC-WFF F1(); ::_thesis: ( S1[p] implies S1[ All (x,p)] )
assume A6: F3() . p = F4() . p ; ::_thesis: S1[ All (x,p)]
A7: All (x,p) is universal by QC_LANG1:def_21;
then  the_scope_of (All (x,p)) = p by QC_LANG1:def_28;
hence F3() . (All (x,p)) = F9((All (x,p)),(F4() . (the_scope_of (All (x,p))))) by A1, A6, A7
.= F4() . (All (x,p)) by A2, A7 ;
::_thesis: verum
end;
A8: for p, q being Element of QC-WFF F1() st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF F1(); ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A9: ( F3() . p = F4() . p & F3() . q = F4() . q ) ; ::_thesis: S1[p '&' q]
A10: p '&' q is conjunctive by QC_LANG1:def_20;
then A11: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def_25, QC_LANG1:def_26;
hence F3() . (p '&' q) = F8((F4() . p),(F4() . q)) by A1, A9, A10
.= F4() . (p '&' q) by A2, A10, A11 ;
::_thesis: verum
end;
A12: for p being Element of QC-WFF F1() st S1[p] holds
S1[ 'not' p]
proof
let p be Element of QC-WFF F1(); ::_thesis: ( S1[p] implies S1[ 'not' p] )
assume A13: F3() . p = F4() . p ; ::_thesis: S1[ 'not' p]
A14: 'not' p is negative by QC_LANG1:def_19;
then A15: the_argument_of ('not' p) = p by QC_LANG1:def_24;
hence F3() . ('not' p) = F7((F4() . p)) by A1, A13, A14
.= F4() . ('not' p) by A2, A14, A15 ;
::_thesis: verum
end;
 F3() . (VERUM F1()) = F5() by A1;
then A16: S1[ VERUM F1()] by A2;
 for p being Element of QC-WFF F1() holds S1[p] from QC_LANG1:sch_1(A3, A16, A12, A8, A5);
hence  F3() = F4() by FUNCT_2:63; ::_thesis: verum
end;

scheme :: QC_LANG3:sch 2
QCDefD{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4() ->  Element of QC-WFF F1(), F5( Element of QC-WFF F1()) ->  Element of F2(), F6( Element of F2()) ->  Element of F2(), F7( Element of F2(), Element of F2()) ->  Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) ->  Element of F2() } :
 ( ex d being Element of F2() ex F being Function of (QC-WFF F1()),F2() st
( d = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ( for x1, x2 being Element of F2() st ex F being Function of (QC-WFF F1()),F2() st
( x1 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F1()),F2() st
( x2 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) holds
x1 = x2 ) )
proof
thus  ex d being Element of F2() ex F being Function of (QC-WFF F1()),F2() st
( d = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ::_thesis: for x1, x2 being Element of F2() st ex F being Function of (QC-WFF F1()),F2() st
( x1 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F1()),F2() st
( x2 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) holds
x1 = x2
proof
consider F being Function of (QC-WFF F1()),F2() such that
A1: ( F . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = F5(p) ) & ( p is negative implies F . p = F6((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F7((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F8(p,(F . (the_scope_of p))) ) ) ) ) from QC_LANG1:sch_3();
take  F . F4() ; ::_thesis: ex F being Function of (QC-WFF F1()),F2() st
( F . F4() = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) )
take  F ; ::_thesis: ( F . F4() = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) )
thus  ( F . F4() = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) by A1; ::_thesis: verum
end;
let x1, x2 be Element of F2(); ::_thesis: ( ex F being Function of (QC-WFF F1()),F2() st
( x1 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F1()),F2() st
( x2 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) implies x1 = x2 )
given F1 being Function of (QC-WFF F1()),F2() such that A2: x1 = F1 . F4() and
A3: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F1 . p = F3() ) & ( p is atomic implies F1 . p = F5(p) ) & ( p is negative & d1 = F1 . (the_argument_of p) implies F1 . p = F6(d1) ) & ( p is conjunctive & d1 = F1 . (the_left_argument_of p) & d2 = F1 . (the_right_argument_of p) implies F1 . p = F7(d1,d2) ) & ( p is universal & d1 = F1 . (the_scope_of p) implies F1 . p = F8(p,d1) ) ) ; ::_thesis: ( for F being Function of (QC-WFF F1()),F2() holds
( not x2 = F . F4() or ex p being Element of QC-WFF F1() ex d1, d2 being Element of F2() st
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) implies ( p is universal & d1 = F . (the_scope_of p) & not F . p = F8(p,d1) ) ) ) or x1 = x2 )
given F2 being Function of (QC-WFF F1()),F2() such that A4: x2 = F2 . F4() and
A5: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F2 . p = F3() ) & ( p is atomic implies F2 . p = F5(p) ) & ( p is negative & d1 = F2 . (the_argument_of p) implies F2 . p = F6(d1) ) & ( p is conjunctive & d1 = F2 . (the_left_argument_of p) & d2 = F2 . (the_right_argument_of p) implies F2 . p = F7(d1,d2) ) & ( p is universal & d1 = F2 . (the_scope_of p) implies F2 . p = F8(p,d1) ) ) ; ::_thesis: x1 = x2
 F1 = F2 from QC_LANG3:sch_1(A3, A5);
hence  x1 = x2 by A2, A4; ::_thesis: verum
end;

scheme :: QC_LANG3:sch 3
QCDResult9VERUM{ F1() ->  QC-alphabet , F2() ->  non empty set , F3( Element of QC-WFF F1()) ->  Element of F2(), F4() ->  Element of F2(), F5( Element of QC-WFF F1()) ->  Element of F2(), F6( Element of F2()) ->  Element of F2(), F7( Element of F2(), Element of F2()) ->  Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) ->  Element of F2() } :
 F3((VERUM F1())) = F4()
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F3(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F4() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) )
proof
 ex F being Function of (QC-WFF F1()),F2() st
( F3((VERUM F1())) = F . (VERUM F1()) & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F4() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) by A1;
hence  F3((VERUM F1())) = F4() ; ::_thesis: verum
end;

scheme :: QC_LANG3:sch 4
QCDResult9atomic{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4( Element of QC-WFF F1()) ->  Element of F2(), F5() ->  QC-formula of F1(), F6( Element of QC-WFF F1()) ->  Element of F2(), F7( Element of F2()) ->  Element of F2(), F8( Element of F2(), Element of F2()) ->  Element of F2(), F9( Element of QC-WFF F1(), Element of F2()) ->  Element of F2() } :
 F4(F5()) = F6(F5())
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F4(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F6(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F7(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F8(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F9(p,d1) ) ) ) ) ) and
A2: F5() is atomic
proof
 ex F being Function of (QC-WFF F1()),F2() st
( F4(F5()) = F . F5() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F6(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F7(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F8(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F9(p,d1) ) ) ) ) by A1;
hence  F4(F5()) = F6(F5()) by A2; ::_thesis: verum
end;

scheme :: QC_LANG3:sch 5
QCDResult9negative{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4() ->  QC-formula of F1(), F5( Element of QC-WFF F1()) ->  Element of F2(), F6( Element of F2()) ->  Element of F2(), F7( Element of F2(), Element of F2()) ->  Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) ->  Element of F2(), F9( Element of QC-WFF F1()) ->  Element of F2() } :
 F9(F4()) = F6(F9((the_argument_of F4())))
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F9(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) and
A2: F4() is negative
proof
consider F being Function of (QC-WFF F1()),F2() such that
A3: F9(F4()) = F . F4() and
A4: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) by A1;
 F . (the_argument_of F4()) = F9((the_argument_of F4())) by A1, A4;
hence  F9(F4()) = F6(F9((the_argument_of F4()))) by A2, A3, A4; ::_thesis: verum
end;

scheme :: QC_LANG3:sch 6
QCDResult9conjunctive{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4( Element of QC-WFF F1()) ->  Element of F2(), F5( Element of F2()) ->  Element of F2(), F6( Element of F2(), Element of F2()) ->  Element of F2(), F7( Element of QC-WFF F1(), Element of F2()) ->  Element of F2(), F8( Element of QC-WFF F1()) ->  Element of F2(), F9() ->  QC-formula of F1() } :
 for d1, d2 being Element of F2() st d1 = F8((the_left_argument_of F9())) & d2 = F8((the_right_argument_of F9())) holds
F8(F9()) = F6(d1,d2)
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F8(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F5(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F6(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F7(p,d1) ) ) ) ) ) and
A2: F9() is conjunctive
proof
consider F being Function of (QC-WFF F1()),F2() such that
A3: F8(F9()) = F . F9() and
A4: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F5(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F6(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F7(p,d1) ) ) by A1;
let d1, d2 be Element of F2(); ::_thesis: ( d1 = F8((the_left_argument_of F9())) & d2 = F8((the_right_argument_of F9())) implies F8(F9()) = F6(d1,d2) )
assume  ( d1 = F8((the_left_argument_of F9())) & d2 = F8((the_right_argument_of F9())) ) ; ::_thesis: F8(F9()) = F6(d1,d2)
then  ( F . (the_left_argument_of F9()) = d1 & F . (the_right_argument_of F9()) = d2 ) by A1, A4;
hence  F8(F9()) = F6(d1,d2) by A2, A3, A4; ::_thesis: verum
end;

scheme :: QC_LANG3:sch 7
QCDResult9universal{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4() ->  QC-formula of F1(), F5( Element of QC-WFF F1()) ->  Element of F2(), F6( Element of F2()) ->  Element of F2(), F7( Element of F2(), Element of F2()) ->  Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) ->  Element of F2(), F9( Element of QC-WFF F1()) ->  Element of F2() } :
 F9(F4()) = F8(F4(),F9((the_scope_of F4())))
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F9(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) and
A2: F4() is universal
proof
consider F being Function of (QC-WFF F1()),F2() such that
A3: F9(F4()) = F . F4() and
A4: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) by A1;
 F . (the_scope_of F4()) = F9((the_scope_of F4())) by A1, A4;
hence  F9(F4()) = F8(F4(),F9((the_scope_of F4()))) by A2, A3, A4; ::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: for P being QC-pred_symbol of A holds P is QC-pred_symbol of (the_arity_of P),A
let P be QC-pred_symbol of A; ::_thesis: P is QC-pred_symbol of (the_arity_of P),A
set k = the_arity_of P;
set QCP =  {  Q where Q is QC-pred_symbol of A : the_arity_of Q = the_arity_of P  }  ;
 P in  {  Q where Q is QC-pred_symbol of A : the_arity_of Q = the_arity_of P  }  ;
hence  P is QC-pred_symbol of (the_arity_of P),A ; ::_thesis: verum
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);
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 )  }  is Subset of V
proof
set A =  {  (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 )  }  c= V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V )  }  or x in V )
assume  x in  {  (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V )  }  ; ::_thesis: x in V
then  ex k being Element of NAT st
( l . k = x & 1 <= k & k <= len l & l . k in V ) ;
hence  x in V ; ::_thesis: verum
end;
hence   {  (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V )  }  is Subset of V ; ::_thesis: verum
end;
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 )  }  ;

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

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_=_H1(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_=_H2(p)_)_&_(_p_is_negative_&_d1_=_F_._(the_argument_of_p)_implies_F_._p_=_H4(d1)_)_&_(_p_is_conjunctive_&_d1_=_F_._(the_left_argument_of_p)_&_d2_=_F_._(the_right_argument_of_p)_implies_F_._p_=_H5(d1,d2)_)_&_(_p_is_universal_&_d1_=_F_._(the_scope_of_p)_implies_F_._p_=_H3(p,d1)_)_)_)_)_)
let A be QC-alphabet ; ::_thesis: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
deffunc H1( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H2( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H4( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H5( 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 = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) ::_thesis: verum
proof
let p be QC-formula of A; ::_thesis: for d being Subset of (bound_QC-variables A) holds
( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
let d be Subset of (bound_QC-variables A); ::_thesis: ( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) implies d = H1(p) )
proof
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;
given F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A2: d = F . p and
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 = H1(p)
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)}_)_)
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)} ) )
proof
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;
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)} ) )
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;
hence  d = H1(p) by A2, QC_LANG1:def_30; ::_thesis: verum
end;
end;

theorem Th3: :: QC_LANG3:3
for A being QC-alphabet holds still_not-bound_in (VERUM A) = {}
proof
let A be QC-alphabet ; ::_thesis: still_not-bound_in (VERUM A) = {}
deffunc H1( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H2( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H4( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H5( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $1 \/ $2;
A1: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) by Lm1;
thus H1( VERUM A) = {} (bound_QC-variables A) from QC_LANG3:sch_3(A1)
.= {} ; ::_thesis: verum
end;

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)
proof
let A be QC-alphabet ; ::_thesis: 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)
deffunc H1( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H2( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H4( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H5( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $1 \/ $2;
A1: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) by Lm1;
let p be QC-formula of A; ::_thesis: ( p is atomic implies still_not-bound_in p = still_not-bound_in (the_arguments_of p) )
assume A2: p is atomic ; ::_thesis: still_not-bound_in p = still_not-bound_in (the_arguments_of p)
thus  H1(p) = H2(p) from QC_LANG3:sch_4(A1, A2); ::_thesis: verum
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
proof
let k be Element of NAT ; ::_thesis: 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
let A be QC-alphabet ; ::_thesis: 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
let P be QC-pred_symbol of k,A; ::_thesis: for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l
let l be QC-variable_list of k,A; ::_thesis: still_not-bound_in (P ! l) = still_not-bound_in l
A1: P ! l is atomic by QC_LANG1:def_18;
then  the_arguments_of (P ! l) = l by QC_LANG1:def_23;
hence  still_not-bound_in (P ! l) = still_not-bound_in l by A1, Th4; ::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: 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)
deffunc H1( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H2( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H4( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H5( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $1 \/ $2;
A1: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) by Lm1;
let p be QC-formula of A; ::_thesis: ( p is negative implies still_not-bound_in p = still_not-bound_in (the_argument_of p) )
assume A2: p is negative ; ::_thesis: still_not-bound_in p = still_not-bound_in (the_argument_of p)
thus  H1(p) = H4(H1( the_argument_of p)) from QC_LANG3:sch_5(A1, A2); ::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: for p being QC-formula of A holds still_not-bound_in ('not' p) = still_not-bound_in p
let p be QC-formula of A; ::_thesis: still_not-bound_in ('not' p) = still_not-bound_in p
A1: 'not' p is negative by QC_LANG1:def_19;
then  the_argument_of ('not' p) = p by QC_LANG1:def_24;
hence  still_not-bound_in ('not' p) = still_not-bound_in p by A1, Th6; ::_thesis: verum
end;

theorem Th8: :: QC_LANG3:8
for A being QC-alphabet holds still_not-bound_in (FALSUM A) = {}
proof
let A be QC-alphabet ; ::_thesis: still_not-bound_in (FALSUM A) = {}
still_not-bound_in (FALSUM A) = still_not-bound_in ('not' (VERUM A)) by QC_LANG2:def_1
.= still_not-bound_in (VERUM A) by Th7
.= {} by Th3 ;
hence  still_not-bound_in (FALSUM A) = {} ; ::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
deffunc H1( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H2( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H4( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H5( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $1 \/ $2;
A1: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) by Lm1;
let p be QC-formula of A; ::_thesis: ( p is conjunctive implies still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) )
assume A2: p is conjunctive ; ::_thesis: still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))
 for d1, d2 being Subset of (bound_QC-variables A) st d1 = H1( the_left_argument_of p) & d2 = H1( the_right_argument_of p) holds
H1(p) = H5(d1,d2) from QC_LANG3:sch_6(A1, A2);
hence  still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) ; ::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let p, q be QC-formula of A; ::_thesis: still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
set pq = p '&' q;
A1: p '&' q is conjunctive by QC_LANG1:def_20;
then  ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def_25, QC_LANG1:def_26;
hence  still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th9; ::_thesis: verum
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)}
proof
let A be QC-alphabet ; ::_thesis: 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)}
deffunc H1( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H2( Element of QC-WFF A) ->  Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H4( Subset of (bound_QC-variables A)) ->  Subset of (bound_QC-variables A) = $1;
deffunc H5( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) ->  Element of bool (bound_QC-variables A) = $1 \/ $2;
A1: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) by Lm1;
let p be QC-formula of A; ::_thesis: ( p is universal implies still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)} )
assume A2: p is universal ; ::_thesis: still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}
thus  H1(p) = H3(p,H1( the_scope_of p)) from QC_LANG3:sch_7(A1, A2); ::_thesis: verum
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}
proof
let A be QC-alphabet ; ::_thesis: 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}
let x be bound_QC-variable of A; ::_thesis: for p being QC-formula of A holds still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x}
let p be QC-formula of A; ::_thesis: still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x}
set a = All (x,p);
A1: All (x,p) is universal by QC_LANG1:def_21;
then  ( the_scope_of (All (x,p)) = p & bound_in (All (x,p)) = x ) by QC_LANG1:def_27, QC_LANG1:def_28;
hence  still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by A1, Th11; ::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p be QC-formula of A; ::_thesis: ( p is disjunctive implies still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p)) )
set p1 = the_left_disjunct_of p;
set p2 = the_right_disjunct_of p;
assume  p is disjunctive ; ::_thesis: still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p))
then  p = (the_left_disjunct_of p) 'or' (the_right_disjunct_of p) by QC_LANG2:37;
then  p = 'not' (('not' (the_left_disjunct_of p)) '&' ('not' (the_right_disjunct_of p))) by QC_LANG2:def_3;
then  still_not-bound_in p = still_not-bound_in (('not' (the_left_disjunct_of p)) '&' ('not' (the_right_disjunct_of p))) by Th7
.= (still_not-bound_in ('not' (the_left_disjunct_of p))) \/ (still_not-bound_in ('not' (the_right_disjunct_of p))) by Th10
.= (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in ('not' (the_right_disjunct_of p))) by Th7
.= (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p)) by Th7 ;
hence  still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p)) ; ::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let p, q be QC-formula of A; ::_thesis: still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
A1: the_right_disjunct_of (p 'or' q) = q by QC_LANG2:29;
 ( p 'or' q is disjunctive & the_left_disjunct_of (p 'or' q) = p ) by QC_LANG2:29, QC_LANG2:def_10;
hence  still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th13; ::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p be QC-formula of A; ::_thesis: ( p is conditional implies still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p)) )
set p1 = the_antecedent_of p;
set p2 = the_consequent_of p;
assume  p is conditional ; ::_thesis: still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p))
then  p = (the_antecedent_of p) => (the_consequent_of p) by QC_LANG2:38;
then  p = 'not' ((the_antecedent_of p) '&' ('not' (the_consequent_of p))) by QC_LANG2:def_2;
then  still_not-bound_in p = still_not-bound_in ((the_antecedent_of p) '&' ('not' (the_consequent_of p))) by Th7
.= (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in ('not' (the_consequent_of p))) by Th10
.= (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p)) by Th7 ;
hence  still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p)) ; ::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let p, q be QC-formula of A; ::_thesis: still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q)
A1: the_consequent_of (p => q) = q by QC_LANG2:30;
 ( p => q is conditional & the_antecedent_of (p => q) = p ) by QC_LANG2:30, QC_LANG2:def_11;
hence  still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th15; ::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p be QC-formula of A; ::_thesis: ( p is biconditional implies still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p)) )
set p1 = the_left_side_of p;
set p2 = the_right_side_of p;
assume  p is biconditional ; ::_thesis: still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))
then  p = (the_left_side_of p) <=> (the_right_side_of p) by QC_LANG2:39;
then  p = ((the_left_side_of p) => (the_right_side_of p)) '&' ((the_right_side_of p) => (the_left_side_of p)) by QC_LANG2:def_4;
then  still_not-bound_in p = (still_not-bound_in ((the_left_side_of p) => (the_right_side_of p))) \/ (still_not-bound_in ((the_right_side_of p) => (the_left_side_of p))) by Th10
.= ((still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))) \/ (still_not-bound_in ((the_right_side_of p) => (the_left_side_of p))) by Th16
.= ((still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))) \/ ((still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))) by Th16
.= (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p)) ;
hence  still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p)) ; ::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let p, q be QC-formula of A; ::_thesis: still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q)
A1: the_right_side_of (p <=> q) = q by QC_LANG2:31;
 ( p <=> q is biconditional & the_left_side_of (p <=> q) = p ) by QC_LANG2:31, QC_LANG2:def_12;
hence  still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th17; ::_thesis: verum
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}
proof
let A be QC-alphabet ; ::_thesis: 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}
let x be bound_QC-variable of A; ::_thesis: for p being QC-formula of A holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}
let p be QC-formula of A; ::_thesis: still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}
 Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def_5;
hence  still_not-bound_in (Ex (x,p)) = still_not-bound_in (All (x,('not' p))) by Th7
.= (still_not-bound_in ('not' p)) \ {x} by Th12
.= (still_not-bound_in p) \ {x} by Th7 ;
::_thesis: verum
end;

theorem :: QC_LANG3:20
for A being QC-alphabet holds
( VERUM A is closed & FALSUM A is closed )
proof
let A be QC-alphabet ; ::_thesis: ( VERUM A is closed & FALSUM A is closed )
 ( still_not-bound_in (VERUM A) = {} & still_not-bound_in (FALSUM A) = {} ) by Th3, Th8;
hence  ( VERUM A is closed & FALSUM A is closed ) by QC_LANG1:def_31; ::_thesis: verum
end;

theorem Th21: :: QC_LANG3:21
for A being QC-alphabet
for p being QC-formula of A holds
( p is closed iff 'not' p is closed )
proof
let A be QC-alphabet ; ::_thesis: for p being QC-formula of A holds
( p is closed iff 'not' p is closed )
let p be QC-formula of A; ::_thesis: ( p is closed iff 'not' p is closed )
thus  ( p is closed implies 'not' p is closed ) ::_thesis: ( 'not' p is closed implies p is closed )
proof
assume  still_not-bound_in p = {} ; :: according to QC_LANG1:def_31 ::_thesis: 'not' p is closed
hence  still_not-bound_in ('not' p) = {} by Th7; :: according to QC_LANG1:def_31 ::_thesis: verum
end;
assume  still_not-bound_in ('not' p) = {} ; :: according to QC_LANG1:def_31 ::_thesis: p is closed
hence  still_not-bound_in p = {} by Th7; :: according to QC_LANG1:def_31 ::_thesis: verum
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 )
proof
let A be QC-alphabet ; ::_thesis: for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p '&' q is closed )
let p, q be QC-formula of A; ::_thesis: ( ( p is closed & q is closed ) iff p '&' q is closed )
thus  ( p is closed & q is closed implies p '&' q is closed ) ::_thesis: ( p '&' q is closed implies ( p is closed & q is closed ) )
proof
assume  ( still_not-bound_in p = {} & still_not-bound_in q = {} ) ; :: according to QC_LANG1:def_31 ::_thesis: p '&' q is closed
then  (still_not-bound_in p) \/ (still_not-bound_in q) = {} ;
hence  still_not-bound_in (p '&' q) = {} by Th10; :: according to QC_LANG1:def_31 ::_thesis: verum
end;
assume A1: still_not-bound_in (p '&' q) = {} ; :: according to QC_LANG1:def_31 ::_thesis: ( p is closed & q is closed )
 still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by Th10;
hence  ( still_not-bound_in p = {} & still_not-bound_in q = {} ) by A1, XBOOLE_1:15; :: according to QC_LANG1:def_31 ::_thesis: verum
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} )
proof
let A be QC-alphabet ; ::_thesis: 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} )
let x be bound_QC-variable of A; ::_thesis: for p being QC-formula of A holds
( All (x,p) is closed iff still_not-bound_in p c= {x} )
let p be QC-formula of A; ::_thesis: ( All (x,p) is closed iff still_not-bound_in p c= {x} )
thus  ( All (x,p) is closed implies still_not-bound_in p c= {x} ) ::_thesis: ( still_not-bound_in p c= {x} implies All (x,p) is closed )
proof
assume  still_not-bound_in (All (x,p)) = {} ; :: according to QC_LANG1:def_31 ::_thesis: still_not-bound_in p c= {x}
then  {} = (still_not-bound_in p) \ {x} by Th12;
hence  still_not-bound_in p c= {x} by XBOOLE_1:37; ::_thesis: verum
end;
assume  still_not-bound_in p c= {x} ; ::_thesis: All (x,p) is closed
then  {} = (still_not-bound_in p) \ {x} by XBOOLE_1:37;
hence  still_not-bound_in (All (x,p)) = {} by Th12; :: according to QC_LANG1:def_31 ::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: 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
let x be bound_QC-variable of A; ::_thesis: for p being QC-formula of A st p is closed holds
All (x,p) is closed
let p be QC-formula of A; ::_thesis: ( p is closed implies All (x,p) is closed )
assume  still_not-bound_in p = {} ; :: according to QC_LANG1:def_31 ::_thesis: All (x,p) is closed
then  still_not-bound_in p c= {x} by XBOOLE_1:2;
hence  All (x,p) is closed by Th23; ::_thesis: verum
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 )
proof
let A be QC-alphabet ; ::_thesis: for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p 'or' q is closed )
let p, q be QC-formula of A; ::_thesis: ( ( p is closed & q is closed ) iff p 'or' q is closed )
A1: p 'or' q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def_3;
 ( ('not' p) '&' ('not' q) is closed iff ( 'not' p is closed & 'not' q is closed ) ) by Th22;
hence  ( ( p is closed & q is closed ) iff p 'or' q is closed ) by A1, Th21; ::_thesis: verum
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 )
proof
let A be QC-alphabet ; ::_thesis: for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p => q is closed )
let p, q be QC-formula of A; ::_thesis: ( ( p is closed & q is closed ) iff p => q is closed )
A1: p => q = 'not' (p '&' ('not' q)) by QC_LANG2:def_2;
 ( p '&' ('not' q) is closed iff ( p is closed & 'not' q is closed ) ) by Th22;
hence  ( ( p is closed & q is closed ) iff p => q is closed ) by A1, Th21; ::_thesis: verum
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 )
proof
let A be QC-alphabet ; ::_thesis: for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p <=> q is closed )
let p, q be QC-formula of A; ::_thesis: ( ( p is closed & q is closed ) iff p <=> q is closed )
 p <=> q = (p => q) '&' (q => p) by QC_LANG2:def_4;
then  ( p <=> q is closed iff ( p => q is closed & q => p is closed ) ) by Th22;
hence  ( ( p is closed & q is closed ) iff p <=> q is closed ) by Th26; ::_thesis: verum
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} )
proof
let A be QC-alphabet ; ::_thesis: 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} )
let x be bound_QC-variable of A; ::_thesis: for p being QC-formula of A holds
( Ex (x,p) is closed iff still_not-bound_in p c= {x} )
let p be QC-formula of A; ::_thesis: ( Ex (x,p) is closed iff still_not-bound_in p c= {x} )
thus  ( Ex (x,p) is closed implies still_not-bound_in p c= {x} ) ::_thesis: ( still_not-bound_in p c= {x} implies Ex (x,p) is closed )
proof
assume  still_not-bound_in (Ex (x,p)) = {} ; :: according to QC_LANG1:def_31 ::_thesis: still_not-bound_in p c= {x}
then  {} = (still_not-bound_in p) \ {x} by Th19;
hence  still_not-bound_in p c= {x} by XBOOLE_1:37; ::_thesis: verum
end;
assume  still_not-bound_in p c= {x} ; ::_thesis: Ex (x,p) is closed
then  {} = (still_not-bound_in p) \ {x} by XBOOLE_1:37;
hence  still_not-bound_in (Ex (x,p)) = {} by Th19; :: according to QC_LANG1:def_31 ::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: 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
let x be bound_QC-variable of A; ::_thesis: for p being QC-formula of A st p is closed holds
Ex (x,p) is closed
let p be QC-formula of A; ::_thesis: ( p is closed implies Ex (x,p) is closed )
assume  still_not-bound_in p = {} ; :: according to QC_LANG1:def_31 ::_thesis: Ex (x,p) is closed
then  still_not-bound_in p c= {x} by XBOOLE_1:2;
hence  Ex (x,p) is closed by Th28; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let s be QC-symbol of A;
func x. s ->  bound_QC-variable of A equals :: QC_LANG3:def 2
[4,s];
coherence
 [4,s] is bound_QC-variable of A
proof
 4 in {4} by TARSKI:def_1;
hence  [4,s] is bound_QC-variable of A by ZFMISC_1:def_2; ::_thesis: verum
end;
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];

theorem :: QC_LANG3:30
for A being QC-alphabet
for x being bound_QC-variable of A ex t being QC-symbol of A st x. t = x
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A ex t being QC-symbol of A st x. t = x
let x be bound_QC-variable of A; ::_thesis: ex t being QC-symbol of A st x. t = x
consider i, t being set  such that
A1: i in {4} and
A2: t in QC-symbols A and
A3: [i,t] = x by ZFMISC_1:def_2;
reconsider t = t as QC-symbol of A by A2;
take  t ; ::_thesis: x. t = x
thus  x. t = x by A1, A3, TARSKI:def_1; ::_thesis: verum
end;

definition
let A be QC-alphabet ;
let k be Element of NAT ;
funcA a. k ->  free_QC-variable of A equals :: QC_LANG3:def 3
[6,k];
coherence
 [6,k] is free_QC-variable of A
proof
 6 in {6} by TARSKI:def_1;
hence  [6,k] is free_QC-variable of A by ZFMISC_1:def_2; ::_thesis: verum
end;
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];

theorem :: QC_LANG3:31
for A being QC-alphabet
for a being free_QC-variable of A ex i being Element of NAT st A a. i = a
proof
let A be QC-alphabet ; ::_thesis: for a being free_QC-variable of A ex i being Element of NAT st A a. i = a
let a be free_QC-variable of A; ::_thesis: ex i being Element of NAT st A a. i = a
consider x, y being set  such that
A1: x in {6} and
A2: y in NAT and
A3: [x,y] = a by ZFMISC_1:def_2;
reconsider i = y as Element of NAT by A2;
take  i ; ::_thesis: A a. i = a
thus  A a. i = a by A1, A3, TARSKI:def_1; ::_thesis: verum
end;

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
proof
let A be QC-alphabet ; ::_thesis: for c being Element of fixed_QC-variables A
for a being Element of free_QC-variables A holds c <> a
let c be Element of fixed_QC-variables A; ::_thesis: for a being Element of free_QC-variables A holds c <> a
let a be Element of free_QC-variables A; ::_thesis: c <> a
consider a1, a2 being set  such that
A1: a1 in {6} and
 a2 in NAT and
A2: a = [a1,a2] by ZFMISC_1:def_2;
consider c1, c2 being set  such that
A3: c1 in {5} and
 c2 in QC-symbols A and
A4: c = [c1,c2] by ZFMISC_1:def_2;
A5: c1 = 5 by A3, TARSKI:def_1;
 a1 = 6 by A1, TARSKI:def_1;
hence  c <> a by A2, A4, A5, XTUPLE_0:1; ::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: for c being Element of fixed_QC-variables A
for x being Element of bound_QC-variables A holds c <> x
let c be Element of fixed_QC-variables A; ::_thesis: for x being Element of bound_QC-variables A holds c <> x
let x be Element of bound_QC-variables A; ::_thesis: c <> x
consider x1, x2 being set  such that
A1: x1 in {4} and
 x2 in QC-symbols A and
A2: x = [x1,x2] by ZFMISC_1:def_2;
consider c1, c2 being set  such that
A3: c1 in {5} and
 c2 in QC-symbols A and
A4: c = [c1,c2] by ZFMISC_1:def_2;
A5: c1 = 5 by A3, TARSKI:def_1;
 x1 = 4 by A1, TARSKI:def_1;
hence  c <> x by A2, A4, A5, XTUPLE_0:1; ::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: for a being Element of free_QC-variables A
for x being Element of bound_QC-variables A holds a <> x
let a be Element of free_QC-variables A; ::_thesis: for x being Element of bound_QC-variables A holds a <> x
let x be Element of bound_QC-variables A; ::_thesis: a <> x
consider x1, x2 being set  such that
A1: x1 in {4} and
 x2 in QC-symbols A and
A2: x = [x1,x2] by ZFMISC_1:def_2;
consider a1, a2 being set  such that
A3: a1 in {6} and
 a2 in NAT and
A4: a = [a1,a2] by ZFMISC_1:def_2;
A5: a1 = 6 by A3, TARSKI:def_1;
 x1 = 4 by A1, TARSKI:def_1;
hence  a <> x by A2, A4, A5, XTUPLE_0:1; ::_thesis: verum
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;
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
existence
ex b1 being Subset of V ex F being Function of (QC-WFF A),(bool V) st
( b1 = 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 b1, b2 being Subset of V st ex F being Function of (QC-WFF A),(bool V) st
( b1 = 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
( b2 = 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
b1 = b2;
proof
deffunc H1( Element of QC-WFF A, Subset of V) ->  Subset of V = $2;
deffunc H2( Subset of V, Subset of V) ->  Element of bool V = $1 \/ $2;
deffunc H3( Subset of V) ->  Subset of V = $1;
deffunc H4( Element of QC-WFF A) ->  Subset of V = variables_in ((the_arguments_of $1),V);
thus  ( ex d being Subset of V ex F being Function of (QC-WFF A),(bool V) st
( d = 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 = H4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H2(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H1(p,d1) ) ) ) ) & ( for x1, x2 being Subset of V st ex F being Function of (QC-WFF A),(bool V) st
( x1 = 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 = H4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H2(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H1(p,d1) ) ) ) ) & ex F being Function of (QC-WFF A),(bool V) st
( x2 = 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 = H4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H2(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H1(p,d1) ) ) ) ) holds
x1 = x2 ) ) from QC_LANG3:sch_2(); ::_thesis: verum
end;
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 b4 being Subset of V holds
( b4 = Vars (p,V) iff ex F being Function of (QC-WFF A),(bool V) st
( b4 = 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 ) ) ) ) );

Lm2: now__::_thesis:_for_A_being_QC-alphabet_
for_V_being_non_empty_Subset_of_(QC-variables_A)_holds_
(_H1(_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 A be QC-alphabet ; ::_thesis: for V being non empty Subset of (QC-variables A) holds
( H1( 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: ( H1( 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 H1( Element of QC-WFF A) ->  Subset of V = Vars ($1,V);
deffunc H2( Element of QC-WFF A) ->  Subset of V = variables_in ((the_arguments_of $1),V);
deffunc H3( Subset of V) ->  Subset of V = $1;
deffunc H4( Subset of V, Subset of V) ->  Element of bool V = $1 \/ $2;
deffunc H5( 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 = H1(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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H4(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H5(p,d1) ) ) ) ) ) by Def4;
thus H1( 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) ) )
proof
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  H1(p) = H2(p) from QC_LANG3:sch_4(A1, A2); ::_thesis: verum
end;
thus  for p being Element of QC-WFF A st p is negative holds
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
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  H1(p) = H3(H1( the_argument_of p)) from QC_LANG3:sch_5(A1, A3); ::_thesis: verum
end;
thus  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)) ::_thesis: for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V)
proof
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 = H1( the_left_argument_of p) & d2 = H1( the_right_argument_of p) holds
H1(p) = H4(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;
thus  for p being Element of QC-WFF A st p is universal holds
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  H1(p) = H5(p,H1( the_scope_of p)) from QC_LANG3:sch_7(A1, A5); ::_thesis: verum
end;
end;

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;

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 )  }  )
proof
let A be QC-alphabet ; ::_thesis: 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 )  }  )
let p be Element of QC-WFF A; ::_thesis: 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 )  }  )
let V be non empty Subset of (QC-variables A); ::_thesis: ( p is atomic implies ( 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 )  }  ) )
assume  p is atomic ; ::_thesis: ( 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 )  }  )
hence  Vars (p,V) = variables_in ((the_arguments_of p),V) by Lm2; ::_thesis: 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 )  }
hence  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 )  }  ; ::_thesis: verum
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 )  }  )
proof
let k be Element of NAT ; ::_thesis: 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 )  }  )
let A be QC-alphabet ; ::_thesis: 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 )  }  )
let V be non empty Subset of (QC-variables A); ::_thesis: 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 )  }  )
let P be QC-pred_symbol of k,A; ::_thesis: 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 )  }  )
let l be QC-variable_list of k,A; ::_thesis: ( 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 )  }  )
A1: P ! l is atomic by QC_LANG1:def_18;
then  the_arguments_of (P ! l) = l by QC_LANG1:def_23;
hence  ( 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 )  }  ) by A1, Th36; ::_thesis: verum
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;

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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let p be Element of QC-WFF A; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars (('not' p),V) = Vars (p,V)
let V be non empty Subset of (QC-variables A); ::_thesis: Vars (('not' p),V) = Vars (p,V)
set 9p = 'not' p;
A1: 'not' p is negative by QC_LANG1:def_19;
then  the_argument_of ('not' p) = p by QC_LANG1:def_24;
hence  Vars (('not' p),V) = Vars (p,V) by A1, Lm2; ::_thesis: verum
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) = {}
proof
let A be QC-alphabet ; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars ((FALSUM A),V) = {}
let V be non empty Subset of (QC-variables A); ::_thesis: Vars ((FALSUM A),V) = {}
 FALSUM A = 'not' (VERUM A) by QC_LANG2:def_1;
hence  Vars ((FALSUM A),V) = Vars ((VERUM A),V) by Th39
.= {} by Lm2 ;
::_thesis: verum
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;

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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p, q be Element of QC-WFF A; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V))
let V be non empty Subset of (QC-variables A); ::_thesis: Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V))
set pq = p '&' q;
A1: p '&' q is conjunctive by QC_LANG1:def_20;
then  ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def_25, QC_LANG1:def_26;
hence  Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V)) by A1, Lm2; ::_thesis: verum
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;

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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let x be bound_QC-variable of A; ::_thesis: 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)
let p be Element of QC-WFF A; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars ((All (x,p)),V) = Vars (p,V)
let V be non empty Subset of (QC-variables A); ::_thesis: Vars ((All (x,p)),V) = Vars (p,V)
A1: All (x,p) is universal by QC_LANG1:def_21;
then  the_scope_of (All (x,p)) = p by QC_LANG1:def_28;
hence  Vars ((All (x,p)),V) = Vars (p,V) by A1, Lm2; ::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p be Element of QC-WFF A; ::_thesis: 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))
let V be non empty Subset of (QC-variables A); ::_thesis: ( p is disjunctive implies Vars (p,V) = (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V)) )
set p1 = the_left_disjunct_of p;
set p2 = the_right_disjunct_of p;
assume  p is disjunctive ; ::_thesis: Vars (p,V) = (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V))
then  p = (the_left_disjunct_of p) 'or' (the_right_disjunct_of p) by QC_LANG2:37;
then  p = 'not' (('not' (the_left_disjunct_of p)) '&' ('not' (the_right_disjunct_of p))) by QC_LANG2:def_3;
hence  Vars (p,V) = Vars ((('not' (the_left_disjunct_of p)) '&' ('not' (the_right_disjunct_of p))),V) by Th39
.= (Vars (('not' (the_left_disjunct_of p)),V)) \/ (Vars (('not' (the_right_disjunct_of p)),V)) by Th42
.= (Vars ((the_left_disjunct_of p),V)) \/ (Vars (('not' (the_right_disjunct_of p)),V)) by Th39
.= (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V)) by Th39 ;
::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p, q be Element of QC-WFF A; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))
let V be non empty Subset of (QC-variables A); ::_thesis: Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))
A1: the_right_disjunct_of (p 'or' q) = q by QC_LANG2:29;
 ( p 'or' q is disjunctive & the_left_disjunct_of (p 'or' q) = p ) by QC_LANG2:29, QC_LANG2:def_10;
hence  Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V)) by A1, Th45; ::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p be Element of QC-WFF A; ::_thesis: 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))
let V be non empty Subset of (QC-variables A); ::_thesis: ( p is conditional implies Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V)) )
set p1 = the_antecedent_of p;
set p2 = the_consequent_of p;
assume  p is conditional ; ::_thesis: Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V))
then  p = (the_antecedent_of p) => (the_consequent_of p) by QC_LANG2:38;
then  p = 'not' ((the_antecedent_of p) '&' ('not' (the_consequent_of p))) by QC_LANG2:def_2;
hence  Vars (p,V) = Vars (((the_antecedent_of p) '&' ('not' (the_consequent_of p))),V) by Th39
.= (Vars ((the_antecedent_of p),V)) \/ (Vars (('not' (the_consequent_of p)),V)) by Th42
.= (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V)) by Th39 ;
::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p, q be Element of QC-WFF A; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars ((p => q),V) = (Vars (p,V)) \/ (Vars (q,V))
let V be non empty Subset of (QC-variables A); ::_thesis: Vars ((p => q),V) = (Vars (p,V)) \/ (Vars (q,V))
A1: the_consequent_of (p => q) = q by QC_LANG2:30;
 ( p => q is conditional & the_antecedent_of (p => q) = p ) by QC_LANG2:30, QC_LANG2:def_11;
hence  Vars ((p => q),V) = (Vars (p,V)) \/ (Vars (q,V)) by A1, Th47; ::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p be Element of QC-WFF A; ::_thesis: 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))
let V be non empty Subset of (QC-variables A); ::_thesis: ( p is biconditional implies Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V)) )
set p1 = the_left_side_of p;
set p2 = the_right_side_of p;
assume  p is biconditional ; ::_thesis: Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))
then  p = (the_left_side_of p) <=> (the_right_side_of p) by QC_LANG2:39;
then  p = ((the_left_side_of p) => (the_right_side_of p)) '&' ((the_right_side_of p) => (the_left_side_of p)) by QC_LANG2:def_4;
hence  Vars (p,V) = (Vars (((the_left_side_of p) => (the_right_side_of p)),V)) \/ (Vars (((the_right_side_of p) => (the_left_side_of p)),V)) by Th42
.= ((Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))) \/ (Vars (((the_right_side_of p) => (the_left_side_of p)),V)) by Th48
.= ((Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))) \/ ((Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))) by Th48
.= (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V)) ;
::_thesis: verum
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))
proof
let A be QC-alphabet ; ::_thesis: 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))
let p, q be Element of QC-WFF A; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))
let V be non empty Subset of (QC-variables A); ::_thesis: Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))
A1: the_right_side_of (p <=> q) = q by QC_LANG2:31;
 ( p <=> q is biconditional & the_left_side_of (p <=> q) = p ) by QC_LANG2:31, QC_LANG2:def_12;
hence  Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V)) by A1, Th49; ::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let p be Element of QC-WFF A; ::_thesis: 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)
let V be non empty Subset of (QC-variables A); ::_thesis: ( p is existential implies Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V) )
set p1 = the_argument_of (the_scope_of (the_argument_of p));
set x = bound_in (the_argument_of p);
assume  p is existential ; ::_thesis: Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)
then  p = Ex ((bound_in (the_argument_of p)),(the_argument_of (the_scope_of (the_argument_of p)))) by QC_LANG2:40;
then  p = 'not' (All ((bound_in (the_argument_of p)),('not' (the_argument_of (the_scope_of (the_argument_of p)))))) by QC_LANG2:def_5;
then  Vars (p,V) = Vars ((All ((bound_in (the_argument_of p)),('not' (the_argument_of (the_scope_of (the_argument_of p)))))),V) by Th39
.= Vars (('not' (the_argument_of (the_scope_of (the_argument_of p)))),V) by Th44
.= Vars ((the_argument_of (the_scope_of (the_argument_of p))),V) by Th39 ;
hence  Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V) ; ::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: 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)
let x be bound_QC-variable of A; ::_thesis: 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)
let p be Element of QC-WFF A; ::_thesis: for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V)
let V be non empty Subset of (QC-variables A); ::_thesis: Vars ((Ex (x,p)),V) = Vars (p,V)
 Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def_5;
hence  Vars ((Ex (x,p)),V) = Vars ((All (x,('not' p))),V) by Th39
.= Vars (('not' p),V) by Th44
.= Vars (p,V) by Th39 ;
::_thesis: verum
end;

definition
let A be QC-alphabet ;
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
coherence
Vars (p,(free_QC-variables A)) is Subset of (free_QC-variables A);
;
end;

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

theorem :: QC_LANG3:53
for A being QC-alphabet holds Free (VERUM A) = {} by Lm2;

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;

theorem :: QC_LANG3:55
for A being QC-alphabet
for p being Element of QC-WFF A holds Free ('not' p) = Free p by Th39;

theorem :: QC_LANG3:56
for A being QC-alphabet holds Free (FALSUM A) = {} by Th40;

theorem :: QC_LANG3:57
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Free (p '&' q) = (Free p) \/ (Free q) by Th42;

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;

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)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds Free (p 'or' q) = (Free p) \/ (Free q)
let p, q be Element of QC-WFF A; ::_thesis: Free (p 'or' q) = (Free p) \/ (Free q)
 p 'or' q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def_3;
hence  Free (p 'or' q) = Free (('not' p) '&' ('not' q)) by Th39
.= (Free ('not' p)) \/ (Free ('not' q)) by Th42
.= (Free p) \/ (Free ('not' q)) by Th39
.= (Free p) \/ (Free q) by Th39 ;
::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds Free (p => q) = (Free p) \/ (Free q)
let p, q be Element of QC-WFF A; ::_thesis: Free (p => q) = (Free p) \/ (Free q)
 p => q = 'not' (p '&' ('not' q)) by QC_LANG2:def_2;
hence  Free (p => q) = Free (p '&' ('not' q)) by Th39
.= (Free p) \/ (Free ('not' q)) by Th42
.= (Free p) \/ (Free q) by Th39 ;
::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds Free (p <=> q) = (Free p) \/ (Free q)
let p, q be Element of QC-WFF A; ::_thesis: Free (p <=> q) = (Free p) \/ (Free q)
 p <=> q = (p => q) '&' (q => p) by QC_LANG2:def_4;
hence  Free (p <=> q) = (Free (p => q)) \/ (Free (q => p)) by Th42
.= ((Free p) \/ (Free q)) \/ (Free (q => p)) by Th60
.= ((Free p) \/ (Free q)) \/ ((Free p) \/ (Free q)) by Th60
.= (Free p) \/ (Free q) ;
::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p
let p be Element of QC-WFF A; ::_thesis: Free (Ex (x,p)) = Free p
 Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def_5;
hence  Free (Ex (x,p)) = Free (All (x,('not' p))) by Th39
.= Free ('not' p) by Th44
.= Free p by Th39 ;
::_thesis: verum
end;

definition
let A be QC-alphabet ;
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
coherence
Vars (p,(fixed_QC-variables A)) is Subset of (fixed_QC-variables A);
;
end;

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

theorem :: QC_LANG3:63
for A being QC-alphabet holds Fixed (VERUM A) = {} by Lm2;

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;

theorem :: QC_LANG3:65
for A being QC-alphabet
for p being Element of QC-WFF A holds Fixed ('not' p) = Fixed p by Th39;

theorem :: QC_LANG3:66
for A being QC-alphabet holds Fixed (FALSUM A) = {}
proof
let A be QC-alphabet ; ::_thesis: Fixed (FALSUM A) = {}
thus  Fixed (FALSUM A) = Fixed ('not' (VERUM A)) by QC_LANG2:def_1
.= Fixed (VERUM A) by Th39
.= {} by Lm2 ; ::_thesis: verum
end;

theorem :: QC_LANG3:67
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Fixed (p '&' q) = (Fixed p) \/ (Fixed q) by Th42;

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;

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)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)
let p, q be Element of QC-WFF A; ::_thesis: Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)
 p 'or' q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def_3;
hence  Fixed (p 'or' q) = Fixed (('not' p) '&' ('not' q)) by Th39
.= (Fixed ('not' p)) \/ (Fixed ('not' q)) by Th42
.= (Fixed p) \/ (Fixed ('not' q)) by Th39
.= (Fixed p) \/ (Fixed q) by Th39 ;
::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds Fixed (p => q) = (Fixed p) \/ (Fixed q)
let p, q be Element of QC-WFF A; ::_thesis: Fixed (p => q) = (Fixed p) \/ (Fixed q)
 p => q = 'not' (p '&' ('not' q)) by QC_LANG2:def_2;
hence  Fixed (p => q) = Fixed (p '&' ('not' q)) by Th39
.= (Fixed p) \/ (Fixed ('not' q)) by Th42
.= (Fixed p) \/ (Fixed q) by Th39 ;
::_thesis: verum
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)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds Fixed (p <=> q) = (Fixed p) \/ (Fixed q)
let p, q be Element of QC-WFF A; ::_thesis: Fixed (p <=> q) = (Fixed p) \/ (Fixed q)
 p <=> q = (p => q) '&' (q => p) by QC_LANG2:def_4;
hence  Fixed (p <=> q) = (Fixed (p => q)) \/ (Fixed (q => p)) by Th42
.= ((Fixed p) \/ (Fixed q)) \/ (Fixed (q => p)) by Th70
.= ((Fixed p) \/ (Fixed q)) \/ ((Fixed q) \/ (Fixed p)) by Th70
.= (Fixed p) \/ (Fixed q) ;
::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Fixed (Ex (x,p)) = Fixed p
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A holds Fixed (Ex (x,p)) = Fixed p
let p be Element of QC-WFF A; ::_thesis: Fixed (Ex (x,p)) = Fixed p
 Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def_5;
hence  Fixed (Ex (x,p)) = Fixed (All (x,('not' p))) by Th39
.= Fixed ('not' p) by Th44
.= Fixed p by Th39 ;
::_thesis: verum
end;