:: CQC_LANG semantic presentation
begin
Lm1: for A being QC-alphabet
for x being bound_QC-variable of A holds not x in fixed_QC-variables A
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A holds not x in fixed_QC-variables A
let x be bound_QC-variable of A; ::_thesis: not x in fixed_QC-variables A
x in bound_QC-variables A ;
then x in [:{4},(QC-symbols A):] by QC_LANG1:def_4;
then 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;
A3: x1 = 4 by A1, TARSKI:def_1;
assume x in fixed_QC-variables A ; ::_thesis: contradiction
then x in [:{5},(QC-symbols A):] by QC_LANG1:def_5;
then consider c1, c2 being set such that
A4: c1 in {5} and
c2 in QC-symbols A and
A5: x = [c1,c2] by ZFMISC_1:def_2;
c1 = 5 by A4, TARSKI:def_1;
hence contradiction by A2, A5, A3, XTUPLE_0:1; ::_thesis: verum
end;
theorem Th1: :: CQC_LANG:1
for A being QC-alphabet
for x being set holds
( x in QC-variables A iff ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) )
proof
let A be QC-alphabet ; ::_thesis: for x being set holds
( x in QC-variables A iff ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) )
let x be set ; ::_thesis: ( x in QC-variables A iff ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) )
thus ( not x in QC-variables A or x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) ::_thesis: ( ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) implies x in QC-variables A )
proof
assume x in QC-variables A ; ::_thesis: ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A )
then x in [:{6},NAT:] \/ [:{4,5},(QC-symbols A):] by QC_LANG1:def_3;
then ( x in [:{6},NAT:] or x in [:{4,5},(QC-symbols A):] ) by XBOOLE_0:def_3;
then consider x1, x2 being set such that
A1: ( ( x1 in {6} & x2 in NAT & x = [x1,x2] ) or ( x1 in {4,5} & x2 in QC-symbols A & x = [x1,x2] ) ) by ZFMISC_1:def_2;
( ( x1 in {6} & x2 in NAT & x = [x1,x2] ) or ( ( x1 = 4 or x1 = 5 ) & x2 in QC-symbols A & x = [x1,x2] ) ) by A1, TARSKI:def_2;
then ( ( ( x1 in {4} & x2 in QC-symbols A ) or ( x1 in {5} & x2 in QC-symbols A ) or ( x1 in {6} & x2 in NAT ) ) & x = [x1,x2] ) by TARSKI:def_1;
then ( x in [:{4},(QC-symbols A):] or x in [:{5},(QC-symbols A):] or x in [:{6},NAT:] ) by ZFMISC_1:def_2;
hence ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) by QC_LANG1:def_4, QC_LANG1:def_5, QC_LANG1:def_6; ::_thesis: verum
end;
thus ( ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) implies x in QC-variables A ) ; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
mode Substitution of A is PartFunc of (free_QC-variables A),(QC-variables A);
end;
definition
let A be QC-alphabet ;
let l be FinSequence of QC-variables A;
let f be Substitution of A;
func Subst (l,f) -> FinSequence of QC-variables A means :Def1: :: CQC_LANG:def 1
( len it = len l & ( for k being Element of 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 A st
( len b1 = len l & ( for k being Element of 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
defpred S1[ set , set ] means ( ( l . $1 in dom f implies $2 = f . (l . $1) ) & ( not l . $1 in dom f implies $2 = l . $1 ) );
A1: for k being natural number st k in Seg (len l) holds
ex y being set st S1[k,y]
proof
let k be natural number ; ::_thesis: ( k in Seg (len l) implies ex y being set st S1[k,y] )
assume k in Seg (len l) ; ::_thesis: ex y being set st S1[k,y]
( l . k in dom f implies ex y being set st S1[k,y] ) ;
hence ex y being set st S1[k,y] ; ::_thesis: verum
end;
consider s being FinSequence such that
A2: dom s = Seg (len l) and
A3: for k being natural number st k in Seg (len l) holds
S1[k,s . k] from FINSEQ_1:sch_1(A1);
rng s c= QC-variables A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in QC-variables A )
assume y in rng s ; ::_thesis: y in QC-variables A
then consider x being set such that
A4: x in dom s and
A5: s . x = y by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A4;
A6: now__::_thesis:_(_(_l_._x_in_dom_f_&_s_._x_=_f_._(l_._x)_&_f_._(l_._x)_in_QC-variables_A_)_or_(_not_l_._x_in_dom_f_&_s_._x_=_l_._x_)_)
percases ( l . x in dom f or not l . x in dom f ) ;
case l . x in dom f ; ::_thesis: ( s . x = f . (l . x) & f . (l . x) in QC-variables A )
hence ( s . x = f . (l . x) & f . (l . x) in QC-variables A ) by A2, A3, A4, PARTFUN1:4; ::_thesis: verum
end;
case not l . x in dom f ; ::_thesis: s . x = l . x
hence s . x = l . x by A2, A3, A4; ::_thesis: verum
end;
end;
end;
dom l = Seg (len l) by FINSEQ_1:def_3;
hence y in QC-variables A by A2, A4, A5, A6, FINSEQ_2:11; ::_thesis: verum
end;
then reconsider s = s as FinSequence of QC-variables A by FINSEQ_1:def_4;
take s ; ::_thesis: ( len s = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) ) ) )
thus len s = len l by A2, FINSEQ_1:def_3; ::_thesis: for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) )
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len l implies ( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) ) )
assume ( 1 <= k & k <= len l ) ; ::_thesis: ( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) )
then k in dom l by FINSEQ_3:25;
then k in Seg (len l) by FINSEQ_1:def_3;
hence ( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of QC-variables A st len b1 = len l & ( for k being Element of 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 Element of 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
let l1, l2 be FinSequence of QC-variables A; ::_thesis: ( len l1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom f implies l1 . k = f . (l . k) ) & ( not l . k in dom f implies l1 . k = l . k ) ) ) & len l2 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom f implies l2 . k = f . (l . k) ) & ( not l . k in dom f implies l2 . k = l . k ) ) ) implies l1 = l2 )
assume that
A7: len l1 = len l and
A8: for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom f implies l1 . k = f . (l . k) ) & ( not l . k in dom f implies l1 . k = l . k ) ) and
A9: len l2 = len l and
A10: for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom f implies l2 . k = f . (l . k) ) & ( not l . k in dom f implies l2 . k = l . k ) ) ; ::_thesis: l1 = l2
now__::_thesis:_for_k_being_natural_number_st_1_<=_k_&_k_<=_len_l_holds_
l1_._k_=_l2_._k
let k be natural number ; ::_thesis: ( 1 <= k & k <= len l implies l1 . k = l2 . k )
assume A11: ( 1 <= k & k <= len l ) ; ::_thesis: l1 . k = l2 . k
A12: k in NAT by ORDINAL1:def_12;
then A13: ( not l . k in dom f implies l1 . k = l . k ) by A8, A11;
( l . k in dom f implies l1 . k = f . (l . k) ) by A8, A12, A11;
hence l1 . k = l2 . k by A10, A12, A11, A13; ::_thesis: verum
end;
hence l1 = l2 by A7, A9, FINSEQ_1:14; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Subst CQC_LANG:def_1_:_
for A being QC-alphabet
for l being FinSequence of QC-variables A
for f being Substitution of A
for b4 being FinSequence of QC-variables A holds
( b4 = Subst (l,f) iff ( len b4 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom f implies b4 . k = f . (l . k) ) & ( not l . k in dom f implies b4 . k = l . k ) ) ) ) );
registration
let A be QC-alphabet ;
let k be Element of NAT ;
let l be QC-variable_list of k,A;
let f be Substitution of A;
cluster Subst (l,f) -> k -element ;
coherence
Subst (l,f) is k -element
proof
( len (Subst (l,f)) = len l & len l = k ) by Def1, CARD_1:def_7;
hence Subst (l,f) is k -element by CARD_1:def_7; ::_thesis: verum
end;
end;
theorem Th2: :: CQC_LANG:2
for A being QC-alphabet
for x being bound_QC-variable of A
for a being free_QC-variable of A holds a .--> x is Substitution of A
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for a being free_QC-variable of A holds a .--> x is Substitution of A
let x be bound_QC-variable of A; ::_thesis: for a being free_QC-variable of A holds a .--> x is Substitution of A
let a be free_QC-variable of A; ::_thesis: a .--> x is Substitution of A
set f = a .--> x;
rng (a .--> x) = {x} by FUNCOP_1:8;
then A1: rng (a .--> x) c= QC-variables A by ZFMISC_1:31;
dom (a .--> x) = {a} by FUNCOP_1:13;
then dom (a .--> x) c= free_QC-variables A by ZFMISC_1:31;
hence a .--> x is Substitution of A by A1, RELSET_1:4; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let a be free_QC-variable of A;
let x be bound_QC-variable of A;
:: original: .-->
redefine funca .--> x -> Substitution of A;
coherence
a .--> x is Substitution of A by Th2;
end;
theorem Th3: :: CQC_LANG:3
for A being QC-alphabet
for k being Element of NAT
for f being Substitution of A
for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for f being Substitution of A
for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 ) )
let k be Element of NAT ; ::_thesis: for f being Substitution of A
for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 ) )
let f be Substitution of A; ::_thesis: for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 ) )
let x be bound_QC-variable of A; ::_thesis: for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 ) )
let a be free_QC-variable of A; ::_thesis: for l, ll being FinSequence of QC-variables A 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 ) )
let l, ll be FinSequence of QC-variables A; ::_thesis: ( f = a .--> x & ll = Subst (l,f) & 1 <= k & k <= len l implies ( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) ) )
set f9 = a .--> x;
assume A1: ( f = a .--> x & ll = Subst (l,f) & 1 <= k & k <= len l ) ; ::_thesis: ( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
thus ( l . k = a implies ll . k = x ) ::_thesis: ( l . k <> a implies ll . k = l . k )
proof
A2: (a .--> x) . a = x by FUNCOP_1:72;
assume A3: l . k = a ; ::_thesis: ll . k = x
then l . k in {a} by TARSKI:def_1;
then l . k in dom (a .--> x) by FUNCOP_1:13;
hence ll . k = x by A1, A3, A2, Def1; ::_thesis: verum
end;
assume l . k <> a ; ::_thesis: ll . k = l . k
then not l . k in {a} by TARSKI:def_1;
then not l . k in dom (a .--> x) by FUNCOP_1:13;
hence ll . k = l . k by A1, Def1; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
func CQC-WFF A -> Subset of (QC-WFF A) equals :: CQC_LANG:def 2
{ s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ;
coherence
{ s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } is Subset of (QC-WFF A)
proof
set F = { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ;
{ s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } c= QC-WFF A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } or x in QC-WFF A )
assume x in { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ; ::_thesis: x in QC-WFF A
then ex s being QC-formula of A st
( s = x & Fixed s = {} & Free s = {} ) ;
hence x in QC-WFF A ; ::_thesis: verum
end;
hence { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } is Subset of (QC-WFF A) ; ::_thesis: verum
end;
end;
:: deftheorem defines CQC-WFF CQC_LANG:def_2_:_
for A being QC-alphabet holds CQC-WFF A = { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ;
registration
let A be QC-alphabet ;
cluster CQC-WFF A -> non empty ;
coherence
not CQC-WFF A is empty
proof
( Fixed (VERUM A) = {} & Free (VERUM A) = {} ) by QC_LANG3:53, QC_LANG3:63;
then VERUM A in { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ;
hence not CQC-WFF A is empty ; ::_thesis: verum
end;
end;
theorem Th4: :: CQC_LANG:4
for A being QC-alphabet
for p being Element of QC-WFF A holds
( p is Element of CQC-WFF A iff ( Fixed p = {} & Free p = {} ) )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of QC-WFF A holds
( p is Element of CQC-WFF A iff ( Fixed p = {} & Free p = {} ) )
let p be Element of QC-WFF A; ::_thesis: ( p is Element of CQC-WFF A iff ( Fixed p = {} & Free p = {} ) )
thus ( p is Element of CQC-WFF A implies ( Fixed p = {} & Free p = {} ) ) ::_thesis: ( Fixed p = {} & Free p = {} implies p is Element of CQC-WFF A )
proof
assume p is Element of CQC-WFF A ; ::_thesis: ( Fixed p = {} & Free p = {} )
then p in CQC-WFF A ;
then ex s being QC-formula of A st
( s = p & Fixed s = {} & Free s = {} ) ;
hence ( Fixed p = {} & Free p = {} ) ; ::_thesis: verum
end;
assume ( Fixed p = {} & Free p = {} ) ; ::_thesis: p is Element of CQC-WFF A
then p in CQC-WFF A ;
hence p is Element of CQC-WFF A ; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let k be Element of NAT ;
cluster Relation-like NAT -defined QC-variables A -valued bound_QC-variables A -valued Function-like k -element FinSequence-like for FinSequence of QC-variables A;
existence
ex b1 being QC-variable_list of k,A st b1 is bound_QC-variables A -valued
proof
set null = 0 ;
reconsider null = 0 as QC-symbol of A by QC_LANG1:3;
set l = k |-> (x. null);
A1: dom (k |-> (x. null)) = Seg k by FUNCOP_1:13;
rng (k |-> (x. null)) c= QC-variables A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (k |-> (x. null)) or y in QC-variables A )
assume y in rng (k |-> (x. null)) ; ::_thesis: y in QC-variables A
then consider x being set such that
A2: x in dom (k |-> (x. null)) and
A3: (k |-> (x. null)) . x = y by FUNCT_1:def_3;
y = x. null by A1, A2, A3, FINSEQ_2:57;
hence y in QC-variables A ; ::_thesis: verum
end;
then reconsider l = k |-> (x. null) as QC-variable_list of k,A by FINSEQ_1:def_4;
take l ; ::_thesis: l is bound_QC-variables A -valued
let x be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not x in rng l or x in bound_QC-variables A )
assume x in rng l ; ::_thesis: x in bound_QC-variables A
then consider i being set such that
A4: i in dom l and
A5: x = l . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A4;
l . i = x. null by A1, A4, FINSEQ_2:57;
hence x in bound_QC-variables A by A5; ::_thesis: verum
end;
end;
definition
let A be QC-alphabet ;
let k be Element of NAT ;
mode CQC-variable_list of k,A is bound_QC-variables A -valued QC-variable_list of k,A;
end;
theorem Th5: :: CQC_LANG:5
for A being QC-alphabet
for k being Element of NAT
for l being QC-variable_list of k,A holds
( l is CQC-variable_list of k,A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for l being QC-variable_list of k,A holds
( l is CQC-variable_list of k,A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
let k be Element of NAT ; ::_thesis: for l being QC-variable_list of k,A holds
( l is CQC-variable_list of k,A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
let l be QC-variable_list of k,A; ::_thesis: ( l is CQC-variable_list of k,A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
set FR = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } ;
set FI = { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } ;
thus ( l is CQC-variable_list of k,A implies ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) ) ::_thesis: ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} implies l is CQC-variable_list of k,A )
proof
assume l is CQC-variable_list of k,A ; ::_thesis: ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} )
then reconsider l = l as CQC-variable_list of k,A ;
now__::_thesis:_not__{__(l_._i)_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_<=_len_l_&_l_._i_in_free_QC-variables_A_)__}__<>_{}
set x = the Element of { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } ;
assume { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } <> {} ; ::_thesis: contradiction
then the Element of { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } ;
then consider i being Element of NAT such that
the Element of { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = l . i and
A1: ( 1 <= i & i <= len l ) and
A2: l . i in free_QC-variables A ;
i in dom l by A1, FINSEQ_3:25;
then ( rng l c= bound_QC-variables A & l . i in rng l ) by FUNCT_1:def_3, RELAT_1:def_19;
hence contradiction by A2, QC_LANG3:34; ::_thesis: verum
end;
hence { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} ; ::_thesis: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {}
now__::_thesis:_not__{__(l_._j)_where_j_is_Element_of_NAT_:_(_1_<=_j_&_j_<=_len_l_&_l_._j_in_fixed_QC-variables_A_)__}__<>_{}
set x = the Element of { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } ;
assume { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } <> {} ; ::_thesis: contradiction
then the Element of { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } in { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } ;
then consider i being Element of NAT such that
the Element of { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = l . i and
A3: ( 1 <= i & i <= len l ) and
A4: l . i in fixed_QC-variables A ;
i in dom l by A3, FINSEQ_3:25;
then ( rng l c= bound_QC-variables A & l . i in rng l ) by FUNCT_1:def_3, RELAT_1:def_19;
hence contradiction by A4, QC_LANG3:33; ::_thesis: verum
end;
hence { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ; ::_thesis: verum
end;
assume that
A5: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} and
A6: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ; ::_thesis: l is CQC-variable_list of k,A
l is bound_QC-variables A -valued
proof
let x be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not x in rng l or x in bound_QC-variables A )
A7: rng l c= QC-variables A by FINSEQ_1:def_4;
assume x in rng l ; ::_thesis: x in bound_QC-variables A
then consider i being set such that
A8: i in dom l and
A9: l . i = x by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A8;
A10: ( 1 <= i & i <= len l ) by A8, FINSEQ_3:25;
A11: now__::_thesis:_not_x_in_fixed_QC-variables_A
assume x in fixed_QC-variables A ; ::_thesis: contradiction
then x in { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } by A9, A10;
hence contradiction by A6; ::_thesis: verum
end;
A12: now__::_thesis:_not_x_in_free_QC-variables_A
assume x in free_QC-variables A ; ::_thesis: contradiction
then x in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by A9, A10;
hence contradiction by A5; ::_thesis: verum
end;
l . i in rng l by A8, FUNCT_1:def_3;
hence x in bound_QC-variables A by A9, A7, A11, A12, Th1; ::_thesis: verum
end;
hence l is CQC-variable_list of k,A ; ::_thesis: verum
end;
theorem Th6: :: CQC_LANG:6
for A being QC-alphabet holds VERUM A is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: VERUM A is Element of CQC-WFF A
( Fixed (VERUM A) = {} & Free (VERUM A) = {} ) by QC_LANG3:53, QC_LANG3:63;
hence VERUM A is Element of CQC-WFF A by Th4; ::_thesis: verum
end;
theorem Th7: :: CQC_LANG:7
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds
( P ! l is Element of CQC-WFF A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds
( P ! l is Element of CQC-WFF A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds
( P ! l is Element of CQC-WFF A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
let P be QC-pred_symbol of k,A; ::_thesis: for l being QC-variable_list of k,A holds
( P ! l is Element of CQC-WFF A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
let l be QC-variable_list of k,A; ::_thesis: ( P ! l is Element of CQC-WFF A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) )
A1: Free (P ! l) = { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in free_QC-variables A ) } by QC_LANG3:54;
Fixed (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by QC_LANG3:64;
hence ( P ! l is Element of CQC-WFF A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) ) by A1, Th4; ::_thesis: verum
end;
definition
let k be Element of NAT ;
let A be QC-alphabet ;
let P be QC-pred_symbol of k,A;
let l be CQC-variable_list of k,A;
:: original: !
redefine funcP ! l -> Element of CQC-WFF A;
coherence
P ! l is Element of CQC-WFF A
proof
A1: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} by Th5;
{ (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} by Th5;
hence P ! l is Element of CQC-WFF A by A1, Th7; ::_thesis: verum
end;
end;
theorem Th8: :: CQC_LANG:8
for A being QC-alphabet
for p being Element of QC-WFF A holds
( 'not' p is Element of CQC-WFF A iff p is Element of CQC-WFF A )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of QC-WFF A holds
( 'not' p is Element of CQC-WFF A iff p is Element of CQC-WFF A )
let p be Element of QC-WFF A; ::_thesis: ( 'not' p is Element of CQC-WFF A iff p is Element of CQC-WFF A )
thus ( 'not' p is Element of CQC-WFF A implies p is Element of CQC-WFF A ) ::_thesis: ( p is Element of CQC-WFF A implies 'not' p is Element of CQC-WFF A )
proof
assume A1: 'not' p is Element of CQC-WFF A ; ::_thesis: p is Element of CQC-WFF A
then Free ('not' p) = {} by Th4;
then A2: Free p = {} by QC_LANG3:55;
Fixed ('not' p) = {} by A1, Th4;
then Fixed p = {} by QC_LANG3:65;
hence p is Element of CQC-WFF A by A2, Th4; ::_thesis: verum
end;
assume p is Element of CQC-WFF A ; ::_thesis: 'not' p is Element of CQC-WFF A
then reconsider r = p as Element of CQC-WFF A ;
Fixed r = {} by Th4;
then A3: Fixed ('not' r) = {} by QC_LANG3:65;
Free r = {} by Th4;
then Free ('not' r) = {} by QC_LANG3:55;
hence 'not' p is Element of CQC-WFF A by A3, Th4; ::_thesis: verum
end;
theorem Th9: :: CQC_LANG:9
for A being QC-alphabet
for p, q being Element of QC-WFF A holds
( p '&' q is Element of CQC-WFF A iff ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds
( p '&' q is Element of CQC-WFF A iff ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) )
let p, q be Element of QC-WFF A; ::_thesis: ( p '&' q is Element of CQC-WFF A iff ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) )
thus ( p '&' q is Element of CQC-WFF A implies ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) ) ::_thesis: ( p is Element of CQC-WFF A & q is Element of CQC-WFF A implies p '&' q is Element of CQC-WFF A )
proof
assume A1: p '&' q is Element of CQC-WFF A ; ::_thesis: ( p is Element of CQC-WFF A & q is Element of CQC-WFF A )
then Fixed (p '&' q) = {} by Th4;
then A2: (Fixed p) \/ (Fixed q) = {} by QC_LANG3:67;
then A3: Fixed p = {} ;
Free (p '&' q) = {} by A1, Th4;
then A4: (Free p) \/ (Free q) = {} by QC_LANG3:57;
then Free p = {} ;
hence ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) by A4, A2, A3, Th4; ::_thesis: verum
end;
assume ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) ; ::_thesis: p '&' q is Element of CQC-WFF A
then reconsider r = p, s = q as Element of CQC-WFF A ;
Fixed r = {} by Th4;
then (Fixed r) \/ (Fixed s) = {} by Th4;
then A5: Fixed (r '&' s) = {} by QC_LANG3:67;
Free r = {} by Th4;
then (Free r) \/ (Free s) = {} by Th4;
then Free (r '&' s) = {} by QC_LANG3:57;
hence p '&' q is Element of CQC-WFF A by A5, Th4; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
:: original: VERUM
redefine func VERUM A -> Element of CQC-WFF A;
coherence
VERUM A is Element of CQC-WFF A by Th6;
let r be Element of CQC-WFF A;
:: original: 'not'
redefine func 'not' r -> Element of CQC-WFF A;
coherence
'not' r is Element of CQC-WFF A by Th8;
let s be Element of CQC-WFF A;
:: original: '&'
redefine funcr '&' s -> Element of CQC-WFF A;
coherence
r '&' s is Element of CQC-WFF A by Th9;
end;
theorem Th10: :: CQC_LANG:10
for A being QC-alphabet
for r, s being Element of CQC-WFF A holds r => s is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for r, s being Element of CQC-WFF A holds r => s is Element of CQC-WFF A
let r, s be Element of CQC-WFF A; ::_thesis: r => s is Element of CQC-WFF A
r => s = 'not' (r '&' ('not' s)) by QC_LANG2:def_2;
hence r => s is Element of CQC-WFF A ; ::_thesis: verum
end;
theorem Th11: :: CQC_LANG:11
for A being QC-alphabet
for r, s being Element of CQC-WFF A holds r 'or' s is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for r, s being Element of CQC-WFF A holds r 'or' s is Element of CQC-WFF A
let r, s be Element of CQC-WFF A; ::_thesis: r 'or' s is Element of CQC-WFF A
r 'or' s = 'not' (('not' r) '&' ('not' s)) by QC_LANG2:def_3;
hence r 'or' s is Element of CQC-WFF A ; ::_thesis: verum
end;
theorem Th12: :: CQC_LANG:12
for A being QC-alphabet
for r, s being Element of CQC-WFF A holds r <=> s is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for r, s being Element of CQC-WFF A holds r <=> s is Element of CQC-WFF A
let r, s be Element of CQC-WFF A; ::_thesis: r <=> s is Element of CQC-WFF A
r <=> s = (r => s) '&' (s => r) by QC_LANG2:def_4
.= ('not' (r '&' ('not' s))) '&' (s => r) by QC_LANG2:def_2
.= ('not' (r '&' ('not' s))) '&' ('not' (s '&' ('not' r))) by QC_LANG2:def_2 ;
hence r <=> s is Element of CQC-WFF A ; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let r, s be Element of CQC-WFF A;
:: original: =>
redefine funcr => s -> Element of CQC-WFF A;
coherence
r => s is Element of CQC-WFF A by Th10;
:: original: 'or'
redefine funcr 'or' s -> Element of CQC-WFF A;
coherence
r 'or' s is Element of CQC-WFF A by Th11;
:: original: <=>
redefine funcr <=> s -> Element of CQC-WFF A;
coherence
r <=> s is Element of CQC-WFF A by Th12;
end;
theorem Th13: :: CQC_LANG:13
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,p) is Element of CQC-WFF A iff p is Element of CQC-WFF A )
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,p) is Element of CQC-WFF A iff p is Element of CQC-WFF A )
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A holds
( All (x,p) is Element of CQC-WFF A iff p is Element of CQC-WFF A )
let p be Element of QC-WFF A; ::_thesis: ( All (x,p) is Element of CQC-WFF A iff p is Element of CQC-WFF A )
thus ( All (x,p) is Element of CQC-WFF A implies p is Element of CQC-WFF A ) ::_thesis: ( p is Element of CQC-WFF A implies All (x,p) is Element of CQC-WFF A )
proof
assume A1: All (x,p) is Element of CQC-WFF A ; ::_thesis: p is Element of CQC-WFF A
then Fixed (All (x,p)) = {} by Th4;
then A2: Fixed p = {} by QC_LANG3:68;
Free (All (x,p)) = {} by A1, Th4;
then Free p = {} by QC_LANG3:58;
hence p is Element of CQC-WFF A by A2, Th4; ::_thesis: verum
end;
assume A3: p is Element of CQC-WFF A ; ::_thesis: All (x,p) is Element of CQC-WFF A
then Fixed p = {} by Th4;
then A4: Fixed (All (x,p)) = {} by QC_LANG3:68;
Free p = {} by A3, Th4;
then Free (All (x,p)) = {} by QC_LANG3:58;
hence All (x,p) is Element of CQC-WFF A by A4, Th4; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let x be bound_QC-variable of A;
let r be Element of CQC-WFF A;
:: original: All
redefine func All (x,r) -> Element of CQC-WFF A;
coherence
All (x,r) is Element of CQC-WFF A by Th13;
end;
theorem Th14: :: CQC_LANG:14
for A being QC-alphabet
for x being bound_QC-variable of A
for r being Element of CQC-WFF A holds Ex (x,r) is Element of CQC-WFF A
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for r being Element of CQC-WFF A holds Ex (x,r) is Element of CQC-WFF A
let x be bound_QC-variable of A; ::_thesis: for r being Element of CQC-WFF A holds Ex (x,r) is Element of CQC-WFF A
let r be Element of CQC-WFF A; ::_thesis: Ex (x,r) is Element of CQC-WFF A
Ex (x,r) = 'not' (All (x,('not' r))) by QC_LANG2:def_5;
hence Ex (x,r) is Element of CQC-WFF A ; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let x be bound_QC-variable of A;
let r be Element of CQC-WFF A;
:: original: Ex
redefine func Ex (x,r) -> Element of CQC-WFF A;
coherence
Ex (x,r) is Element of CQC-WFF A by Th14;
end;
scheme :: CQC_LANG:sch 1
CQCInd{ F1() -> QC-alphabet , P1[ set ] } :
for r being Element of CQC-WFF F1() holds P1[r]
provided
A1: for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( P1[ VERUM F1()] & 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
defpred S1[ Element of QC-WFF F1()] means ( $1 is Element of CQC-WFF F1() implies P1[$1] );
A2: 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 A3: S1[p] ; ::_thesis: S1[ 'not' p]
assume 'not' p is Element of CQC-WFF F1() ; ::_thesis: P1[ 'not' p]
then p is Element of CQC-WFF F1() by Th8;
hence P1[ 'not' p] by A1, A3; ::_thesis: verum
end;
A4: 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 A5: ( S1[p] & S1[q] ) ; ::_thesis: S1[p '&' q]
assume p '&' q is Element of CQC-WFF F1() ; ::_thesis: P1[p '&' q]
then ( p is Element of CQC-WFF F1() & q is Element of CQC-WFF F1() ) by Th9;
hence P1[p '&' q] by A1, A5; ::_thesis: verum
end;
A6: 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]
assume A7: P ! l is Element of CQC-WFF F1() ; ::_thesis: P1[P ! l]
then A8: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables F1() ) } = {} by Th7;
{ (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables F1() ) } = {} by A7, Th7;
then l is CQC-variable_list of k,F1() by A8, Th5;
hence P1[P ! l] by A1; ::_thesis: verum
end;
A9: 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 A10: S1[p] ; ::_thesis: S1[ All (x,p)]
assume All (x,p) is Element of CQC-WFF F1() ; ::_thesis: P1[ All (x,p)]
then p is Element of CQC-WFF F1() by Th13;
hence P1[ All (x,p)] by A1, A10; ::_thesis: verum
end;
A11: S1[ VERUM F1()] by A1;
for p being Element of QC-WFF F1() holds S1[p] from QC_LANG1:sch_1(A6, A11, A2, A4, A9);
hence for r being Element of CQC-WFF F1() holds P1[r] ; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 2
CQCFuncEx{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5( set ) -> Element of F2(), F6( set , set ) -> Element of F2(), F7( set , set ) -> Element of F2() } :
ex F being Function of (CQC-WFF F1()),F2() st
( F . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() 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
deffunc H1( Element of QC-WFF F1(), Element of F2()) -> Element of F2() = F7((bound_in $1),$2);
deffunc H2( Element of QC-WFF F1()) -> Element of F2() = F4((the_arity_of (the_pred_symbol_of $1)),(the_pred_symbol_of $1),(the_arguments_of $1));
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 = H2(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = H1(p,F . (the_scope_of p)) ) ) ) ) from QC_LANG1:sch_3();
reconsider G = F | (CQC-WFF F1()) as Function of (CQC-WFF F1()),F2() by FUNCT_2:32;
take G ; ::_thesis: ( G . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) ) ) )
thus G . (VERUM F1()) = F3() by A1, FUNCT_1:49; ::_thesis: for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let r, s be Element of CQC-WFF F1(); ::_thesis: for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let x be bound_QC-variable of F1(); ::_thesis: for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let k be Element of NAT ; ::_thesis: for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let l be CQC-variable_list of k,F1(); ::_thesis: for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let P be QC-pred_symbol of k,F1(); ::_thesis: ( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
A2: the_arity_of P = k by QC_LANG1:11;
A3: P ! l is atomic by QC_LANG1:def_18;
then A4: ( the_arguments_of (P ! l) = l & the_pred_symbol_of (P ! l) = P ) by QC_LANG1:def_22, QC_LANG1:def_23;
thus G . (P ! l) = F . (P ! l) by FUNCT_1:49
.= F4(k,P,l) by A1, A3, A4, A2 ; ::_thesis: ( G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
set r9 = G . r;
set s9 = G . s;
A5: G . r = F . r by FUNCT_1:49;
A6: r '&' s is conjunctive by QC_LANG1:def_20;
then A7: ( the_left_argument_of (r '&' s) = r & the_right_argument_of (r '&' s) = s ) by QC_LANG1:def_25, QC_LANG1:def_26;
A8: 'not' r is negative by QC_LANG1:def_19;
then A9: the_argument_of ('not' r) = r by QC_LANG1:def_24;
thus G . ('not' r) = F . ('not' r) by FUNCT_1:49
.= F5((G . r)) by A1, A5, A8, A9 ; ::_thesis: ( G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
A10: G . s = F . s by FUNCT_1:49;
thus G . (r '&' s) = F . (r '&' s) by FUNCT_1:49
.= F6((G . r),(G . s)) by A1, A5, A10, A6, A7 ; ::_thesis: G . (All (x,r)) = F7(x,(G . r))
A11: All (x,r) is universal by QC_LANG1:def_21;
then A12: ( bound_in (All (x,r)) = x & the_scope_of (All (x,r)) = r ) by QC_LANG1:def_27, QC_LANG1:def_28;
thus G . (All (x,r)) = F . (All (x,r)) by FUNCT_1:49
.= F7(x,(G . r)) by A1, A5, A11, A12 ; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 3
CQCFuncUniq{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Function of (CQC-WFF F1()),F2(), F4() -> Function of (CQC-WFF F1()),F2(), F5() -> Element of F2(), F6( set , set , 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: ( F3() . (VERUM F1()) = F5() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F3() . (P ! l) = F6(k,P,l) & F3() . ('not' r) = F7((F3() . r)) & F3() . (r '&' s) = F8((F3() . r),(F3() . s)) & F3() . (All (x,r)) = F9(x,(F3() . r)) ) ) ) and
A2: ( F4() . (VERUM F1()) = F5() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F4() . (P ! l) = F6(k,P,l) & F4() . ('not' r) = F7((F4() . r)) & F4() . (r '&' s) = F8((F4() . r),(F4() . s)) & F4() . (All (x,r)) = F9(x,(F4() . r)) ) ) )
proof
defpred S1[ set ] means F3() . $1 = F4() . $1;
A3: for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( S1[ VERUM F1()] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
proof
let r, s be Element of CQC-WFF F1(); ::_thesis: for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( S1[ VERUM F1()] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
let x be bound_QC-variable of F1(); ::_thesis: for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( S1[ VERUM F1()] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
let k be Element of NAT ; ::_thesis: for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( S1[ VERUM F1()] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
let l be CQC-variable_list of k,F1(); ::_thesis: for P being QC-pred_symbol of k,F1() holds
( S1[ VERUM F1()] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
let P be QC-pred_symbol of k,F1(); ::_thesis: ( S1[ VERUM F1()] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
thus F3() . (VERUM F1()) = F4() . (VERUM F1()) by A1, A2; ::_thesis: ( S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
F3() . (P ! l) = F6(k,P,l) by A1;
hence F3() . (P ! l) = F4() . (P ! l) by A2; ::_thesis: ( ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
F3() . ('not' r) = F7((F3() . r)) by A1;
hence ( F3() . r = F4() . r implies F3() . ('not' r) = F4() . ('not' r) ) by A2; ::_thesis: ( ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) )
F3() . (r '&' s) = F8((F3() . r),(F3() . s)) by A1;
hence ( F3() . r = F4() . r & F3() . s = F4() . s implies F3() . (r '&' s) = F4() . (r '&' s) ) by A2; ::_thesis: ( S1[r] implies S1[ All (x,r)] )
F3() . (All (x,r)) = F9(x,(F3() . r)) by A1;
hence ( S1[r] implies S1[ All (x,r)] ) by A2; ::_thesis: verum
end;
for r being Element of CQC-WFF F1() holds S1[r] from CQC_LANG:sch_1(A3);
hence F3() = F4() by FUNCT_2:63; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 4
CQCDefcorrectness{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of CQC-WFF F1(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8( set , set ) -> Element of F2() } :
( ex d being Element of F2() ex F being Function of (CQC-WFF F1()),F2() st
( d = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ( for d1, d2 being Element of F2() st ex F being Function of (CQC-WFF F1()),F2() st
( d1 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ex F being Function of (CQC-WFF F1()),F2() st
( d2 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) holds
d1 = d2 ) )
proof
thus ex d being Element of F2() ex F being Function of (CQC-WFF F1()),F2() st
( d = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) ::_thesis: for d1, d2 being Element of F2() st ex F being Function of (CQC-WFF F1()),F2() st
( d1 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ex F being Function of (CQC-WFF F1()),F2() st
( d2 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) holds
d1 = d2
proof
consider F being Function of (CQC-WFF F1()),F2() such that
A1: ( F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) from CQC_LANG:sch_2();
take F . F3() ; ::_thesis: ex F being Function of (CQC-WFF F1()),F2() st
( F . F3() = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) )
take F ; ::_thesis: ( F . F3() = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) )
thus ( F . F3() = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) by A1; ::_thesis: verum
end;
let d1, d2 be Element of F2(); ::_thesis: ( ex F being Function of (CQC-WFF F1()),F2() st
( d1 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ex F being Function of (CQC-WFF F1()),F2() st
( d2 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) implies d1 = d2 )
given F1 being Function of (CQC-WFF F1()),F2() such that A2: d1 = F1 . F3() and
A3: ( F1 . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F1 . (P ! l) = F5(k,P,l) & F1 . ('not' r) = F6((F1 . r)) & F1 . (r '&' s) = F7((F1 . r),(F1 . s)) & F1 . (All (x,r)) = F8(x,(F1 . r)) ) ) ) ; ::_thesis: ( for F being Function of (CQC-WFF F1()),F2() holds
( not d2 = F . F3() or not F . (VERUM F1()) = F4() or ex r, s being Element of CQC-WFF F1() ex x being bound_QC-variable of F1() ex k being Element of NAT ex l being CQC-variable_list of k,F1() ex P being QC-pred_symbol of k,F1() st
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) implies not F . (All (x,r)) = F8(x,(F . r)) ) ) or d1 = d2 )
given F2 being Function of (CQC-WFF F1()),F2() such that A4: d2 = F2 . F3() and
A5: ( F2 . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() 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)) ) ) ) ; ::_thesis: d1 = d2
F1 = F2 from CQC_LANG:sch_3(A3, A5);
hence d1 = d2 by A2, A4; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 5
CQCDefVERUM{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8( set , set ) -> Element of F2() } :
F3((VERUM F1())) = F4()
provided
A1: for p being Element of CQC-WFF F1()
for d being Element of F2() holds
( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st
( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) )
proof
ex F being Function of (CQC-WFF F1()),F2() st
( F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) from CQC_LANG:sch_2();
hence F3((VERUM F1())) = F4() by A1; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 6
CQCDefatomic{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( set ) -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6() -> Element of NAT , F7() -> QC-pred_symbol of F6(),F1(), F8() -> CQC-variable_list of F6(),F1(), F9( set ) -> Element of F2(), F10( set , set ) -> Element of F2(), F11( set , set ) -> Element of F2() } :
F4((F7() ! F8())) = F5(F6(),F7(),F8())
provided
A1: for p being Element of CQC-WFF F1()
for d being Element of F2() holds
( d = F4(p) iff ex F being Function of (CQC-WFF F1()),F2() st
( d = F . p & F . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F9((F . r)) & F . (r '&' s) = F10((F . r),(F . s)) & F . (All (x,r)) = F11(x,(F . r)) ) ) ) )
proof
consider F being Function of (CQC-WFF F1()),F2() such that
A2: ( F . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F9((F . r)) & F . (r '&' s) = F10((F . r),(F . s)) & F . (All (x,r)) = F11(x,(F . r)) ) ) ) from CQC_LANG:sch_2();
F5(F6(),F7(),F8()) = F . (F7() ! F8()) by A2;
hence F4((F7() ! F8())) = F5(F6(),F7(),F8()) by A1, A2; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 7
CQCDefnegative{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7() -> Element of CQC-WFF F1(), F8( set , set ) -> Element of F2(), F9( set , set ) -> Element of F2() } :
F3(('not' F7())) = F6(F3(F7()))
provided
A1: for p being Element of CQC-WFF F1()
for d being Element of F2() holds
( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st
( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F8((F . r),(F . s)) & F . (All (x,r)) = F9(x,(F . r)) ) ) ) )
proof
consider G being Function of (CQC-WFF F1()),F2() such that
A2: F3(F7()) = G . F7() and
A3: ( G . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F5(k,P,l) & G . ('not' r) = F6((G . r)) & G . (r '&' s) = F8((G . r),(G . s)) & G . (All (x,r)) = F9(x,(G . r)) ) ) ) by A1;
consider F being Function of (CQC-WFF F1()),F2() such that
A4: ( F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F8((F . r),(F . s)) & F . (All (x,r)) = F9(x,(F . r)) ) ) ) from CQC_LANG:sch_2();
A5: F . ('not' F7()) = F6((F . F7())) by A4;
F = G from CQC_LANG:sch_3(A4, A3);
hence F3(('not' F7())) = F6(F3(F7())) by A1, A4, A5, A2; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 8
QCDefconjunctive{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8() -> Element of CQC-WFF F1(), F9() -> Element of CQC-WFF F1(), F10( set , set ) -> Element of F2() } :
F3((F8() '&' F9())) = F7(F3(F8()),F3(F9()))
provided
A1: for p being Element of CQC-WFF F1()
for d being Element of F2() holds
( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st
( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F10(x,(F . r)) ) ) ) )
proof
consider F2 being Function of (CQC-WFF F1()),F2() such that
A2: F3(F9()) = F2 . F9() and
A3: ( F2 . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() 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)) = F10(x,(F2 . r)) ) ) ) by A1;
consider F1 being Function of (CQC-WFF F1()),F2() such that
A4: F3(F8()) = F1 . F8() and
A5: ( F1 . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F1 . (P ! l) = F5(k,P,l) & F1 . ('not' r) = F6((F1 . r)) & F1 . (r '&' s) = F7((F1 . r),(F1 . s)) & F1 . (All (x,r)) = F10(x,(F1 . r)) ) ) ) by A1;
consider F being Function of (CQC-WFF F1()),F2() such that
A6: ( F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F10(x,(F . r)) ) ) ) from CQC_LANG:sch_2();
A7: F . (F8() '&' F9()) = F7((F . F8()),(F . F9())) by A6;
A8: F = F2 from CQC_LANG:sch_3(A6, A3);
F = F1 from CQC_LANG:sch_3(A6, A5);
hence F3((F8() '&' F9())) = F7(F3(F8()),F3(F9())) by A1, A6, A7, A4, A2, A8; ::_thesis: verum
end;
scheme :: CQC_LANG:sch 9
QCDefuniversal{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8( set , set ) -> Element of F2(), F9() -> bound_QC-variable of F1(), F10() -> Element of CQC-WFF F1() } :
F3((All (F9(),F10()))) = F8(F9(),F3(F10()))
provided
A1: for p being Element of CQC-WFF F1()
for d being Element of F2() holds
( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st
( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) )
proof
consider G being Function of (CQC-WFF F1()),F2() such that
A2: F3(F10()) = G . F10() and
A3: ( G . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F5(k,P,l) & G . ('not' r) = F6((G . r)) & G . (r '&' s) = F7((G . r),(G . s)) & G . (All (x,r)) = F8(x,(G . r)) ) ) ) by A1;
consider F being Function of (CQC-WFF F1()),F2() such that
A4: ( F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Element of NAT
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) from CQC_LANG:sch_2();
A5: F . (All (F9(),F10())) = F8(F9(),(F . F10())) by A4;
F = G from CQC_LANG:sch_3(A4, A3);
hence F3((All (F9(),F10()))) = F8(F9(),F3(F10())) by A1, A4, A5, A2; ::_thesis: verum
end;
Lm2: for A being QC-alphabet
for x being bound_QC-variable of A
for F1, F2 being Function of (QC-WFF A),(QC-WFF A) st ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for F1, F2 being Function of (QC-WFF A),(QC-WFF A) st ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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
let x be bound_QC-variable of A; ::_thesis: for F1, F2 being Function of (QC-WFF A),(QC-WFF A) st ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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
deffunc H1( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = $1 '&' $2;
deffunc H2( Element of QC-WFF A) -> Element of QC-WFF A = 'not' $1;
let F1, F2 be Function of (QC-WFF A),(QC-WFF A); ::_thesis: ( ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) ) implies F1 = F2 )
deffunc H3( Element of QC-WFF A) -> Element of QC-WFF A = (the_pred_symbol_of $1) ! (Subst ((the_arguments_of $1),((A a. 0) .--> x)));
deffunc H4( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = IFEQ ((bound_in $1),x,$1,(All ((bound_in $1),$2)));
assume for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = H3(q) ) & ( 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))))) ) ) ; ::_thesis: ( ex q being Element of QC-WFF A st
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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)) ) implies ( q is universal & not F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) or F1 = F2 )
then A1: for p, d1, d2 being Element of QC-WFF A holds
( ( p = VERUM A implies F1 . p = VERUM A ) & ( p is atomic implies F1 . p = H3(p) ) & ( p is negative & d1 = F1 . (the_argument_of p) implies F1 . p = H2(d1) ) & ( p is conjunctive & d1 = F1 . (the_left_argument_of p) & d2 = F1 . (the_right_argument_of p) implies F1 . p = H1(d1,d2) ) & ( p is universal & d1 = F1 . (the_scope_of p) implies F1 . p = H4(p,d1) ) ) ;
assume for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) ; ::_thesis: F1 = F2
then A2: for p, d1, d2 being Element of QC-WFF A holds
( ( p = VERUM A implies F2 . p = VERUM A ) & ( p is atomic implies F2 . p = H3(p) ) & ( p is negative & d1 = F2 . (the_argument_of p) implies F2 . p = H2(d1) ) & ( p is conjunctive & d1 = F2 . (the_left_argument_of p) & d2 = F2 . (the_right_argument_of p) implies F2 . p = H1(d1,d2) ) & ( p is universal & d1 = F2 . (the_scope_of p) implies F2 . p = H4(p,d1) ) ) ;
thus F1 = F2 from QC_LANG3:sch_1(A1, A2); ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
let x be bound_QC-variable of A;
funcp . x -> Element of QC-WFF A means :Def3: :: CQC_LANG:def 3
ex F being Function of (QC-WFF A),(QC-WFF A) st
( it = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 A ex F being Function of (QC-WFF A),(QC-WFF A) st
( b1 = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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
deffunc H1( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = IFEQ ((bound_in $1),x,$1,(All ((bound_in $1),$2)));
deffunc H2( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = $1 '&' $2;
deffunc H3( Element of QC-WFF A) -> Element of QC-WFF A = 'not' $1;
deffunc H4( Element of QC-WFF A) -> Element of QC-WFF A = (the_pred_symbol_of $1) ! (Subst ((the_arguments_of $1),((A a. 0) .--> x)));
consider F being Function of (QC-WFF A),(QC-WFF A) such that
A1: ( F . (VERUM A) = VERUM A & ( for p being Element of QC-WFF A holds
( ( p is atomic implies F . p = H4(p) ) & ( p is negative implies F . p = H3(F . (the_argument_of p)) ) & ( p is conjunctive implies F . p = H2(F . (the_left_argument_of p),F . (the_right_argument_of p)) ) & ( p is universal implies F . p = H1(p,F . (the_scope_of p)) ) ) ) ) from QC_LANG1:sch_3();
take F . p ; ::_thesis: ex F being Function of (QC-WFF A),(QC-WFF A) st
( F . p = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) ) )
take F ; ::_thesis: ( F . p = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) ) )
thus F . p = F . p ; ::_thesis: for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) )
thus for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of QC-WFF A st ex F being Function of (QC-WFF A),(QC-WFF A) st
( b1 = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 A),(QC-WFF A) st
( b2 = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 Def3 defines . CQC_LANG:def_3_:_
for A being QC-alphabet
for p being Element of QC-WFF A
for x being bound_QC-variable of A
for b4 being Element of QC-WFF A holds
( b4 = p . x iff ex F being Function of (QC-WFF A),(QC-WFF A) st
( b4 = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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 Th15: :: CQC_LANG:15
for A being QC-alphabet
for x being bound_QC-variable of A holds (VERUM A) . x = VERUM A
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A holds (VERUM A) . x = VERUM A
let x be bound_QC-variable of A; ::_thesis: (VERUM A) . x = VERUM A
ex F being Function of (QC-WFF A),(QC-WFF A) st
( (VERUM A) . x = F . (VERUM A) & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) ) ) by Def3;
hence (VERUM A) . x = VERUM A ; ::_thesis: verum
end;
theorem Th16: :: CQC_LANG:16
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is atomic holds
p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((A a. 0) .--> x)))
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is atomic holds
p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((A a. 0) .--> x)))
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st p is atomic holds
p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((A a. 0) .--> x)))
let p be Element of QC-WFF A; ::_thesis: ( p is atomic implies p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((A a. 0) .--> x))) )
ex F being Function of (QC-WFF A),(QC-WFF A) st
( p . x = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) ) ) by Def3;
hence ( p is atomic implies p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((A a. 0) .--> x))) ) ; ::_thesis: verum
end;
theorem Th17: :: CQC_LANG:17
for A being QC-alphabet
for k being Element of NAT
for x being bound_QC-variable of A
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for x being bound_QC-variable of A
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let k be Element of NAT ; ::_thesis: for x being bound_QC-variable of A
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let x be bound_QC-variable of A; ::_thesis: for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let P be QC-pred_symbol of k,A; ::_thesis: for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let l be QC-variable_list of k,A; ::_thesis: (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
reconsider P9 = P as QC-pred_symbol of A ;
A1: P ! l is atomic by QC_LANG1:def_18;
then ( the_arguments_of (P ! l) = l & the_pred_symbol_of (P ! l) = P9 ) by QC_LANG1:def_22, QC_LANG1:def_23;
hence (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x))) by A1, Th16; ::_thesis: verum
end;
theorem Th18: :: CQC_LANG:18
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is negative holds
p . x = 'not' ((the_argument_of p) . x)
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is negative holds
p . x = 'not' ((the_argument_of p) . x)
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st p is negative holds
p . x = 'not' ((the_argument_of p) . x)
let p be Element of QC-WFF A; ::_thesis: ( p is negative implies p . x = 'not' ((the_argument_of p) . x) )
consider F being Function of (QC-WFF A),(QC-WFF A) such that
A1: p . x = F . p and
A2: for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) by Def3;
consider G being Function of (QC-WFF A),(QC-WFF A) such that
A3: (the_argument_of p) . x = G . (the_argument_of p) and
A4: for q being Element of QC-WFF A holds
( G . (VERUM A) = VERUM A & ( q is atomic implies G . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies G . q = 'not' (G . (the_argument_of q)) ) & ( q is conjunctive implies G . q = (G . (the_left_argument_of q)) '&' (G . (the_right_argument_of q)) ) & ( q is universal implies G . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(G . (the_scope_of q))))) ) ) by Def3;
F = G by A2, A4, Lm2;
hence ( p is negative implies p . x = 'not' ((the_argument_of p) . x) ) by A1, A2, A3; ::_thesis: verum
end;
theorem Th19: :: CQC_LANG:19
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds ('not' p) . x = 'not' (p . x)
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds ('not' p) . x = 'not' (p . x)
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A holds ('not' p) . x = 'not' (p . x)
let p be Element of QC-WFF A; ::_thesis: ('not' p) . x = 'not' (p . x)
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 ('not' p) . x = 'not' (p . x) by A1, Th18; ::_thesis: verum
end;
theorem Th20: :: CQC_LANG:20
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is conjunctive holds
p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x)
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is conjunctive holds
p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x)
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st p is conjunctive holds
p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x)
let p be Element of QC-WFF A; ::_thesis: ( p is conjunctive implies p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x) )
consider F being Function of (QC-WFF A),(QC-WFF A) such that
A1: p . x = F . p and
A2: for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) by Def3;
consider F2 being Function of (QC-WFF A),(QC-WFF A) such that
A3: (the_right_argument_of p) . x = F2 . (the_right_argument_of p) and
A4: for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) by Def3;
A5: F2 = F by A2, A4, Lm2;
consider F1 being Function of (QC-WFF A),(QC-WFF A) such that
A6: (the_left_argument_of p) . x = F1 . (the_left_argument_of p) and
A7: for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) by Def3;
F1 = F by A2, A7, Lm2;
hence ( p is conjunctive implies p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x) ) by A1, A2, A6, A3, A5; ::_thesis: verum
end;
theorem Th21: :: CQC_LANG:21
for A being QC-alphabet
for x being bound_QC-variable of A
for p, q being Element of QC-WFF A holds (p '&' q) . x = (p . x) '&' (q . x)
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p, q being Element of QC-WFF A holds (p '&' q) . x = (p . x) '&' (q . x)
let x be bound_QC-variable of A; ::_thesis: for p, q being Element of QC-WFF A holds (p '&' q) . x = (p . x) '&' (q . x)
let p, q be Element of QC-WFF A; ::_thesis: (p '&' q) . x = (p . x) '&' (q . x)
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 (p '&' q) . x = (p . x) '&' (q . x) by A1, Th20; ::_thesis: verum
end;
Lm3: for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal holds
p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x))))
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal holds
p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x))))
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st p is universal holds
p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x))))
let p be Element of QC-WFF A; ::_thesis: ( p is universal implies p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) )
consider F being Function of (QC-WFF A),(QC-WFF A) such that
A1: p . x = F . p and
A2: for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A 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))))) ) ) by Def3;
consider G being Function of (QC-WFF A),(QC-WFF A) such that
A3: (the_scope_of p) . x = G . (the_scope_of p) and
A4: for q being Element of QC-WFF A holds
( G . (VERUM A) = VERUM A & ( q is atomic implies G . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies G . q = 'not' (G . (the_argument_of q)) ) & ( q is conjunctive implies G . q = (G . (the_left_argument_of q)) '&' (G . (the_right_argument_of q)) ) & ( q is universal implies G . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(G . (the_scope_of q))))) ) ) by Def3;
F = G by A2, A4, Lm2;
hence ( p is universal implies p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) ) by A1, A2, A3; ::_thesis: verum
end;
theorem Th22: :: CQC_LANG:22
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal & bound_in p = x holds
p . x = p
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal & bound_in p = x holds
p . x = p
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st p is universal & bound_in p = x holds
p . x = p
let p be Element of QC-WFF A; ::_thesis: ( p is universal & bound_in p = x implies p . x = p )
assume p is universal ; ::_thesis: ( not bound_in p = x or p . x = p )
then p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) by Lm3;
hence ( not bound_in p = x or p . x = p ) by FUNCOP_1:def_8; ::_thesis: verum
end;
theorem Th23: :: CQC_LANG:23
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal & bound_in p <> x holds
p . x = All ((bound_in p),((the_scope_of p) . x))
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal & bound_in p <> x holds
p . x = All ((bound_in p),((the_scope_of p) . x))
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st p is universal & bound_in p <> x holds
p . x = All ((bound_in p),((the_scope_of p) . x))
let p be Element of QC-WFF A; ::_thesis: ( p is universal & bound_in p <> x implies p . x = All ((bound_in p),((the_scope_of p) . x)) )
assume p is universal ; ::_thesis: ( not bound_in p <> x or p . x = All ((bound_in p),((the_scope_of p) . x)) )
then p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) by Lm3;
hence ( not bound_in p <> x or p . x = All ((bound_in p),((the_scope_of p) . x)) ) by FUNCOP_1:def_8; ::_thesis: verum
end;
theorem Th24: :: CQC_LANG:24
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds (All (x,p)) . x = All (x,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 (All (x,p)) . x = All (x,p)
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A holds (All (x,p)) . x = All (x,p)
let p be Element of QC-WFF A; ::_thesis: (All (x,p)) . x = All (x,p)
set q = All (x,p);
A1: All (x,p) is universal by QC_LANG1:def_21;
then bound_in (All (x,p)) = x by QC_LANG1:def_27;
hence (All (x,p)) . x = All (x,p) by A1, Th22; ::_thesis: verum
end;
theorem Th25: :: CQC_LANG:25
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A st x <> y holds
(All (x,p)) . y = All (x,(p . y))
proof
let A be QC-alphabet ; ::_thesis: for x, y being bound_QC-variable of A
for p being Element of QC-WFF A st x <> y holds
(All (x,p)) . y = All (x,(p . y))
let x, y be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st x <> y holds
(All (x,p)) . y = All (x,(p . y))
let p be Element of QC-WFF A; ::_thesis: ( x <> y implies (All (x,p)) . y = All (x,(p . y)) )
set q = 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 ( x <> y implies (All (x,p)) . y = All (x,(p . y)) ) by A1, Th23; ::_thesis: verum
end;
theorem Th26: :: CQC_LANG:26
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st Free p = {} holds
p . x = p
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st Free p = {} holds
p . x = p
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st Free p = {} holds
p . x = p
let p be Element of QC-WFF A; ::_thesis: ( Free p = {} implies p . x = p )
defpred S1[ Element of QC-WFF A] means ( Free $1 = {} implies $1 . x = $1 );
A1: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p] by Th19, QC_LANG3:55;
A2: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A3: ( ( Free p = {} implies p . x = p ) & ( Free q = {} implies q . x = q ) ) ; ::_thesis: S1[p '&' q]
assume Free (p '&' q) = {} ; ::_thesis: (p '&' q) . x = p '&' q
then (Free p) \/ (Free q) = {} by QC_LANG3:57;
hence (p '&' q) . x = p '&' q by A3, Th21; ::_thesis: verum
end;
A4: for k being Element of NAT
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S1[P ! l]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S1[P ! l]
let P be QC-pred_symbol of k,A; ::_thesis: for l being QC-variable_list of k,A holds S1[P ! l]
let l be QC-variable_list of k,A; ::_thesis: S1[P ! l]
assume A5: Free (P ! l) = {} ; ::_thesis: (P ! l) . x = P ! l
A6: now__::_thesis:_for_j_being_natural_number_st_1_<=_j_&_j_<=_len_l_holds_
(Subst_(l,((A_a._0)_.-->_x)))_._j_=_l_._j
let j be natural number ; ::_thesis: ( 1 <= j & j <= len l implies (Subst (l,((A a. 0) .--> x))) . j = l . j )
assume A7: ( 1 <= j & j <= len l ) ; ::_thesis: (Subst (l,((A a. 0) .--> x))) . j = l . j
A8: j in NAT by ORDINAL1:def_12;
now__::_thesis:_not_l_._j_=_A_a._0
assume l . j = A a. 0 ; ::_thesis: contradiction
then A a. 0 in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by A8, A7;
hence contradiction by A5, QC_LANG3:54; ::_thesis: verum
end;
hence (Subst (l,((A a. 0) .--> x))) . j = l . j by A8, A7, Th3; ::_thesis: verum
end;
len (Subst (l,((A a. 0) .--> x))) = len l by Def1;
then Subst (l,((A a. 0) .--> x)) = l by A6, FINSEQ_1:14;
hence (P ! l) . x = P ! l by Th17; ::_thesis: verum
end;
A9: for y being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
proof
let y be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ All (y,p)] )
assume A10: ( Free p = {} implies p . x = p ) ; ::_thesis: S1[ All (y,p)]
A11: ( x = y implies (All (y,p)) . x = All (y,p) ) by Th24;
assume Free (All (y,p)) = {} ; ::_thesis: (All (y,p)) . x = All (y,p)
hence (All (y,p)) . x = All (y,p) by A10, A11, Th25, QC_LANG3:58; ::_thesis: verum
end;
A12: S1[ VERUM A] by Th15;
for p being Element of QC-WFF A holds S1[p] from QC_LANG1:sch_1(A4, A12, A1, A2, A9);
hence ( Free p = {} implies p . x = p ) ; ::_thesis: verum
end;
theorem :: CQC_LANG:27
for A being QC-alphabet
for x being bound_QC-variable of A
for r being Element of CQC-WFF A holds r . x = r
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for r being Element of CQC-WFF A holds r . x = r
let x be bound_QC-variable of A; ::_thesis: for r being Element of CQC-WFF A holds r . x = r
let r be Element of CQC-WFF A; ::_thesis: r . x = r
Free r = {} by Th4;
hence r . x = r by Th26; ::_thesis: verum
end;
theorem :: CQC_LANG:28
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Fixed (p . x) = 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 (p . x) = Fixed p
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A holds Fixed (p . x) = Fixed p
let p be Element of QC-WFF A; ::_thesis: Fixed (p . x) = Fixed p
defpred S1[ Element of QC-WFF A] means Fixed ($1 . x) = Fixed $1;
A1: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
proof
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ 'not' p] )
assume A2: Fixed (p . x) = Fixed p ; ::_thesis: S1[ 'not' p]
thus Fixed (('not' p) . x) = Fixed ('not' (p . x)) by Th19
.= Fixed p by A2, QC_LANG3:65
.= Fixed ('not' p) by QC_LANG3:65 ; ::_thesis: verum
end;
A3: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A4: ( Fixed (p . x) = Fixed p & Fixed (q . x) = Fixed q ) ; ::_thesis: S1[p '&' q]
thus Fixed ((p '&' q) . x) = Fixed ((p . x) '&' (q . x)) by Th21
.= (Fixed p) \/ (Fixed q) by A4, QC_LANG3:67
.= Fixed (p '&' q) by QC_LANG3:67 ; ::_thesis: verum
end;
A5: for k being Element of NAT
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S1[P ! l]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S1[P ! l]
let P be QC-pred_symbol of k,A; ::_thesis: for l being QC-variable_list of k,A holds S1[P ! l]
let l be QC-variable_list of k,A; ::_thesis: S1[P ! l]
set F1 = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ;
set ll = Subst (l,((A a. 0) .--> x));
set F2 = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ;
A6: len l = len (Subst (l,((A a. 0) .--> x))) by Def1;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in__{__(l_._i)_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_<=_len_l_&_l_._i_in_fixed_QC-variables_A_)__}__implies_y_in__{__((Subst_(l,((A_a._0)_.-->_x)))_._i)_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_<=_len_(Subst_(l,((A_a._0)_.-->_x)))_&_(Subst_(l,((A_a._0)_.-->_x)))_._i_in_fixed_QC-variables_A_)__}__)_&_(_y_in__{__((Subst_(l,((A_a._0)_.-->_x)))_._i)_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_<=_len_(Subst_(l,((A_a._0)_.-->_x)))_&_(Subst_(l,((A_a._0)_.-->_x)))_._i_in_fixed_QC-variables_A_)__}__implies_y_in__{__(l_._i)_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_<=_len_l_&_l_._i_in_fixed_QC-variables_A_)__}__)_)
let y be set ; ::_thesis: ( ( y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) & ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ) )
thus ( y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) ::_thesis: ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } )
proof
assume y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ; ::_thesis: y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) }
then consider i being Element of NAT such that
A7: y = l . i and
A8: ( 1 <= i & i <= len l ) and
A9: l . i in fixed_QC-variables A ;
l . i <> A a. 0 by A9, QC_LANG3:32;
then (Subst (l,((A a. 0) .--> x))) . i = l . i by A8, Th3;
hence y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } by A6, A7, A8, A9; ::_thesis: verum
end;
assume y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ; ::_thesis: y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) }
then consider i being Element of NAT such that
A10: y = (Subst (l,((A a. 0) .--> x))) . i and
A11: ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) ) and
A12: (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ;
now__::_thesis:_not_l_._i_=_A_a._0
assume l . i = A a. 0 ; ::_thesis: contradiction
then (Subst (l,((A a. 0) .--> x))) . i = x by A6, A11, Th3;
hence contradiction by A12, Lm1; ::_thesis: verum
end;
then (Subst (l,((A a. 0) .--> x))) . i = l . i by A6, A11, Th3;
hence y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by A6, A10, A11, A12; ::_thesis: verum
end;
then A13: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } by TARSKI:1;
( Fixed (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } & Fixed (P ! (Subst (l,((A a. 0) .--> x)))) = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) by QC_LANG3:64;
hence S1[P ! l] by A13, Th17; ::_thesis: verum
end;
A14: for y being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
proof
let y be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ All (y,p)] )
assume A15: Fixed (p . x) = Fixed p ; ::_thesis: S1[ All (y,p)]
now__::_thesis:_(_x_<>_y_implies_Fixed_((All_(y,p))_._x)_=_Fixed_(All_(y,p))_)
assume x <> y ; ::_thesis: Fixed ((All (y,p)) . x) = Fixed (All (y,p))
hence Fixed ((All (y,p)) . x) = Fixed (All (y,(p . x))) by Th25
.= Fixed p by A15, QC_LANG3:68
.= Fixed (All (y,p)) by QC_LANG3:68 ;
::_thesis: verum
end;
hence S1[ All (y,p)] by Th24; ::_thesis: verum
end;
A16: S1[ VERUM A] by Th15;
for p being Element of QC-WFF A holds S1[p] from QC_LANG1:sch_1(A5, A16, A1, A3, A14);
hence Fixed (p . x) = Fixed p ; ::_thesis: verum
end;
begin
theorem :: CQC_LANG:29
for i, j, k being set holds (i,j) :-> k = [i,j] .--> k ;
theorem :: CQC_LANG:30
for i, j, k being set holds ((i,j) :-> k) . (i,j) = k by FUNCT_4:80;
theorem :: CQC_LANG:31
for a, b, c being set holds (a,a) --> (b,c) = a .--> c by FUNCT_4:81;
theorem :: CQC_LANG:32
for f being Function
for a, b, c being set st a <> c holds
(f +* (a .--> b)) . c = f . c by FUNCT_4:83;
theorem :: CQC_LANG:33
for f being Function
for a, b, c, d being set st a <> b holds
( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d ) by FUNCT_4:84;