:: CQC_LANG semantic presentation

definition
let c1, c2, c3, c4 be set ;
func IFEQ c1,c2,c3,c4 -> set equals :Def1: :: CQC_LANG:def 1
a3 if a1 = a2
otherwise a4;
correctness
coherence
( ( c1 = c2 implies c3 is set ) & ( not c1 = c2 implies c4 is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def1 defines IFEQ CQC_LANG:def 1 :
for b1, b2, b3, b4 being set holds
( ( b1 = b2 implies IFEQ b1,b2,b3,b4 = b3 ) & ( not b1 = b2 implies IFEQ b1,b2,b3,b4 = b4 ) );

definition
let c1 be non empty set ;
let c2, c3 be set ;
let c4, c5 be Element of c1;
redefine func IFEQ as IFEQ c2,c3,c4,c5 -> Element of a1;
coherence
IFEQ c2,c3,c4,c5 is Element of c1
proof end;
end;

definition
let c1, c2 be set ;
func c1 .--> c2 -> set equals :: CQC_LANG:def 2
{a1} --> a2;
coherence
{c1} --> c2 is set ;
end;

:: deftheorem Def2 defines .--> CQC_LANG:def 2 :
for b1, b2 being set holds b1 .--> b2 = {b1} --> b2;

registration
let c1, c2 be set ;
cluster a1 .--> a2 -> Relation-like Function-like ;
coherence
( c1 .--> c2 is Function-like & c1 .--> c2 is Relation-like ) ;
end;

theorem Th1: :: CQC_LANG:1
canceled;

theorem Th2: :: CQC_LANG:2
canceled;

theorem Th3: :: CQC_LANG:3
canceled;

theorem Th4: :: CQC_LANG:4
canceled;

theorem Th5: :: CQC_LANG:5
for b1, b2 being set holds
( dom (b1 .--> b2) = {b1} & rng (b1 .--> b2) = {b2} ) by FUNCOP_1:14, FUNCOP_1:19;

theorem Th6: :: CQC_LANG:6
for b1, b2 being set holds (b1 .--> b2) . b1 = b2
proof end;

Lemma4: for b1 being bound_QC-variable holds not b1 in fixed_QC-variables
proof end;

theorem Th7: :: CQC_LANG:7
for b1 being set holds
( b1 in QC-variables iff ( b1 in fixed_QC-variables or b1 in free_QC-variables or b1 in bound_QC-variables ) )
proof end;

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

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

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

definition
let c1 be Nat;
let c2 be QC-variable_list of c1;
let c3 be Substitution;
redefine func Subst as Subst c2,c3 -> QC-variable_list of a1;
coherence
Subst c2,c3 is QC-variable_list of c1
proof end;
end;

theorem Th8: :: CQC_LANG:8
canceled;

theorem Th9: :: CQC_LANG:9
canceled;

theorem Th10: :: CQC_LANG:10
for b1 being bound_QC-variable
for b2 being free_QC-variable holds b2 .--> b1 is Substitution
proof end;

definition
let c1 be free_QC-variable;
let c2 be bound_QC-variable;
redefine func .--> as c1 .--> c2 -> Substitution;
coherence
c1 .--> c2 is Substitution by Th10;
end;

theorem Th11: :: CQC_LANG:11
for b1 being Nat
for b2 being bound_QC-variable
for b3 being free_QC-variable
for b4, b5 being FinSequence of QC-variables
for b6 being Substitution st b6 = b3 .--> b2 & b4 = Subst b5,b6 & 1 <= b1 & b1 <= len b5 holds
( ( b5 . b1 = b3 implies b4 . b1 = b2 ) & ( b5 . b1 <> b3 implies b4 . b1 = b5 . b1 ) )
proof end;

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

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

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

theorem Th12: :: CQC_LANG:12
canceled;

theorem Th13: :: CQC_LANG:13
for b1 being Element of QC-WFF holds
( b1 is Element of CQC-WFF iff ( Fixed b1 = {} & Free b1 = {} ) )
proof end;

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

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

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

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

theorem Th14: :: CQC_LANG:14
canceled;

theorem Th15: :: CQC_LANG:15
for b1 being Nat
for b2 being QC-variable_list of b1 holds
( b2 is CQC-variable_list of b1 iff ( { (b2 . b3) where B is Nat : ( 1 <= b3 & b3 <= len b2 & b2 . b3 in free_QC-variables ) } = {} & { (b2 . b3) where B is Nat : ( 1 <= b3 & b3 <= len b2 & b2 . b3 in fixed_QC-variables ) } = {} ) )
proof end;

theorem Th16: :: CQC_LANG:16
VERUM is Element of CQC-WFF by Th13, QC_LANG3:65, QC_LANG3:76;

theorem Th17: :: CQC_LANG:17
for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being QC-variable_list of b1 holds
( b2 ! b3 is Element of CQC-WFF iff ( { (b3 . b4) where B is Nat : ( 1 <= b4 & b4 <= len b3 & b3 . b4 in free_QC-variables ) } = {} & { (b3 . b4) where B is Nat : ( 1 <= b4 & b4 <= len b3 & b3 . b4 in fixed_QC-variables ) } = {} ) )
proof end;

definition
let c1 be Nat;
let c2 be QC-pred_symbol of c1;
let c3 be CQC-variable_list of c1;
redefine func ! as c2 ! c3 -> Element of CQC-WFF ;
coherence
c2 ! c3 is Element of CQC-WFF
proof end;
end;

theorem Th18: :: CQC_LANG:18
for b1 being Element of QC-WFF holds
( 'not' b1 is Element of CQC-WFF iff b1 is Element of CQC-WFF )
proof end;

theorem Th19: :: CQC_LANG:19
for b1, b2 being Element of QC-WFF holds
( b1 '&' b2 is Element of CQC-WFF iff ( b1 is Element of CQC-WFF & b2 is Element of CQC-WFF ) )
proof end;

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

theorem Th20: :: CQC_LANG:20
for b1, b2 being Element of CQC-WFF holds b1 => b2 is Element of CQC-WFF
proof end;

theorem Th21: :: CQC_LANG:21
for b1, b2 being Element of CQC-WFF holds b1 'or' b2 is Element of CQC-WFF
proof end;

theorem Th22: :: CQC_LANG:22
for b1, b2 being Element of CQC-WFF holds b1 <=> b2 is Element of CQC-WFF
proof end;

definition
let c1, c2 be Element of CQC-WFF ;
redefine func => as c1 => c2 -> Element of CQC-WFF ;
coherence
c1 => c2 is Element of CQC-WFF by Th20;
redefine func 'or' as c1 'or' c2 -> Element of CQC-WFF ;
coherence
c1 'or' c2 is Element of CQC-WFF by Th21;
redefine func <=> as c1 <=> c2 -> Element of CQC-WFF ;
coherence
c1 <=> c2 is Element of CQC-WFF by Th22;
end;

theorem Th23: :: CQC_LANG:23
for b1 being bound_QC-variable
for b2 being Element of QC-WFF holds
( All b1,b2 is Element of CQC-WFF iff b2 is Element of CQC-WFF )
proof end;

definition
let c1 be bound_QC-variable;
let c2 be Element of CQC-WFF ;
redefine func All as All c1,c2 -> Element of CQC-WFF ;
coherence
All c1,c2 is Element of CQC-WFF by Th23;
end;

theorem Th24: :: CQC_LANG:24
for b1 being bound_QC-variable
for b2 being Element of CQC-WFF holds Ex b1,b2 is Element of CQC-WFF
proof end;

definition
let c1 be bound_QC-variable;
let c2 be Element of CQC-WFF ;
redefine func Ex as Ex c1,c2 -> Element of CQC-WFF ;
coherence
Ex c1,c2 is Element of CQC-WFF by Th24;
end;

scheme :: CQC_LANG:sch 1
s1{ P1[ set ] } :
for b1 being Element of CQC-WFF holds P1[b1]
provided
E20: for b1, b2 being Element of CQC-WFF
for b3 being bound_QC-variable
for b4 being Nat
for b5 being CQC-variable_list of b4
for b6 being QC-pred_symbol of b4 holds
( P1[ VERUM ] & P1[b6 ! b5] & ( P1[b1] implies P1[ 'not' b1] ) & ( P1[b1] & P1[b2] implies P1[b1 '&' b2] ) & ( P1[b1] implies P1[ All b3,b1] ) )
proof end;

scheme :: CQC_LANG:sch 2
s2{ 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 b1 being Function of CQC-WFF ,F1() st
( b1 . VERUM = F2() & ( for b2, b3 being Element of CQC-WFF
for b4 being bound_QC-variable
for b5 being Nat
for b6 being CQC-variable_list of b5
for b7 being QC-pred_symbol of b5 holds
( b1 . (b7 ! b6) = F3(b5,b7,b6) & b1 . ('not' b2) = F4((b1 . b2)) & b1 . (b2 '&' b3) = F5((b1 . b2),(b1 . b3)) & b1 . (All b4,b2) = F6(b4,(b1 . b2)) ) ) )
proof end;

scheme :: CQC_LANG:sch 3
s3{ 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
E20: ( F2() . VERUM = F4() & ( for b1, b2 being Element of CQC-WFF
for b3 being bound_QC-variable
for b4 being Nat
for b5 being CQC-variable_list of b4
for b6 being QC-pred_symbol of b4 holds
( F2() . (b6 ! b5) = F5(b4,b6,b5) & F2() . ('not' b1) = F6((F2() . b1)) & F2() . (b1 '&' b2) = F7((F2() . b1),(F2() . b2)) & F2() . (All b3,b1) = F8(b3,(F2() . b1)) ) ) ) and
E21: ( F3() . VERUM = F4() & ( for b1, b2 being Element of CQC-WFF
for b3 being bound_QC-variable
for b4 being Nat
for b5 being CQC-variable_list of b4
for b6 being QC-pred_symbol of b4 holds
( F3() . (b6 ! b5) = F5(b4,b6,b5) & F3() . ('not' b1) = F6((F3() . b1)) & F3() . (b1 '&' b2) = F7((F3() . b1),(F3() . b2)) & F3() . (All b3,b1) = F8(b3,(F3() . b1)) ) ) )
proof end;

scheme :: CQC_LANG:sch 4
s4{ 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 b1 being Element of F1()ex b2 being Function of CQC-WFF ,F1() st
( b1 = b2 . F2() & b2 . VERUM = F3() & ( for b3, b4 being Element of CQC-WFF
for b5 being bound_QC-variable
for b6 being Nat
for b7 being CQC-variable_list of b6
for b8 being QC-pred_symbol of b6 holds
( b2 . (b8 ! b7) = F4(b6,b8,b7) & b2 . ('not' b3) = F5((b2 . b3)) & b2 . (b3 '&' b4) = F6((b2 . b3),(b2 . b4)) & b2 . (All b5,b3) = F7(b5,(b2 . b3)) ) ) ) & ( for b1, b2 being Element of F1() st ex b3 being Function of CQC-WFF ,F1() st
( b1 = b3 . F2() & b3 . VERUM = F3() & ( for b4, b5 being Element of CQC-WFF
for b6 being bound_QC-variable
for b7 being Nat
for b8 being CQC-variable_list of b7
for b9 being QC-pred_symbol of b7 holds
( b3 . (b9 ! b8) = F4(b7,b9,b8) & b3 . ('not' b4) = F5((b3 . b4)) & b3 . (b4 '&' b5) = F6((b3 . b4),(b3 . b5)) & b3 . (All b6,b4) = F7(b6,(b3 . b4)) ) ) ) & ex b3 being Function of CQC-WFF ,F1() st
( b2 = b3 . F2() & b3 . VERUM = F3() & ( for b4, b5 being Element of CQC-WFF
for b6 being bound_QC-variable
for b7 being Nat
for b8 being CQC-variable_list of b7
for b9 being QC-pred_symbol of b7 holds
( b3 . (b9 ! b8) = F4(b7,b9,b8) & b3 . ('not' b4) = F5((b3 . b4)) & b3 . (b4 '&' b5) = F6((b3 . b4),(b3 . b5)) & b3 . (All b6,b4) = F7(b6,(b3 . b4)) ) ) ) holds
b1 = b2 ) )
proof end;

scheme :: CQC_LANG:sch 5
s5{ 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
E20: for b1 being Element of CQC-WFF
for b2 being Element of F1() holds
( b2 = F2(b1) iff ex b3 being Function of CQC-WFF ,F1() st
( b2 = b3 . b1 & b3 . VERUM = F3() & ( for b4, b5 being Element of CQC-WFF
for b6 being bound_QC-variable
for b7 being Nat
for b8 being CQC-variable_list of b7
for b9 being QC-pred_symbol of b7 holds
( b3 . (b9 ! b8) = F4(b7,b9,b8) & b3 . ('not' b4) = F5((b3 . b4)) & b3 . (b4 '&' b5) = F6((b3 . b4),(b3 . b5)) & b3 . (All b6,b4) = F7(b6,(b3 . b4)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 6
s6{ 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
E20: for b1 being Element of CQC-WFF
for b2 being Element of F1() holds
( b2 = F3(b1) iff ex b3 being Function of CQC-WFF ,F1() st
( b2 = b3 . b1 & b3 . VERUM = F2() & ( for b4, b5 being Element of CQC-WFF
for b6 being bound_QC-variable
for b7 being Nat
for b8 being CQC-variable_list of b7
for b9 being QC-pred_symbol of b7 holds
( b3 . (b9 ! b8) = F4(b7,b9,b8) & b3 . ('not' b4) = F8((b3 . b4)) & b3 . (b4 '&' b5) = F9((b3 . b4),(b3 . b5)) & b3 . (All b6,b4) = F10(b6,(b3 . b4)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 7
s7{ 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
E20: for b1 being Element of CQC-WFF
for b2 being Element of F1() holds
( b2 = F2(b1) iff ex b3 being Function of CQC-WFF ,F1() st
( b2 = b3 . b1 & b3 . VERUM = F3() & ( for b4, b5 being Element of CQC-WFF
for b6 being bound_QC-variable
for b7 being Nat
for b8 being CQC-variable_list of b7
for b9 being QC-pred_symbol of b7 holds
( b3 . (b9 ! b8) = F4(b7,b9,b8) & b3 . ('not' b4) = F5((b3 . b4)) & b3 . (b4 '&' b5) = F7((b3 . b4),(b3 . b5)) & b3 . (All b6,b4) = F8(b6,(b3 . b4)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 8
s8{ 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
E20: for b1 being Element of CQC-WFF
for b2 being Element of F1() holds
( b2 = F2(b1) iff ex b3 being Function of CQC-WFF ,F1() st
( b2 = b3 . b1 & b3 . VERUM = F3() & ( for b4, b5 being Element of CQC-WFF
for b6 being bound_QC-variable
for b7 being Nat
for b8 being CQC-variable_list of b7
for b9 being QC-pred_symbol of b7 holds
( b3 . (b9 ! b8) = F4(b7,b9,b8) & b3 . ('not' b4) = F5((b3 . b4)) & b3 . (b4 '&' b5) = F6((b3 . b4),(b3 . b5)) & b3 . (All b6,b4) = F9(b6,(b3 . b4)) ) ) ) )
proof end;

scheme :: CQC_LANG:sch 9
s9{ 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
E20: for b1 being Element of CQC-WFF
for b2 being Element of F1() holds
( b2 = F2(b1) iff ex b3 being Function of CQC-WFF ,F1() st
( b2 = b3 . b1 & b3 . VERUM = F3() & ( for b4, b5 being Element of CQC-WFF
for b6 being bound_QC-variable
for b7 being Nat
for b8 being CQC-variable_list of b7
for b9 being QC-pred_symbol of b7 holds
( b3 . (b9 ! b8) = F4(b7,b9,b8) & b3 . ('not' b4) = F5((b3 . b4)) & b3 . (b4 '&' b5) = F6((b3 . b4),(b3 . b5)) & b3 . (All b6,b4) = F7(b6,(b3 . b4)) ) ) ) )
proof end;

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

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

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

theorem Th25: :: CQC_LANG:25
canceled;

theorem Th26: :: CQC_LANG:26
canceled;

theorem Th27: :: CQC_LANG:27
canceled;

theorem Th28: :: CQC_LANG:28
for b1 being bound_QC-variable holds VERUM . b1 = VERUM
proof end;

theorem Th29: :: CQC_LANG:29
for b1 being bound_QC-variable
for b2 being Element of QC-WFF st b2 is atomic holds
b2 . b1 = (the_pred_symbol_of b2) ! (Subst (the_arguments_of b2),((a. 0) .--> b1))
proof end;

theorem Th30: :: CQC_LANG:30
for b1 being Nat
for b2 being bound_QC-variable
for b3 being QC-pred_symbol of b1
for b4 being QC-variable_list of b1 holds (b3 ! b4) . b2 = b3 ! (Subst b4,((a. 0) .--> b2))
proof end;

theorem Th31: :: CQC_LANG:31
for b1 being bound_QC-variable
for b2 being Element of QC-WFF st b2 is negative holds
b2 . b1 = 'not' ((the_argument_of b2) . b1)
proof end;

theorem Th32: :: CQC_LANG:32
for b1 being bound_QC-variable
for b2 being Element of QC-WFF holds ('not' b2) . b1 = 'not' (b2 . b1)
proof end;

theorem Th33: :: CQC_LANG:33
for b1 being bound_QC-variable
for b2 being Element of QC-WFF st b2 is conjunctive holds
b2 . b1 = ((the_left_argument_of b2) . b1) '&' ((the_right_argument_of b2) . b1)
proof end;

theorem Th34: :: CQC_LANG:34
for b1 being bound_QC-variable
for b2, b3 being Element of QC-WFF holds (b2 '&' b3) . b1 = (b2 . b1) '&' (b3 . b1)
proof end;

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

theorem Th35: :: CQC_LANG:35
for b1 being bound_QC-variable
for b2 being Element of QC-WFF st b2 is universal & bound_in b2 = b1 holds
b2 . b1 = b2
proof end;

theorem Th36: :: CQC_LANG:36
for b1 being bound_QC-variable
for b2 being Element of QC-WFF st b2 is universal & bound_in b2 <> b1 holds
b2 . b1 = All (bound_in b2),((the_scope_of b2) . b1)
proof end;

theorem Th37: :: CQC_LANG:37
for b1 being bound_QC-variable
for b2 being Element of QC-WFF holds (All b1,b2) . b1 = All b1,b2
proof end;

theorem Th38: :: CQC_LANG:38
for b1, b2 being bound_QC-variable
for b3 being Element of QC-WFF st b1 <> b2 holds
(All b1,b3) . b2 = All b1,(b3 . b2)
proof end;

theorem Th39: :: CQC_LANG:39
for b1 being bound_QC-variable
for b2 being Element of QC-WFF st Free b2 = {} holds
b2 . b1 = b2
proof end;

theorem Th40: :: CQC_LANG:40
for b1 being bound_QC-variable
for b2 being Element of CQC-WFF holds b2 . b1 = b2
proof end;

theorem Th41: :: CQC_LANG:41
for b1 being bound_QC-variable
for b2 being Element of QC-WFF holds Fixed (b2 . b1) = Fixed b2
proof end;

theorem Th42: :: CQC_LANG:42
for b1, b2, b3 being set holds b1,b2 :-> b3 = [b1,b2] .--> b3
proof end;

theorem Th43: :: CQC_LANG:43
for b1, b2, b3 being set holds (b1,b2 :-> b3) . b1,b2 = b3
proof end;