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

definition
let x, y, a, b be set ;
func IFEQ x,y,a,b -> set equals :Def1: :: CQC_LANG:def 1
a if x = y
otherwise b;
correctness
coherence
( ( x = y implies a is set ) & ( not x = y implies b is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def1 defines IFEQ CQC_LANG:def 1 :
for x, y, a, b being set holds
( ( x = y implies IFEQ x,y,a,b = a ) & ( not x = y implies IFEQ x,y,a,b = b ) );

definition
let D be non empty set ;
let x, y be set ;
let a, b be Element of D;
:: original: IFEQ
redefine func IFEQ x,y,a,b -> Element of D;
coherence
IFEQ x,y,a,b is Element of D
proof end;
end;

definition
let x, y be set ;
func x .--> y -> set equals :: CQC_LANG:def 2
{x} --> y;
coherence
{x} --> y is set ;
end;

:: deftheorem defines .--> CQC_LANG:def 2 :
for x, y being set holds x .--> y = {x} --> y;

registration
let x, y be set ;
cluster x .--> y -> Relation-like Function-like ;
coherence
( x .--> y is Function-like & x .--> y is Relation-like ) ;
end;

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

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

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

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

theorem Th5: :: CQC_LANG:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds
( dom (x .--> y) = {x} & rng (x .--> y) = {y} ) by FUNCOP_1:14, FUNCOP_1:19;

theorem Th6: :: CQC_LANG:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds (x .--> y) . x = y
proof end;

Lm1: for x being bound_QC-variable holds not x in fixed_QC-variables
proof end;

theorem Th7: :: CQC_LANG:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( x in QC-variables iff ( x in fixed_QC-variables or x in free_QC-variables or x in bound_QC-variables ) )
proof end;

definition
mode Substitution is PartFunc of free_QC-variables , QC-variables ;
end;

definition
let l be FinSequence of QC-variables ;
let f be Substitution;
func Subst l,f -> FinSequence of QC-variables means :Def3: :: CQC_LANG:def 3
( len it = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies it . k = f . (l . k) ) & ( not l . k in dom f implies it . k = l . k ) ) ) );
existence
ex b1 being FinSequence of QC-variables st
( len b1 = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies b1 . k = f . (l . k) ) & ( not l . k in dom f implies b1 . k = l . k ) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of QC-variables st len b1 = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies b1 . k = f . (l . k) ) & ( not l . k in dom f implies b1 . k = l . k ) ) ) & len b2 = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies b2 . k = f . (l . k) ) & ( not l . k in dom f implies b2 . k = l . k ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Subst CQC_LANG:def 3 :
for l being FinSequence of QC-variables
for f being Substitution
for b3 being FinSequence of QC-variables holds
( b3 = Subst l,f iff ( len b3 = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies b3 . k = f . (l . k) ) & ( not l . k in dom f implies b3 . k = l . k ) ) ) ) );

definition
let k be Nat;
let l be QC-variable_list of k;
let f be Substitution;
:: original: Subst
redefine func Subst l,f -> QC-variable_list of k;
coherence
Subst l,f is QC-variable_list of k
proof end;
end;

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

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

theorem Th10: :: CQC_LANG:10  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 a being free_QC-variable holds a .--> x is Substitution
proof end;

definition
let a be free_QC-variable;
let x be bound_QC-variable;
:: original: .-->
redefine func a .--> x -> Substitution;
coherence
a .--> x is Substitution by Th10;
end;

theorem Th11: :: CQC_LANG:11  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 x being bound_QC-variable
for a being free_QC-variable
for ll, l being FinSequence of QC-variables
for f being Substitution st f = a .--> x & ll = Subst l,f & 1 <= k & k <= len l holds
( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
proof end;

definition
func CQC-WFF -> Subset of QC-WFF equals :: CQC_LANG:def 4
{ s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } ;
coherence
{ s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } is Subset of QC-WFF
proof end;
end;

:: deftheorem defines CQC-WFF CQC_LANG:def 4 :
CQC-WFF = { s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } ;

registration
cluster CQC-WFF -> non empty ;
coherence
not CQC-WFF is empty
proof end;
end;

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

theorem Th13: :: CQC_LANG:13  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
( p is Element of CQC-WFF iff ( Fixed p = {} & Free p = {} ) )
proof end;

definition
let k be Nat;
let IT be QC-variable_list of k;
attr IT is CQC-variable_list-like means :Def5: :: CQC_LANG:def 5
 rng IT c= bound_QC-variables ;
end;

:: deftheorem Def5 defines CQC-variable_list-like CQC_LANG:def 5 :
for k being Nat
for IT being QC-variable_list of k holds
( IT is CQC-variable_list-like iff rng IT c= bound_QC-variables );

registration
let k be Nat;
cluster CQC-variable_list-like QC-variable_list of k;
existence
ex b1 being QC-variable_list of k st b1 is CQC-variable_list-like
proof end;
end;

definition
let k be Nat;
mode CQC-variable_list of k is CQC-variable_list-like QC-variable_list of k;
end;

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

theorem Th15: :: CQC_LANG:15  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 l being QC-variable_list of k holds
( l is CQC-variable_list of k iff ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} ) )
proof end;

theorem :: CQC_LANG:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
VERUM is Element of CQC-WFF by Th13, QC_LANG3:65, QC_LANG3:76;

theorem Th17: :: CQC_LANG:17  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
( P ! l is Element of CQC-WFF iff ( { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} & { (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} ) )
proof end;

definition
let k be Nat;
let P be QC-pred_symbol of k;
let l be CQC-variable_list of k;
:: original: !
redefine func P ! l -> Element of CQC-WFF ;
coherence
P ! l is Element of CQC-WFF
proof end;
end;

theorem Th18: :: CQC_LANG:18  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
( 'not' p is Element of CQC-WFF iff p is Element of CQC-WFF )
proof end;

theorem Th19: :: CQC_LANG:19  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
( p '&' q is Element of CQC-WFF iff ( p is Element of CQC-WFF & q is Element of CQC-WFF ) )
proof end;

definition
:: original: VERUM
redefine func VERUM -> Element of CQC-WFF ;
coherence
VERUM is Element of CQC-WFF by Th13, QC_LANG3:65, QC_LANG3:76;
let r be Element of CQC-WFF ;
:: original: 'not'
redefine func 'not' r -> Element of CQC-WFF ;
coherence
'not' r is Element of CQC-WFF by Th18;
let s be Element of CQC-WFF ;
:: original: '&'
redefine func r '&' s -> Element of CQC-WFF ;
coherence
r '&' s is Element of CQC-WFF by Th19;
end;

theorem Th20: :: CQC_LANG:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being Element of CQC-WFF holds r => s is Element of CQC-WFF
proof end;

theorem Th21: :: CQC_LANG:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being Element of CQC-WFF holds r 'or' s is Element of CQC-WFF
proof end;

theorem Th22: :: CQC_LANG:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being Element of CQC-WFF holds r <=> s is Element of CQC-WFF
proof end;

definition
let r, s be Element of CQC-WFF ;
:: original: =>
redefine func r => s -> Element of CQC-WFF ;
coherence
r => s is Element of CQC-WFF by Th20;
:: original: 'or'
redefine func r 'or' s -> Element of CQC-WFF ;
coherence
r 'or' s is Element of CQC-WFF by Th21;
:: original: <=>
redefine func r <=> s -> Element of CQC-WFF ;
coherence
r <=> s is Element of CQC-WFF by Th22;
end;

theorem Th23: :: CQC_LANG: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 Element of QC-WFF holds
( All x,p is Element of CQC-WFF iff p is Element of CQC-WFF )
proof end;

definition
let x be bound_QC-variable;
let r be Element of CQC-WFF ;
:: original: All
redefine func All x,r -> Element of CQC-WFF ;
coherence
All x,r is Element of CQC-WFF by Th23;
end;

theorem Th24: :: CQC_LANG:24  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 r being Element of CQC-WFF holds Ex x,r is Element of CQC-WFF
proof end;

definition
let x be bound_QC-variable;
let r be Element of CQC-WFF ;
:: original: Ex
redefine func Ex x,r -> Element of CQC-WFF ;
coherence
Ex x,r is Element of CQC-WFF by Th24;
end;

scheme :: CQC_LANG:sch 1
CQCInd{ P1[ set ] } :
for r being Element of CQC-WFF holds P1[r]
provided
A1: for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( P1[ VERUM ] & P1[P ! l] & ( P1[r] implies P1[ 'not' r] ) & ( P1[r] & P1[s] implies P1[r '&' s] ) & ( P1[r] implies P1[ All x,r] ) )
proof end;

scheme :: CQC_LANG:sch 2
CQCFuncEx{ F1() -> non empty set , F2() -> Element of F1(), F3( set , set , set ) -> Element of F1(), F4( set ) -> Element of F1(), F5( set , set ) -> Element of F1(), F6( set , set ) -> Element of F1() } :
ex F being Function of CQC-WFF ,F1() st
( F . VERUM = F2() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F3(k,P,l) & F . ('not' r) = F4((F . r)) & F . (r '&' s) = F5((F . r),(F . s)) & F . (All x,r) = F6(x,(F . r)) ) ) )
proof end;

scheme :: CQC_LANG:sch 3
CQCFuncUniq{ F1() -> non empty set , F2() -> Function of CQC-WFF ,F1(), F3() -> Function of CQC-WFF ,F1(), F4() -> Element of F1(), F5( set , set , 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: ( F2() . VERUM = F4() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F2() . (P ! l) = F5(k,P,l) & F2() . ('not' r) = F6((F2() . r)) & F2() . (r '&' s) = F7((F2() . r),(F2() . s)) & F2() . (All x,r) = F8(x,(F2() . r)) ) ) ) and
A2: ( F3() . VERUM = F4() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F3() . (P ! l) = F5(k,P,l) & F3() . ('not' r) = F6((F3() . r)) & F3() . (r '&' s) = F7((F3() . r),(F3() . s)) & F3() . (All x,r) = F8(x,(F3() . r)) ) ) )
proof end;

scheme :: CQC_LANG:sch 4
CQCDefcorrectness{ F1() -> non empty set , F2() -> Element of CQC-WFF , F3() -> Element of F1(), F4( set , set , set ) -> Element of F1(), F5( set ) -> Element of F1(), F6( set , set ) -> Element of F1(), F7( set , set ) -> Element of F1() } :
( ex d being Element of F1() ex F being Function of CQC-WFF ,F1() st
( d = F . F2() & F . VERUM = F3() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F6((F . r),(F . s)) & F . (All x,r) = F7(x,(F . r)) ) ) ) & ( for d1, d2 being Element of F1() st ex F being Function of CQC-WFF ,F1() st
( d1 = F . F2() & F . VERUM = F3() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F6((F . r),(F . s)) & F . (All x,r) = F7(x,(F . r)) ) ) ) & ex F being Function of CQC-WFF ,F1() st
( d2 = F . F2() & F . VERUM = F3() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F6((F . r),(F . s)) & F . (All x,r) = F7(x,(F . r)) ) ) ) holds
d1 = d2 ) )
proof end;

scheme :: CQC_LANG:sch 5
CQCDefVERUM{ F1() -> non empty set , F2( set ) -> Element of F1(), F3() -> Element of F1(), F4( set , set , set ) -> Element of F1(), F5( set ) -> Element of F1(), F6( set , set ) -> Element of F1(), F7( set , set ) -> Element of F1() } :
F2(VERUM ) = F3()
provided
A1: for p being Element of CQC-WFF
for d being Element of F1() holds
( d = F2(p) iff ex F being Function of CQC-WFF ,F1() st
( d = F . p & F . VERUM = F3() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F6((F . r),(F . s)) & F . (All x,r) = F7(x,(F . r)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 6
CQCDefatomic{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> Element of F1(), F4( set , set , set ) -> Element of F1(), F5() -> Nat, F6() -> QC-pred_symbol of F5(), F7() -> CQC-variable_list of F5(), F8( set ) -> Element of F1(), F9( set , set ) -> Element of F1(), F10( set , set ) -> Element of F1() } :
F3((F6() ! F7())) = F4(F5(),F6(),F7())
provided
A1: for p being Element of CQC-WFF
for d being Element of F1() holds
( d = F3(p) iff ex F being Function of CQC-WFF ,F1() st
( d = F . p & F . VERUM = F2() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F8((F . r)) & F . (r '&' s) = F9((F . r),(F . s)) & F . (All x,r) = F10(x,(F . r)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 7
CQCDefnegative{ F1() -> non empty set , F2( set ) -> Element of F1(), F3() -> Element of F1(), F4( set , set , set ) -> Element of F1(), F5( set ) -> Element of F1(), F6() -> Element of CQC-WFF , F7( set , set ) -> Element of F1(), F8( set , set ) -> Element of F1() } :
F2(('not' F6())) = F5(F2(F6()))
provided
A1: for p being Element of CQC-WFF
for d being Element of F1() holds
( d = F2(p) iff ex F being Function of CQC-WFF ,F1() st
( d = F . p & F . VERUM = F3() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All x,r) = F8(x,(F . r)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 8
QCDefconjunctive{ F1() -> non empty set , F2( set ) -> Element of F1(), F3() -> Element of F1(), F4( set , set , set ) -> Element of F1(), F5( set ) -> Element of F1(), F6( set , set ) -> Element of F1(), F7() -> Element of CQC-WFF , F8() -> Element of CQC-WFF , F9( set , set ) -> Element of F1() } :
F2((F7() '&' F8())) = F6(F2(F7()),F2(F8()))
provided
A1: for p being Element of CQC-WFF
for d being Element of F1() holds
( d = F2(p) iff ex F being Function of CQC-WFF ,F1() st
( d = F . p & F . VERUM = F3() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F6((F . r),(F . s)) & F . (All x,r) = F9(x,(F . r)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 9
QCDefuniversal{ F1() -> non empty set , F2( set ) -> Element of F1(), F3() -> Element of F1(), F4( set , set , set ) -> Element of F1(), F5( set ) -> Element of F1(), F6( set , set ) -> Element of F1(), F7( set , set ) -> Element of F1(), F8() -> bound_QC-variable, F9() -> Element of CQC-WFF } :
F2((All F8(),F9())) = F7(F8(),F2(F9()))
provided
A1: for p being Element of CQC-WFF
for d being Element of F1() holds
( d = F2(p) iff ex F being Function of CQC-WFF ,F1() st
( d = F . p & F . VERUM = F3() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F6((F . r),(F . s)) & F . (All x,r) = F7(x,(F . r)) ) ) ) )
proof end;

Lm2: for x being bound_QC-variable
for F1, F2 being Function of QC-WFF , QC-WFF st ( for q being Element of QC-WFF holds
( F1 . VERUM = VERUM & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst (the_arguments_of q),((a. 0) .--> x)) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ (bound_in q),x,q,(All (bound_in q),(F1 . (the_scope_of q))) ) ) ) & ( for q being Element of QC-WFF holds
( F2 . VERUM = VERUM & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst (the_arguments_of q),((a. 0) .--> x)) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ (bound_in q),x,q,(All (bound_in q),(F2 . (the_scope_of q))) ) ) ) holds
F1 = F2
proof end;

definition
let p be Element of QC-WFF ;
let x be bound_QC-variable;
func p . x -> Element of QC-WFF means :Def6: :: CQC_LANG:def 6
 ex F being Function of QC-WFF , QC-WFF st
( it = F . p & ( for q being Element of QC-WFF holds
( F . VERUM = VERUM & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst (the_arguments_of q),((a. 0) .--> x)) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ (bound_in q),x,q,(All (bound_in q),(F . (the_scope_of q))) ) ) ) );
existence
ex b1 being Element of QC-WFF ex F being Function of QC-WFF , QC-WFF st
( b1 = F . p & ( for q being Element of QC-WFF holds
( F . VERUM = VERUM & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst (the_arguments_of q),((a. 0) .--> x)) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ (bound_in q),x,q,(All (bound_in q),(F . (the_scope_of q))) ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of QC-WFF st ex F being Function of QC-WFF , QC-WFF st
( b1 = F . p & ( for q being Element of QC-WFF holds
( F . VERUM = VERUM & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst (the_arguments_of q),((a. 0) .--> x)) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ (bound_in q),x,q,(All (bound_in q),(F . (the_scope_of q))) ) ) ) ) & ex F being Function of QC-WFF , QC-WFF st
( b2 = F . p & ( for q being Element of QC-WFF holds
( F . VERUM = VERUM & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst (the_arguments_of q),((a. 0) .--> x)) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ (bound_in q),x,q,(All (bound_in q),(F . (the_scope_of q))) ) ) ) ) holds
b1 = b2 by Lm2;
end;

:: deftheorem Def6 defines . CQC_LANG:def 6 :
for p being Element of QC-WFF
for x being bound_QC-variable
for b3 being Element of QC-WFF holds
( b3 = p . x iff ex F being Function of QC-WFF , QC-WFF st
( b3 = F . p & ( for q being Element of QC-WFF holds
( F . VERUM = VERUM & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst (the_arguments_of q),((a. 0) .--> x)) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ (bound_in q),x,q,(All (bound_in q),(F . (the_scope_of q))) ) ) ) ) );

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

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

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

theorem Th28: :: CQC_LANG: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 holds VERUM . x = VERUM
proof end;

theorem Th29: :: CQC_LANG:29  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 st p is atomic holds
p . x = (the_pred_symbol_of p) ! (Subst (the_arguments_of p),((a. 0) .--> x))
proof end;

theorem Th30: :: CQC_LANG:30  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 x being bound_QC-variable
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds (P ! l) . x = P ! (Subst l,((a. 0) .--> x))
proof end;

theorem Th31: :: CQC_LANG:31  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 st p is negative holds
p . x = 'not' ((the_argument_of p) . x)
proof end;

theorem Th32: :: CQC_LANG: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 Element of QC-WFF holds ('not' p) . x = 'not' (p . x)
proof end;

theorem Th33: :: CQC_LANG: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 Element of QC-WFF st p is conjunctive holds
p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x)
proof end;

theorem Th34: :: CQC_LANG:34  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, q being Element of QC-WFF holds (p '&' q) . x = (p . x) '&' (q . x)
proof end;

Lm3: for x being bound_QC-variable
for p being Element of QC-WFF st p is universal holds
p . x = IFEQ (bound_in p),x,p,(All (bound_in p),((the_scope_of p) . x))
proof end;

theorem Th35: :: CQC_LANG:35  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 st p is universal & bound_in p = x holds
p . x = p
proof end;

theorem Th36: :: CQC_LANG: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
for p being Element of QC-WFF st p is universal & bound_in p <> x holds
p . x = All (bound_in p),((the_scope_of p) . x)
proof end;

theorem Th37: :: CQC_LANG:37  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 (All x,p) . x = All x,p
proof end;

theorem Th38: :: CQC_LANG:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being bound_QC-variable
for p being Element of QC-WFF st x <> y holds
(All x,p) . y = All x,(p . y)
proof end;

theorem Th39: :: CQC_LANG:39  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 st Free p = {} holds
p . x = p
proof end;

theorem :: CQC_LANG:40  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 r being Element of CQC-WFF holds r . x = r
proof end;

theorem :: CQC_LANG:41  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 (p . x) = Fixed p
proof end;

theorem Th42: :: CQC_LANG:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being set holds i,j :-> k = [i,j] .--> k
proof end;

theorem :: CQC_LANG:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being set holds (i,j :-> k) . i,j = k
proof end;