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

definition
func vSUB -> set equals :: SUBSTUT1:def 1
PFuncs bound_QC-variables ,bound_QC-variables ;
coherence
PFuncs bound_QC-variables ,bound_QC-variables is set
;
end;

:: deftheorem defines vSUB SUBSTUT1:def 1 :
vSUB = PFuncs bound_QC-variables ,bound_QC-variables ;

registration
cluster vSUB -> non empty ;
coherence
not vSUB is empty
;
end;

definition
mode CQC_Substitution is Element of vSUB ;
end;

registration
cluster vSUB -> non empty functional ;
coherence
vSUB is functional
;
end;

definition
let Sub be CQC_Substitution;
func @ Sub -> PartFunc of bound_QC-variables , bound_QC-variables equals :: SUBSTUT1:def 2
Sub;
coherence
Sub is PartFunc of bound_QC-variables , bound_QC-variables
by PARTFUN1:121;
end;

:: deftheorem defines @ SUBSTUT1:def 2 :
for Sub being CQC_Substitution holds @ Sub = Sub;

theorem Th1: :: SUBSTUT1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set
for Sub being CQC_Substitution st a in dom Sub holds
Sub . a in bound_QC-variables
proof end;

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

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

definition
let l be FinSequence of bound_QC-variables ;
func @ l -> FinSequence of QC-variables equals :: SUBSTUT1:def 4
l;
coherence
l is FinSequence of QC-variables
proof end;
end;

:: deftheorem defines @ SUBSTUT1:def 4 :
for l being FinSequence of bound_QC-variables holds @ l = l;

definition
let l be FinSequence of bound_QC-variables ;
let Sub be CQC_Substitution;
func CQC_Subst l,Sub -> FinSequence of bound_QC-variables equals :: SUBSTUT1:def 5
CQC_Subst (@ l),Sub;
coherence
CQC_Subst (@ l),Sub is FinSequence of bound_QC-variables
proof end;
end;

:: deftheorem defines CQC_Subst SUBSTUT1:def 5 :
for l being FinSequence of bound_QC-variables
for Sub being CQC_Substitution holds CQC_Subst l,Sub = CQC_Subst (@ l),Sub;

definition
let Sub be CQC_Substitution;
let X be set ;
:: original: |
redefine func Sub | X -> CQC_Substitution;
coherence
Sub | X is CQC_Substitution
proof end;
end;

registration
cluster finite Element of vSUB ;
existence
ex b1 being CQC_Substitution st b1 is finite
proof end;
end;

definition
let x be bound_QC-variable;
let p be QC-formula;
let Sub be CQC_Substitution;
func RestrictSub x,p,Sub -> finite CQC_Substitution equals :: SUBSTUT1:def 6
Sub | { y where y is bound_QC-variable : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
coherence
Sub | { y where y is bound_QC-variable : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } is finite CQC_Substitution
proof end;
end;

:: deftheorem defines RestrictSub SUBSTUT1:def 6 :
for x being bound_QC-variable
for p being QC-formula
for Sub being CQC_Substitution holds RestrictSub x,p,Sub = Sub | { y where y is bound_QC-variable : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;

definition
let l1 be FinSequence of QC-variables ;
func Bound_Vars l1 -> Subset of bound_QC-variables equals :: SUBSTUT1:def 7
{ (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) } ;
coherence
{ (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) } is Subset of bound_QC-variables
proof end;
end;

:: deftheorem defines Bound_Vars SUBSTUT1:def 7 :
for l1 being FinSequence of QC-variables holds Bound_Vars l1 = { (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) } ;

definition
let p be QC-formula;
func Bound_Vars p -> Subset of bound_QC-variables means :Def8: :: SUBSTUT1:def 8
ex F being Function of QC-WFF , bool bound_QC-variables st
( it = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) );
correctness
existence
ex b1 being Subset of bound_QC-variables ex F being Function of QC-WFF , bool bound_QC-variables st
( b1 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) )
;
uniqueness
for b1, b2 being Subset of bound_QC-variables st ex F being Function of QC-WFF , bool bound_QC-variables st
( b1 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) & ex F being Function of QC-WFF , bool bound_QC-variables st
( b2 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines Bound_Vars SUBSTUT1:def 8 :
for p being QC-formula
for b2 being Subset of bound_QC-variables holds
( b2 = Bound_Vars p iff ex F being Function of QC-WFF , bool bound_QC-variables st
( b2 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) );

Lm1: for p being QC-formula holds
( Bound_Vars VERUM = {} bound_QC-variables & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
proof end;

theorem :: SUBSTUT1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Bound_Vars VERUM = {} by Lm1;

theorem :: SUBSTUT1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is atomic holds
Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1;

theorem :: SUBSTUT1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is negative holds
Bound_Vars p = Bound_Vars (the_argument_of p) by Lm1;

theorem :: SUBSTUT1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is conjunctive holds
Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by Lm1;

theorem :: SUBSTUT1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being QC-formula st p is universal holds
Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by Lm1;

registration
let p be QC-formula;
cluster Bound_Vars p -> finite ;
coherence
Bound_Vars p is finite
proof end;
end;

definition
let p be QC-formula;
func Dom_Bound_Vars p -> finite Subset of NAT equals :: SUBSTUT1:def 9
{ i where i is Nat : x. i in Bound_Vars p } ;
coherence
{ i where i is Nat : x. i in Bound_Vars p } is finite Subset of NAT
proof end;
end;

:: deftheorem defines Dom_Bound_Vars SUBSTUT1:def 9 :
for p being QC-formula holds Dom_Bound_Vars p = { i where i is Nat : x. i in Bound_Vars p } ;

definition
let finSub be finite CQC_Substitution;
func Sub_Var finSub -> finite Subset of NAT equals :: SUBSTUT1:def 10
{ i where i is Nat : x. i in rng finSub } ;
coherence
{ i where i is Nat : x. i in rng finSub } is finite Subset of NAT
proof end;
end;

:: deftheorem defines Sub_Var SUBSTUT1:def 10 :
for finSub being finite CQC_Substitution holds Sub_Var finSub = { i where i is Nat : x. i in rng finSub } ;

definition
let p be QC-formula;
let finSub be finite CQC_Substitution;
func NSub p,finSub -> non empty Subset of NAT equals :: SUBSTUT1:def 11
NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));
coherence
NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of NAT
proof end;
end;

:: deftheorem defines NSub SUBSTUT1:def 11 :
for p being QC-formula
for finSub being finite CQC_Substitution holds NSub p,finSub = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

definition
let finSub be finite CQC_Substitution;
let p be QC-formula;
func upVar finSub,p -> Nat equals :: SUBSTUT1:def 12
min (NSub p,finSub);
coherence
min (NSub p,finSub) is Nat
;
end;

:: deftheorem defines upVar SUBSTUT1:def 12 :
for finSub being finite CQC_Substitution
for p being QC-formula holds upVar finSub,p = min (NSub p,finSub);

definition
let x be bound_QC-variable;
let p be QC-formula;
let finSub be finite CQC_Substitution;
assume A1: ex Sub being CQC_Substitution st finSub = RestrictSub x,(All x,p),Sub ;
func ExpandSub x,p,finSub -> CQC_Substitution equals :: SUBSTUT1:def 13
finSub \/ {[x,(x. (upVar finSub,p))]} if x in rng finSub
otherwise finSub \/ {[x,x]};
coherence
( ( x in rng finSub implies finSub \/ {[x,(x. (upVar finSub,p))]} is CQC_Substitution ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution ) )
proof end;
consistency
for b1 being CQC_Substitution holds verum
;
end;

:: deftheorem defines ExpandSub SUBSTUT1:def 13 :
for x being bound_QC-variable
for p being QC-formula
for finSub being finite CQC_Substitution st ex Sub being CQC_Substitution st finSub = RestrictSub x,(All x,p),Sub holds
( ( x in rng finSub implies ExpandSub x,p,finSub = finSub \/ {[x,(x. (upVar finSub,p))]} ) & ( not x in rng finSub implies ExpandSub x,p,finSub = finSub \/ {[x,x]} ) );

definition
let p be QC-formula;
let Sub be CQC_Substitution;
let b be set ;
pred p,Sub PQSub b means :Def14: :: SUBSTUT1:def 14
( ( p is universal implies b = ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub) ) & ( not p is universal implies b = {} ) );
end;

:: deftheorem Def14 defines PQSub SUBSTUT1:def 14 :
for p being QC-formula
for Sub being CQC_Substitution
for b being set holds
( p,Sub PQSub b iff ( ( p is universal implies b = ExpandSub (bound_in p),(the_scope_of p),(RestrictSub (bound_in p),p,Sub) ) & ( not p is universal implies b = {} ) ) );

definition
func QSub -> Function means :: SUBSTUT1:def 15
for a being set holds
( a in it iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) );
existence
ex b1 being Function st
for a being set holds
( a in b1 iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) )
proof end;
uniqueness
for b1, b2 being Function st ( for a being set holds
( a in b1 iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being set holds
( a in b2 iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines QSub SUBSTUT1:def 15 :
for b1 being Function holds
( b1 = QSub iff for a being set holds
( a in b1 iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) );

theorem Th7: :: SUBSTUT1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( [:QC-WFF ,vSUB :] is Subset of [:([:NAT ,NAT :] * ),vSUB :] & ( for k being Nat
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :] ) & ( for e being Element of vSUB holds [<*[0,0]*>,e] in [:QC-WFF ,vSUB :] ) & ( for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] holds
[(<*[1,0]*> ^ p),e] in [:QC-WFF ,vSUB :] ) & ( for p, q being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in [:QC-WFF ,vSUB :] & [q,e] in [:QC-WFF ,vSUB :] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:QC-WFF ,vSUB :] ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:QC-WFF ,vSUB :] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:QC-WFF ,vSUB :] ) )
proof end;

definition
let IT be set ;
attr IT is QC-Sub-closed means :Def16: :: SUBSTUT1:def 16
( IT is Subset of [:([:NAT ,NAT :] * ),vSUB :] & ( for k being Nat
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in IT holds
[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in IT & [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) );
end;

:: deftheorem Def16 defines QC-Sub-closed SUBSTUT1:def 16 :
for IT being set holds
( IT is QC-Sub-closed iff ( IT is Subset of [:([:NAT ,NAT :] * ),vSUB :] & ( for k being Nat
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in IT holds
[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,e] in IT & [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :]
for e being Element of vSUB st [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) ) );

registration
cluster non empty QC-Sub-closed set ;
existence
ex b1 being set st
( b1 is QC-Sub-closed & not b1 is empty )
proof end;
end;

Lm2: for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT ,NAT :]
proof end;

Lm3: for k, l being Nat
for e being Element of vSUB holds [<*[k,l]*>,e] in [:([:NAT ,NAT :] * ),vSUB :]
proof end;

Lm4: for k being Nat
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:([:NAT ,NAT :] * ),vSUB :]
proof end;

definition
func QC-Sub-WFF -> non empty set means :Def17: :: SUBSTUT1:def 17
( it is QC-Sub-closed & ( for D being non empty set st D is QC-Sub-closed holds
it c= D ) );
existence
ex b1 being non empty set st
( b1 is QC-Sub-closed & ( for D being non empty set st D is QC-Sub-closed holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being non empty set st b1 is QC-Sub-closed & ( for D being non empty set st D is QC-Sub-closed holds
b1 c= D ) & b2 is QC-Sub-closed & ( for D being non empty set st D is QC-Sub-closed holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def 17 :
for b1 being non empty set holds
( b1 = QC-Sub-WFF iff ( b1 is QC-Sub-closed & ( for D being non empty set st D is QC-Sub-closed holds
b1 c= D ) ) );

theorem Th8: :: SUBSTUT1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF ex p being QC-formula ex e being Element of vSUB st S = [p,e]
proof end;

registration
cluster QC-Sub-WFF -> non empty QC-Sub-closed ;
coherence
QC-Sub-WFF is QC-Sub-closed
by Def17;
end;

definition
let P be QC-pred_symbol;
let l be FinSequence of QC-variables ;
let e be Element of vSUB ;
assume A1: the_arity_of P = len l ;
func Sub_P P,l,e -> Element of QC-Sub-WFF equals :Def18: :: SUBSTUT1:def 18
[(P ! l),e];
coherence
[(P ! l),e] is Element of QC-Sub-WFF
proof end;
end;

:: deftheorem Def18 defines Sub_P SUBSTUT1:def 18 :
for P being QC-pred_symbol
for l being FinSequence of QC-variables
for e being Element of vSUB st the_arity_of P = len l holds
Sub_P P,l,e = [(P ! l),e];

theorem Th9: :: SUBSTUT1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for e being Element of vSUB
for k being Nat
for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds Sub_P P,ll,e = [(P ! ll),e]
proof end;

definition
let S be Element of QC-Sub-WFF ;
attr S is Sub_VERUM means :Def19: :: SUBSTUT1:def 19
ex e being Element of vSUB st S = [VERUM ,e];
end;

:: deftheorem Def19 defines Sub_VERUM SUBSTUT1:def 19 :
for S being Element of QC-Sub-WFF holds
( S is Sub_VERUM iff ex e being Element of vSUB st S = [VERUM ,e] );

definition
let S be Element of QC-Sub-WFF ;
:: original: `1
redefine func S `1 -> Element of QC-WFF ;
coherence
S `1 is Element of QC-WFF
proof end;
:: original: `2
redefine func S `2 -> Element of vSUB ;
coherence
S `2 is Element of vSUB
proof end;
end;

theorem Th10: :: SUBSTUT1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF holds S = [(S `1 ),(S `2 )]
proof end;

definition
let S be Element of QC-Sub-WFF ;
func Sub_not S -> Element of QC-Sub-WFF equals :: SUBSTUT1:def 20
[('not' (S `1 )),(S `2 )];
coherence
[('not' (S `1 )),(S `2 )] is Element of QC-Sub-WFF
proof end;
end;

:: deftheorem defines Sub_not SUBSTUT1:def 20 :
for S being Element of QC-Sub-WFF holds Sub_not S = [('not' (S `1 )),(S `2 )];

definition
let S, S' be Element of QC-Sub-WFF ;
assume A1: S `2 = S' `2 ;
func Sub_& S,S' -> Element of QC-Sub-WFF equals :Def21: :: SUBSTUT1:def 21
[((S `1 ) '&' (S' `1 )),(S `2 )];
coherence
[((S `1 ) '&' (S' `1 )),(S `2 )] is Element of QC-Sub-WFF
proof end;
end;

:: deftheorem Def21 defines Sub_& SUBSTUT1:def 21 :
for S, S' being Element of QC-Sub-WFF st S `2 = S' `2 holds
Sub_& S,S' = [((S `1 ) '&' (S' `1 )),(S `2 )];

definition
let B be Element of [:QC-Sub-WFF ,bound_QC-variables :];
:: original: `1
redefine func B `1 -> Element of QC-Sub-WFF ;
coherence
B `1 is Element of QC-Sub-WFF
by MCART_1:10;
:: original: `2
redefine func B `2 -> Element of bound_QC-variables ;
coherence
B `2 is Element of bound_QC-variables
by MCART_1:10;
end;

definition
let B be Element of [:QC-Sub-WFF ,bound_QC-variables :];
attr B is quantifiable means :Def22: :: SUBSTUT1:def 22
ex e being Element of vSUB st (B `1 ) `2 = QSub . [(All (B `2 ),((B `1 ) `1 )),e];
end;

:: deftheorem Def22 defines quantifiable SUBSTUT1:def 22 :
for B being Element of [:QC-Sub-WFF ,bound_QC-variables :] holds
( B is quantifiable iff ex e being Element of vSUB st (B `1 ) `2 = QSub . [(All (B `2 ),((B `1 ) `1 )),e] );

definition
let B be Element of [:QC-Sub-WFF ,bound_QC-variables :];
assume A1: B is quantifiable ;
mode second_Q_comp of B -> Element of vSUB means :Def23: :: SUBSTUT1:def 23
(B `1 ) `2 = QSub . [(All (B `2 ),((B `1 ) `1 )),it];
existence
ex b1 being Element of vSUB st (B `1 ) `2 = QSub . [(All (B `2 ),((B `1 ) `1 )),b1]
by A1, Def22;
end;

:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def 23 :
for B being Element of [:QC-Sub-WFF ,bound_QC-variables :] st B is quantifiable holds
for b2 being Element of vSUB holds
( b2 is second_Q_comp of B iff (B `1 ) `2 = QSub . [(All (B `2 ),((B `1 ) `1 )),b2] );

definition
let B be Element of [:QC-Sub-WFF ,bound_QC-variables :];
let SQ be second_Q_comp of B;
assume A1: B is quantifiable ;
func Sub_All B,SQ -> Element of QC-Sub-WFF equals :Def24: :: SUBSTUT1:def 24
[(All (B `2 ),((B `1 ) `1 )),SQ];
coherence
[(All (B `2 ),((B `1 ) `1 )),SQ] is Element of QC-Sub-WFF
proof end;
end;

:: deftheorem Def24 defines Sub_All SUBSTUT1:def 24 :
for B being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All B,SQ = [(All (B `2 ),((B `1 ) `1 )),SQ];

definition
let S be Element of QC-Sub-WFF ;
let x be bound_QC-variable;
:: original: [
redefine func [S,x] -> Element of [:QC-Sub-WFF ,bound_QC-variables :];
coherence
[S,x] is Element of [:QC-Sub-WFF ,bound_QC-variables :]
proof end;
end;

scheme :: SUBSTUT1:sch 1
SubQCInd{ P1[ Element of QC-Sub-WFF ] } :
for S being Element of QC-Sub-WFF holds P1[S]
provided
A1: for k being Nat
for P being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds P1[ Sub_P P,ll,e] and
A2: for S being Element of QC-Sub-WFF st S is Sub_VERUM holds
P1[S] and
A3: for S being Element of QC-Sub-WFF st P1[S] holds
P1[ Sub_not S] and
A4: for S, S' being Element of QC-Sub-WFF st S `2 = S' `2 & P1[S] & P1[S'] holds
P1[ Sub_& S,S'] and
A5: for x being bound_QC-variable
for S being Element of QC-Sub-WFF
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All [S,x],SQ]
proof end;

definition
let S be Element of QC-Sub-WFF ;
attr S is Sub_atomic means :Def25: :: SUBSTUT1:def 25
ex k being Nat ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st S = Sub_P P,ll,e;
end;

:: deftheorem Def25 defines Sub_atomic SUBSTUT1:def 25 :
for S being Element of QC-Sub-WFF holds
( S is Sub_atomic iff ex k being Nat ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st S = Sub_P P,ll,e );

theorem Th11: :: SUBSTUT1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_atomic holds
S `1 is atomic
proof end;

registration
let k be Nat;
let P be QC-pred_symbol of k;
let ll be QC-variable_list of k;
let e be Element of vSUB ;
cluster Sub_P P,ll,e -> Sub_atomic ;
coherence
Sub_P P,ll,e is Sub_atomic
by Def25;
end;

definition
let S be Element of QC-Sub-WFF ;
attr S is Sub_negative means :Def26: :: SUBSTUT1:def 26
ex S' being Element of QC-Sub-WFF st S = Sub_not S';
attr S is Sub_conjunctive means :Def27: :: SUBSTUT1:def 27
ex S1, S2 being Element of QC-Sub-WFF st
( S = Sub_& S1,S2 & S1 `2 = S2 `2 );
end;

:: deftheorem Def26 defines Sub_negative SUBSTUT1:def 26 :
for S being Element of QC-Sub-WFF holds
( S is Sub_negative iff ex S' being Element of QC-Sub-WFF st S = Sub_not S' );

:: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def 27 :
for S being Element of QC-Sub-WFF holds
( S is Sub_conjunctive iff ex S1, S2 being Element of QC-Sub-WFF st
( S = Sub_& S1,S2 & S1 `2 = S2 `2 ) );

definition
let A be set ;
attr A is Sub_universal means :Def28: :: SUBSTUT1:def 28
ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B is quantifiable );
end;

:: deftheorem Def28 defines Sub_universal SUBSTUT1:def 28 :
for A being set holds
( A is Sub_universal iff ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B is quantifiable ) );

theorem Th12: :: SUBSTUT1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF holds
( S is Sub_VERUM or S is Sub_atomic or S is Sub_negative or S is Sub_conjunctive or S is Sub_universal )
proof end;

definition
let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_atomic ;
func Sub_the_arguments_of S -> FinSequence of QC-variables means :Def29: :: SUBSTUT1:def 29
ex k being Nat ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st
( it = ll & S = Sub_P P,ll,e );
existence
ex b1 being FinSequence of QC-variables ex k being Nat ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st
( b1 = ll & S = Sub_P P,ll,e )
proof end;
uniqueness
for b1, b2 being FinSequence of QC-variables st ex k being Nat ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st
( b1 = ll & S = Sub_P P,ll,e ) & ex k being Nat ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st
( b2 = ll & S = Sub_P P,ll,e ) holds
b1 = b2
proof end;
end;

:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def 29 :
for S being Element of QC-Sub-WFF st S is Sub_atomic holds
for b2 being FinSequence of QC-variables holds
( b2 = Sub_the_arguments_of S iff ex k being Nat ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st
( b2 = ll & S = Sub_P P,ll,e ) );

definition
let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_negative ;
func Sub_the_argument_of S -> Element of QC-Sub-WFF means :Def30: :: SUBSTUT1:def 30
S = Sub_not it;
existence
ex b1 being Element of QC-Sub-WFF st S = Sub_not b1
by A1, Def26;
uniqueness
for b1, b2 being Element of QC-Sub-WFF st S = Sub_not b1 & S = Sub_not b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def 30 :
for S being Element of QC-Sub-WFF st S is Sub_negative holds
for b2 being Element of QC-Sub-WFF holds
( b2 = Sub_the_argument_of S iff S = Sub_not b2 );

definition
let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_conjunctive ;
func Sub_the_left_argument_of S -> Element of QC-Sub-WFF means :Def31: :: SUBSTUT1:def 31
ex S' being Element of QC-Sub-WFF st
( S = Sub_& it,S' & it `2 = S' `2 );
existence
ex b1, S' being Element of QC-Sub-WFF st
( S = Sub_& b1,S' & b1 `2 = S' `2 )
by A1, Def27;
uniqueness
for b1, b2 being Element of QC-Sub-WFF st ex S' being Element of QC-Sub-WFF st
( S = Sub_& b1,S' & b1 `2 = S' `2 ) & ex S' being Element of QC-Sub-WFF st
( S = Sub_& b2,S' & b2 `2 = S' `2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def 31 :
for S being Element of QC-Sub-WFF st S is Sub_conjunctive holds
for b2 being Element of QC-Sub-WFF holds
( b2 = Sub_the_left_argument_of S iff ex S' being Element of QC-Sub-WFF st
( S = Sub_& b2,S' & b2 `2 = S' `2 ) );

definition
let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_conjunctive ;
func Sub_the_right_argument_of S -> Element of QC-Sub-WFF means :Def32: :: SUBSTUT1:def 32
ex S' being Element of QC-Sub-WFF st
( S = Sub_& S',it & S' `2 = it `2 );
existence
ex b1, S' being Element of QC-Sub-WFF st
( S = Sub_& S',b1 & S' `2 = b1 `2 )
proof end;
uniqueness
for b1, b2 being Element of QC-Sub-WFF st ex S' being Element of QC-Sub-WFF st
( S = Sub_& S',b1 & S' `2 = b1 `2 ) & ex S' being Element of QC-Sub-WFF st
( S = Sub_& S',b2 & S' `2 = b2 `2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def 32 :
for S being Element of QC-Sub-WFF st S is Sub_conjunctive holds
for b2 being Element of QC-Sub-WFF holds
( b2 = Sub_the_right_argument_of S iff ex S' being Element of QC-Sub-WFF st
( S = Sub_& S',b2 & S' `2 = b2 `2 ) );

definition
let A be set ;
assume A1: A is Sub_universal ;
func Sub_the_bound_of A -> bound_QC-variable means :: SUBSTUT1:def 33
ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = it & B is quantifiable );
existence
ex b1 being bound_QC-variable ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = b1 & B is quantifiable )
proof end;
uniqueness
for b1, b2 being bound_QC-variable st ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = b1 & B is quantifiable ) & ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = b2 & B is quantifiable ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Sub_the_bound_of SUBSTUT1:def 33 :
for A being set st A is Sub_universal holds
for b2 being bound_QC-variable holds
( b2 = Sub_the_bound_of A iff ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = b2 & B is quantifiable ) );

definition
let A be set ;
assume A1: A is Sub_universal ;
func Sub_the_scope_of A -> Element of QC-Sub-WFF means :Def34: :: SUBSTUT1:def 34
ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `1 = it & B is quantifiable );
existence
ex b1 being Element of QC-Sub-WFF ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `1 = b1 & B is quantifiable )
proof end;
uniqueness
for b1, b2 being Element of QC-Sub-WFF st ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `1 = b1 & B is quantifiable ) & ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `1 = b2 & B is quantifiable ) holds
b1 = b2
proof end;
end;

:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def 34 :
for A being set st A is Sub_universal holds
for b2 being Element of QC-Sub-WFF holds
( b2 = Sub_the_scope_of A iff ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `1 = b2 & B is quantifiable ) );

registration
let S be Element of QC-Sub-WFF ;
cluster Sub_not S -> Sub_negative ;
coherence
Sub_not S is Sub_negative
proof end;
end;

theorem Th13: :: SUBSTUT1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 holds
Sub_& S1,S2 is Sub_conjunctive
proof end;

theorem Th14: :: SUBSTUT1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All B,SQ is Sub_universal
proof end;

theorem :: SUBSTUT1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, S' being Element of QC-Sub-WFF st Sub_not S = Sub_not S' holds
S = S'
proof end;

theorem :: SUBSTUT1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF holds Sub_the_argument_of (Sub_not S) = S by Def30;

theorem Th17: :: SUBSTUT1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2, S1', S2' being Element of QC-Sub-WFF st S1 `2 = S2 `2 & S1' `2 = S2' `2 & Sub_& S1,S2 = Sub_& S1',S2' holds
( S1 = S1' & S2 = S2' )
proof end;

theorem Th18: :: SUBSTUT1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 holds
Sub_the_left_argument_of (Sub_& S1,S2) = S1
proof end;

theorem Th19: :: SUBSTUT1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 holds
Sub_the_right_argument_of (Sub_& S1,S2) = S2
proof end;

theorem Th20: :: SUBSTUT1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B1, B2 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ1 being second_Q_comp of B1
for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All B1,SQ1 = Sub_All B2,SQ2 holds
B1 = B2
proof end;

theorem Th21: :: SUBSTUT1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_the_scope_of (Sub_All B,SQ) = B `1
proof end;

scheme :: SUBSTUT1:sch 2
SubQCInd2{ P1[ Element of QC-Sub-WFF ] } :
for S being Element of QC-Sub-WFF holds P1[S]
provided
A1: for S being Element of QC-Sub-WFF holds
( ( S is Sub_atomic implies P1[S] ) & ( S is Sub_VERUM implies P1[S] ) & ( S is Sub_negative & P1[ Sub_the_argument_of S] implies P1[S] ) & ( S is Sub_conjunctive & P1[ Sub_the_left_argument_of S] & P1[ Sub_the_right_argument_of S] implies P1[S] ) & ( S is Sub_universal & P1[ Sub_the_scope_of S] implies P1[S] ) )
proof end;

theorem Th22: :: SUBSTUT1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_negative holds
len (@ ((Sub_the_argument_of S) `1 )) < len (@ (S `1 ))
proof end;

theorem Th23: :: SUBSTUT1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_conjunctive holds
( len (@ ((Sub_the_left_argument_of S) `1 )) < len (@ (S `1 )) & len (@ ((Sub_the_right_argument_of S) `1 )) < len (@ (S `1 )) )
proof end;

theorem Th24: :: SUBSTUT1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_universal holds
len (@ ((Sub_the_scope_of S) `1 )) < len (@ (S `1 ))
proof end;

theorem Th25: :: SUBSTUT1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF holds
( ( S is Sub_VERUM implies ((@ (S `1 )) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Nat st (@ (S `1 )) . 1 is QC-pred_symbol of k ) & ( S is Sub_negative implies ((@ (S `1 )) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1 )) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1 )) . 1) `1 = 3 ) )
proof end;

theorem Th26: :: SUBSTUT1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_atomic holds
( ((@ (S `1 )) . 1) `1 <> 0 & ((@ (S `1 )) . 1) `1 <> 1 & ((@ (S `1 )) . 1) `1 <> 2 & ((@ (S `1 )) . 1) `1 <> 3 )
proof end;

theorem Th27: :: SUBSTUT1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF holds
( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is Sub_VERUM & S is Sub_atomic ) & not ( S is Sub_VERUM & S is Sub_negative ) & not ( S is Sub_VERUM & S is Sub_conjunctive ) & not ( S is Sub_VERUM & S is Sub_universal ) )
proof end;

scheme :: SUBSTUT1:sch 3
SubFuncEx{ F1() -> non empty set , F2() -> Element of F1(), F3( Element of QC-Sub-WFF ) -> Element of F1(), F4( Element of F1()) -> Element of F1(), F5( Element of F1(), Element of F1()) -> Element of F1(), F6( Element of QC-Sub-WFF , Element of F1()) -> Element of F1() } :
ex F being Function of QC-Sub-WFF ,F1() st
for S being Element of QC-Sub-WFF
for d1, d2 being Element of F1() holds
( ( S is Sub_VERUM implies F . S = F2() ) & ( S is Sub_atomic implies F . S = F3(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F4(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F5(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F6(S,d1) ) )
proof end;

scheme :: SUBSTUT1:sch 4
SubQCFuncUniq{ F1() -> non empty set , F2() -> Function of QC-Sub-WFF ,F1(), F3() -> Function of QC-Sub-WFF ,F1(), F4() -> Element of F1(), F5( set ) -> Element of F1(), F6( set ) -> Element of F1(), F7( set , set ) -> Element of F1(), F8( set , set ) -> Element of F1() } :
F2() = F3()
provided
A1: for S being Element of QC-Sub-WFF
for d1, d2 being Element of F1() holds
( ( S is Sub_VERUM implies F2() . S = F4() ) & ( S is Sub_atomic implies F2() . S = F5(S) ) & ( S is Sub_negative & d1 = F2() . (Sub_the_argument_of S) implies F2() . S = F6(d1) ) & ( S is Sub_conjunctive & d1 = F2() . (Sub_the_left_argument_of S) & d2 = F2() . (Sub_the_right_argument_of S) implies F2() . S = F7(d1,d2) ) & ( S is Sub_universal & d1 = F2() . (Sub_the_scope_of S) implies F2() . S = F8(S,d1) ) ) and
A2: for S being Element of QC-Sub-WFF
for d1, d2 being Element of F1() holds
( ( S is Sub_VERUM implies F3() . S = F4() ) & ( S is Sub_atomic implies F3() . S = F5(S) ) & ( S is Sub_negative & d1 = F3() . (Sub_the_argument_of S) implies F3() . S = F6(d1) ) & ( S is Sub_conjunctive & d1 = F3() . (Sub_the_left_argument_of S) & d2 = F3() . (Sub_the_right_argument_of S) implies F3() . S = F7(d1,d2) ) & ( S is Sub_universal & d1 = F3() . (Sub_the_scope_of S) implies F3() . S = F8(S,d1) ) )
proof end;

definition
let S be Element of QC-Sub-WFF ;
func @ S -> Element of [:QC-WFF ,vSUB :] equals :: SUBSTUT1:def 35
S;
coherence
S is Element of [:QC-WFF ,vSUB :]
proof end;
end;

:: deftheorem defines @ SUBSTUT1:def 35 :
for S being Element of QC-Sub-WFF holds @ S = S;

definition
let Z be Element of [:QC-WFF ,vSUB :];
:: original: `1
redefine func Z `1 -> Element of QC-WFF ;
coherence
Z `1 is Element of QC-WFF
proof end;
:: original: `2
redefine func Z `2 -> CQC_Substitution;
coherence
Z `2 is CQC_Substitution
proof end;
end;

definition
let Z be Element of [:QC-WFF ,vSUB :];
func S_Bound Z -> bound_QC-variable equals :: SUBSTUT1:def 36
x. (upVar (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )),(the_scope_of (Z `1 ))) if bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 ))
otherwise bound_in (Z `1 );
coherence
( ( bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )) implies x. (upVar (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )),(the_scope_of (Z `1 ))) is bound_QC-variable ) & ( not bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )) implies bound_in (Z `1 ) is bound_QC-variable ) )
;
consistency
for b1 being bound_QC-variable holds verum
;
end;

:: deftheorem defines S_Bound SUBSTUT1:def 36 :
for Z being Element of [:QC-WFF ,vSUB :] holds
( ( bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )) implies S_Bound Z = x. (upVar (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )),(the_scope_of (Z `1 ))) ) & ( not bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )) implies S_Bound Z = bound_in (Z `1 ) ) );

definition
let S be Element of QC-Sub-WFF ;
let p be QC-formula;
func Quant S,p -> Element of QC-WFF equals :: SUBSTUT1:def 37
All (S_Bound (@ S)),p;
coherence
All (S_Bound (@ S)),p is Element of QC-WFF
;
end;

:: deftheorem defines Quant SUBSTUT1:def 37 :
for S being Element of QC-Sub-WFF
for p being QC-formula holds Quant S,p = All (S_Bound (@ S)),p;

Lm5: for F1, F2 being Function of QC-Sub-WFF , QC-WFF st ( for S being Element of QC-Sub-WFF holds
( ( S is Sub_VERUM implies F1 . S = VERUM ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1 )) ! (CQC_Subst (Sub_the_arguments_of S),(S `2 )) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant S,(F1 . (Sub_the_scope_of S)) ) ) ) & ( for S being Element of QC-Sub-WFF holds
( ( S is Sub_VERUM implies F2 . S = VERUM ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1 )) ! (CQC_Subst (Sub_the_arguments_of S),(S `2 )) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant S,(F2 . (Sub_the_scope_of S)) ) ) ) holds
F1 = F2
proof end;

definition
let S be Element of QC-Sub-WFF ;
func CQC_Sub S -> Element of QC-WFF means :Def38: :: SUBSTUT1:def 38
ex F being Function of QC-Sub-WFF , QC-WFF st
( it = F . S & ( for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F . S' = VERUM ) & ( S' is Sub_atomic implies F . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F . S' = 'not' (F . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F . S' = (F . (Sub_the_left_argument_of S')) '&' (F . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F . S' = Quant S',(F . (Sub_the_scope_of S')) ) ) ) );
existence
ex b1 being Element of QC-WFF ex F being Function of QC-Sub-WFF , QC-WFF st
( b1 = F . S & ( for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F . S' = VERUM ) & ( S' is Sub_atomic implies F . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F . S' = 'not' (F . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F . S' = (F . (Sub_the_left_argument_of S')) '&' (F . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F . S' = Quant S',(F . (Sub_the_scope_of S')) ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of QC-WFF st ex F being Function of QC-Sub-WFF , QC-WFF st
( b1 = F . S & ( for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F . S' = VERUM ) & ( S' is Sub_atomic implies F . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F . S' = 'not' (F . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F . S' = (F . (Sub_the_left_argument_of S')) '&' (F . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F . S' = Quant S',(F . (Sub_the_scope_of S')) ) ) ) ) & ex F being Function of QC-Sub-WFF , QC-WFF st
( b2 = F . S & ( for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F . S' = VERUM ) & ( S' is Sub_atomic implies F . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F . S' = 'not' (F . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F . S' = (F . (Sub_the_left_argument_of S')) '&' (F . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F . S' = Quant S',(F . (Sub_the_scope_of S')) ) ) ) ) holds
b1 = b2
by Lm5;
end;

:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def 38 :
for S being Element of QC-Sub-WFF
for b2 being Element of QC-WFF holds
( b2 = CQC_Sub S iff ex F being Function of QC-Sub-WFF , QC-WFF st
( b2 = F . S & ( for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F . S' = VERUM ) & ( S' is Sub_atomic implies F . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F . S' = 'not' (F . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F . S' = (F . (Sub_the_left_argument_of S')) '&' (F . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F . S' = Quant S',(F . (Sub_the_scope_of S')) ) ) ) ) );

theorem Th28: :: SUBSTUT1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_negative holds
CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S))
proof end;

theorem Th29: :: SUBSTUT1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)
proof end;

theorem Th30: :: SUBSTUT1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_conjunctive holds
CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S))
proof end;

theorem Th31: :: SUBSTUT1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 holds
CQC_Sub (Sub_& S1,S2) = (CQC_Sub S1) '&' (CQC_Sub S2)
proof end;

theorem Th32: :: SUBSTUT1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_universal holds
CQC_Sub S = Quant S,(CQC_Sub (Sub_the_scope_of S))
proof end;

definition
func CQC-Sub-WFF -> Subset of QC-Sub-WFF equals :: SUBSTUT1:def 39
{ S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } ;
coherence
{ S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } is Subset of QC-Sub-WFF
proof end;
end;

:: deftheorem defines CQC-Sub-WFF SUBSTUT1:def 39 :
CQC-Sub-WFF = { S where S is Element of QC-Sub-WFF : S `1 is Element of CQC-WFF } ;

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

theorem Th33: :: SUBSTUT1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st S is Sub_VERUM holds
CQC_Sub S is Element of CQC-WFF
proof end;

Lm6: for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k holds the_pred_symbol_of (P ! ll) = P
proof end;

theorem Th34: :: SUBSTUT1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for h being FinSequence holds
( h is CQC-variable_list of k iff ( h is FinSequence of bound_QC-variables & len h = k ) )
proof end;

theorem Th35: :: SUBSTUT1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for e being Element of vSUB holds CQC_Sub (Sub_P P,ll,e) is Element of CQC-WFF
proof end;

theorem Th36: :: SUBSTUT1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of QC-Sub-WFF st CQC_Sub S is Element of CQC-WFF holds
CQC_Sub (Sub_not S) is Element of CQC-WFF
proof end;

theorem Th37: :: SUBSTUT1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF & CQC_Sub S2 is Element of CQC-WFF holds
CQC_Sub (Sub_& S1,S2) is Element of CQC-WFF
proof end;

theorem Th38: :: SUBSTUT1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of QC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF & [S,x] is quantifiable holds
CQC_Sub (Sub_All [S,x],xSQ) is Element of CQC-WFF
proof end;

scheme :: SUBSTUT1:sch 5
SubCQCInd{ P1[ set ] } :
for S being Element of CQC-Sub-WFF holds P1[S]
provided
A1: for S, S' being Element of CQC-Sub-WFF
for x being bound_QC-variable
for SQ being second_Q_comp of [S,x]
for k being Nat
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k
for e being Element of vSUB holds
( P1[ Sub_P P,ll,e] & ( S is Sub_VERUM implies P1[S] ) & ( P1[S] implies P1[ Sub_not S] ) & ( S `2 = S' `2 & P1[S] & P1[S'] implies P1[ Sub_& S,S'] ) & ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All [S,x],SQ] ) )
proof end;

definition
let S be Element of CQC-Sub-WFF ;
:: original: CQC_Sub
redefine func CQC_Sub S -> Element of CQC-WFF ;
coherence
CQC_Sub S is Element of CQC-WFF
proof end;
end;