:: QC_LANG3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: QC_LANG3:sch 1
QCFuncUniq{ F1() -> non empty set , F2() -> Function of QC-WFF ,F1(), F3() -> Function of QC-WFF ,F1(), F4() -> Element of F1(), F5( set ) -> Element of F1(), F6( set ) -> Element of F1(), F7( set , set ) -> Element of F1(), F8( set , set ) -> Element of F1() } :
F2() = F3()
provided
A1: for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F2() . p = F4() ) & ( 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) ) ) and
A2: for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F3() . p = F4() ) & ( p is atomic implies F3() . p = F5(p) ) & ( p is negative & d1 = F3() . (the_argument_of p) implies F3() . p = F6(d1) ) & ( p is conjunctive & d1 = F3() . (the_left_argument_of p) & d2 = F3() . (the_right_argument_of p) implies F3() . p = F7(d1,d2) ) & ( p is universal & d1 = F3() . (the_scope_of p) implies F3() . p = F8(p,d1) ) )
proof end;

scheme :: QC_LANG3:sch 2
QCDefD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of QC-WFF , F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1() } :
( ex d being Element of F1() ex F being Function of QC-WFF ,F1() st
( d = F . F3() & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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) ) ) ) ) & ( for x1, x2 being Element of F1() st ex F being Function of QC-WFF ,F1() st
( x1 = F . F3() & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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) ) ) ) ) & ex F being Function of QC-WFF ,F1() st
( x2 = F . F3() & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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) ) ) ) ) holds
x1 = x2 ) )
proof end;

scheme :: QC_LANG3:sch 3
QCDResult'VERUM{ F1() -> non empty set , F2( Element of QC-WFF ) -> Element of F1(), F3() -> Element of F1(), F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1() } :
F2(VERUM ) = F3()
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F2(p) iff ex F being Function of QC-WFF ,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM 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) ) ) ) ) )
proof end;

scheme :: QC_LANG3:sch 4
QCDResult'atomic{ F1() -> non empty set , F2() -> Element of F1(), F3( Element of QC-WFF ) -> Element of F1(), F4() -> QC-formula, F5( Element of QC-WFF ) -> Element of F1(), F6( Element of F1()) -> Element of F1(), F7( Element of F1(), Element of F1()) -> Element of F1(), F8( Element of QC-WFF , Element of F1()) -> Element of F1() } :
F3(F4()) = F5(F4())
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F3(p) iff ex F being Function of QC-WFF ,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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 atomic
proof end;

scheme :: QC_LANG3:sch 5
QCDResult'negative{ F1() -> non empty set , F2() -> Element of F1(), F3() -> QC-formula, F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1(), F8( Element of QC-WFF ) -> Element of F1() } :
F8(F3()) = F5(F8((the_argument_of F3())))
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F8(p) iff ex F being Function of QC-WFF ,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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: F3() is negative
proof end;

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

scheme :: QC_LANG3:sch 7
QCDResult'universal{ F1() -> non empty set , F2() -> Element of F1(), F3() -> QC-formula, F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1(), F8( Element of QC-WFF ) -> Element of F1() } :
F8(F3()) = F7(F3(),F8((the_scope_of F3())))
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F8(p) iff ex F being Function of QC-WFF ,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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: F3() is universal
proof end;

theorem :: QC_LANG3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being QC-pred_symbol holds P is QC-pred_symbol of (the_arity_of P)
proof end;

definition
let l be FinSequence of QC-variables ;
let V be non empty Subset of QC-variables ;
canceled;
func variables_in l,V -> Subset of V equals :: QC_LANG3:def 2
{ (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } ;
coherence
{ (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } is Subset of V
proof end;
end;

:: deftheorem QC_LANG3:def 1 :
canceled;

:: deftheorem defines variables_in QC_LANG3:def 2 :
for l being FinSequence of QC-variables
for V being non empty Subset of QC-variables holds variables_in l,V = { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } ;

theorem :: QC_LANG3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being FinSequence of QC-variables holds still_not-bound_in l = variables_in l,bound_QC-variables ;

deffunc H1( Element of QC-WFF ) -> Element of bool bound_QC-variables = still_not-bound_in $1;

deffunc H2( Element of QC-WFF ) -> Element of bool bound_QC-variables = still_not-bound_in (the_arguments_of $1);

deffunc H3( Subset of bound_QC-variables ) -> Subset of bound_QC-variables = $1;

deffunc H4( Subset of bound_QC-variables , Subset of bound_QC-variables ) -> Element of bool bound_QC-variables = $1 \/ $2;

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

Lm1: for p being QC-formula
for d being Subset of bound_QC-variables holds
( d = H1(p) iff ex F being Function of QC-WFF , bool bound_QC-variables st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( 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) ) ) ) ) )
proof end;

theorem Th7: :: QC_LANG3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
still_not-bound_in VERUM = {}
proof end;

theorem Th8: :: QC_LANG3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is atomic holds
still_not-bound_in p = still_not-bound_in (the_arguments_of p)
proof end;

theorem :: QC_LANG3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds still_not-bound_in (P ! l) = still_not-bound_in l
proof end;

theorem Th10: :: QC_LANG3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is negative holds
still_not-bound_in p = still_not-bound_in (the_argument_of p)
proof end;

theorem Th11: :: QC_LANG3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula holds still_not-bound_in ('not' p) = still_not-bound_in p
proof end;

theorem Th12: :: QC_LANG3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
still_not-bound_in FALSUM = {} by Th7, Th11, QC_LANG2:def 1;

theorem Th13: :: QC_LANG3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is conjunctive holds
still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))
proof end;

theorem Th14: :: QC_LANG3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th15: :: QC_LANG3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is universal holds
still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}
proof end;

theorem Th16: :: QC_LANG3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being QC-formula holds still_not-bound_in (All x,p) = (still_not-bound_in p) \ {x}
proof end;

theorem Th17: :: QC_LANG3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is disjunctive holds
still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p))
proof end;

theorem :: QC_LANG3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th19: :: QC_LANG3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is conditional holds
still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p))
proof end;

theorem Th20: :: QC_LANG3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th21: :: QC_LANG3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is biconditional holds
still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))
proof end;

theorem :: QC_LANG3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th23: :: QC_LANG3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being QC-formula holds still_not-bound_in (Ex x,p) = (still_not-bound_in p) \ {x}
proof end;

theorem :: QC_LANG3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( VERUM is closed & FALSUM is closed ) by Th7, Th12, QC_LANG1:def 30;

theorem Th25: :: QC_LANG3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula holds
( p is closed iff 'not' p is closed )
proof end;

theorem Th26: :: QC_LANG3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds
( ( p is closed & q is closed ) iff p '&' q is closed )
proof end;

theorem Th27: :: QC_LANG3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being QC-formula holds
( All x,p is closed iff still_not-bound_in p c= {x} )
proof end;

theorem :: QC_LANG3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being QC-formula st p is closed holds
All x,p is closed
proof end;

theorem :: QC_LANG3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds
( ( p is closed & q is closed ) iff p 'or' q is closed )
proof end;

theorem Th30: :: QC_LANG3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds
( ( p is closed & q is closed ) iff p => q is closed )
proof end;

theorem :: QC_LANG3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being QC-formula holds
( ( p is closed & q is closed ) iff p <=> q is closed )
proof end;

theorem Th32: :: QC_LANG3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being QC-formula holds
( Ex x,p is closed iff still_not-bound_in p c= {x} )
proof end;

theorem :: QC_LANG3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being QC-formula st p is closed holds
Ex x,p is closed
proof end;

definition
let k be Nat;
func x. k -> bound_QC-variable equals :: QC_LANG3:def 3
[4,k];
coherence
[4,k] is bound_QC-variable
proof end;
end;

:: deftheorem defines x. QC_LANG3:def 3 :
for k being Nat holds x. k = [4,k];

theorem :: QC_LANG3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat st x. i = x. j holds
i = j by ZFMISC_1:33;

theorem :: QC_LANG3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable ex i being Nat st x. i = x
proof end;

definition
let k be Nat;
func a. k -> free_QC-variable equals :: QC_LANG3:def 4
[6,k];
coherence
[6,k] is free_QC-variable
proof end;
end;

:: deftheorem defines a. QC_LANG3:def 4 :
for k being Nat holds a. k = [6,k];

theorem :: QC_LANG3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat st a. i = a. j holds
i = j by ZFMISC_1:33;

theorem :: QC_LANG3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being free_QC-variable ex i being Nat st a. i = a
proof end;

theorem :: QC_LANG3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Element of fixed_QC-variables
for a being Element of free_QC-variables holds c <> a
proof end;

theorem :: QC_LANG3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Element of fixed_QC-variables
for x being Element of bound_QC-variables holds c <> x
proof end;

theorem :: QC_LANG3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Element of free_QC-variables
for x being Element of bound_QC-variables holds a <> x
proof end;

definition
let V be non empty Subset of QC-variables ;
let p be Element of QC-WFF ;
func Vars p,V -> Subset of V means :Def5: :: QC_LANG3:def 5
 ex F being Function of QC-WFF , bool V st
( it = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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 , bool V st
( b1 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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 , bool V st
( b1 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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 , bool V st
( b2 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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 end;
end;

:: deftheorem Def5 defines Vars QC_LANG3:def 5 :
for V being non empty Subset of QC-variables
for p being Element of QC-WFF
for b3 being Subset of V holds
( b3 = Vars p,V iff ex F being Function of QC-WFF , bool V st
( b3 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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
let V be non empty Subset of QC-variables ; :: thesis: ( H6( VERUM ) = {} & ( for p being Element of QC-WFF st p is atomic holds
Vars p,V = variables_in (the_arguments_of p),V ) & ( for p being Element of QC-WFF st p is negative holds
Vars p,V = Vars (the_argument_of p),V ) & ( for p being Element of QC-WFF 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 st p is universal holds
Vars p,V = Vars (the_scope_of p),V ) )
deffunc H6( Element of QC-WFF ) -> Subset of V = Vars $1,V;
deffunc H7( Element of QC-WFF ) -> Subset of V = variables_in (the_arguments_of $1),V;
deffunc H8( Subset of V) -> Subset of V = $1;
deffunc H9( Subset of V, Subset of V) -> Element of bool V = $1 \/ $2;
deffunc H10( Element of QC-WFF , Subset of V) -> Subset of V = $2;
A1: for p being Element of QC-WFF
for X being Subset of V holds
( X = H6(p) iff ex F being Function of QC-WFF , bool V st
( X = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM implies F . p = {} V ) & ( p is atomic implies F . p = H7(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H8(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H9(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H10(p,d1) ) ) ) ) ) by Def5;
thus H6( VERUM ) = {} V from QC_LANG3:sch 3( bool x {} x , A1)
.= {} ; :: thesis: ( ( for p being Element of QC-WFF st p is atomic holds
Vars p,V = variables_in (the_arguments_of p),V ) & ( for p being Element of QC-WFF st p is negative holds
Vars p,V = Vars (the_argument_of p),V ) & ( for p being Element of QC-WFF 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 st p is universal holds
Vars p,V = Vars (the_scope_of p),V ) )
thus for p being Element of QC-WFF st p is atomic holds
Vars p,V = variables_in (the_arguments_of p),V :: thesis: ( ( for p being Element of QC-WFF st p is negative holds
Vars p,V = Vars (the_argument_of p),V ) & ( for p being Element of QC-WFF 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 st p is universal holds
Vars p,V = Vars (the_scope_of p),V ) )
proof
let p be Element of QC-WFF ; :: 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 H6(p) = H7(p) from QC_LANG3:sch 4( bool x {} x p , A1, A2); :: thesis: verum
end;
thus for p being Element of QC-WFF st p is negative holds
Vars p,V = Vars (the_argument_of p),V :: thesis: ( ( for p being Element of QC-WFF 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 st p is universal holds
Vars p,V = Vars (the_scope_of p),V ) )
proof
let p be Element of QC-WFF ; :: 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 H6(p) = H8(H6( the_argument_of p)) from QC_LANG3:sch 5( bool x {} x p , A1, A3); :: thesis: verum
end;
thus for p being Element of QC-WFF 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 st p is universal holds
Vars p,V = Vars (the_scope_of p),V
proof
let p be Element of QC-WFF ; :: 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 = H6( the_left_argument_of p) & d2 = H6( the_right_argument_of p) holds
H6(p) = H9(d1,d2) from QC_LANG3:sch 6( bool x {} x p , 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 st p is universal holds
Vars p,V = Vars (the_scope_of p),V :: thesis: verum
proof
let p be Element of QC-WFF ; :: 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 H6(p) = H10(p,H6( the_scope_of p)) from QC_LANG3:sch 7( bool x {} x p , A1, A5); :: thesis: verum
end;
end;

theorem :: QC_LANG3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty Subset of QC-variables holds Vars VERUM ,V = {} by Lm2;

theorem Th47: :: QC_LANG3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables 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 Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )
proof end;

theorem Th48: :: QC_LANG3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for V being non empty Subset of QC-variables
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds
( Vars (P ! l),V = variables_in l,V & Vars (P ! l),V = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in V ) } )
proof end;

theorem :: QC_LANG3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables st p is negative holds
Vars p,V = Vars (the_argument_of p),V by Lm2;

theorem Th50: :: QC_LANG3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars ('not' p),V = Vars p,V
proof end;

theorem Th51: :: QC_LANG3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non empty Subset of QC-variables holds Vars FALSUM ,V = {}
proof end;

theorem :: QC_LANG3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables 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 Th53: :: QC_LANG3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (p '&' q),V = (Vars p,V) \/ (Vars q,V)
proof end;

theorem :: QC_LANG3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables st p is universal holds
Vars p,V = Vars (the_scope_of p),V by Lm2;

theorem Th55: :: QC_LANG3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (All x,p),V = Vars p,V
proof end;

theorem Th56: :: QC_LANG3:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables st p is disjunctive holds
Vars p,V = (Vars (the_left_disjunct_of p),V) \/ (Vars (the_right_disjunct_of p),V)
proof end;

theorem :: QC_LANG3:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (p 'or' q),V = (Vars p,V) \/ (Vars q,V)
proof end;

theorem Th58: :: QC_LANG3:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables st p is conditional holds
Vars p,V = (Vars (the_antecedent_of p),V) \/ (Vars (the_consequent_of p),V)
proof end;

theorem Th59: :: QC_LANG3:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (p => q),V = (Vars p,V) \/ (Vars q,V)
proof end;

theorem Th60: :: QC_LANG3:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables st p is biconditional holds
Vars p,V = (Vars (the_left_side_of p),V) \/ (Vars (the_right_side_of p),V)
proof end;

theorem :: QC_LANG3:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (p <=> q),V = (Vars p,V) \/ (Vars q,V)
proof end;

theorem :: QC_LANG3:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF
for V being non empty Subset of QC-variables st p is existential holds
Vars p,V = Vars (the_argument_of (the_scope_of (the_argument_of p))),V
proof end;

theorem :: QC_LANG3:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (Ex x,p),V = Vars p,V
proof end;

definition
let p be Element of QC-WFF ;
func Free p -> Subset of free_QC-variables equals :: QC_LANG3:def 6
 Vars p,free_QC-variables ;
correctness
coherence
Vars p,free_QC-variables is Subset of free_QC-variables ;
;
end;

:: deftheorem defines Free QC_LANG3:def 6 :
for p being Element of QC-WFF holds Free p = Vars p,free_QC-variables ;

theorem :: QC_LANG3:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG3:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Free VERUM = {} by Lm2;

theorem :: QC_LANG3:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds Free (P ! l) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } by Th48;

theorem Th67: :: QC_LANG3:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF holds Free ('not' p) = Free p by Th50;

theorem :: QC_LANG3:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Free FALSUM = {} by Th51;

theorem Th69: :: QC_LANG3:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Free (p '&' q) = (Free p) \/ (Free q) by Th53;

theorem Th70: :: QC_LANG3:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being Element of QC-WFF holds Free (All x,p) = Free p by Th55;

theorem :: QC_LANG3:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Free (p 'or' q) = (Free p) \/ (Free q)
proof end;

theorem Th72: :: QC_LANG3:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Free (p => q) = (Free p) \/ (Free q)
proof end;

theorem :: QC_LANG3:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Free (p <=> q) = (Free p) \/ (Free q)
proof end;

theorem :: QC_LANG3:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being Element of QC-WFF holds Free (Ex x,p) = Free p
proof end;

definition
let p be Element of QC-WFF ;
func Fixed p -> Subset of fixed_QC-variables equals :: QC_LANG3:def 7
 Vars p,fixed_QC-variables ;
correctness
coherence
Vars p,fixed_QC-variables is Subset of fixed_QC-variables ;
;
end;

:: deftheorem defines Fixed QC_LANG3:def 7 :
for p being Element of QC-WFF holds Fixed p = Vars p,fixed_QC-variables ;

theorem :: QC_LANG3:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th76: :: QC_LANG3:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Fixed VERUM = {} by Lm2;

theorem :: QC_LANG3:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds Fixed (P ! l) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables ) } by Th48;

theorem Th78: :: QC_LANG3:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF holds Fixed ('not' p) = Fixed p by Th50;

theorem :: QC_LANG3:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Fixed FALSUM = {} by Th76, Th78, QC_LANG2:def 1;

theorem Th80: :: QC_LANG3:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Fixed (p '&' q) = (Fixed p) \/ (Fixed q) by Th53;

theorem Th81: :: QC_LANG3:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being Element of QC-WFF holds Fixed (All x,p) = Fixed p by Th55;

theorem :: QC_LANG3:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)
proof end;

theorem Th83: :: QC_LANG3:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Fixed (p => q) = (Fixed p) \/ (Fixed q)
proof end;

theorem :: QC_LANG3:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of QC-WFF holds Fixed (p <=> q) = (Fixed p) \/ (Fixed q)
proof end;

theorem :: QC_LANG3:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being Element of QC-WFF holds Fixed (Ex x,p) = Fixed p
proof end;