:: by Patrick Braselmann and Peter Koepke

::

:: Received September 25, 2004

:: Copyright (c) 2004-2016 Association of Mizar Users

definition
end;

:: deftheorem defines vSUB SUBSTUT1:def 1 :

for A being QC-alphabet holds vSUB A = PFuncs ((bound_QC-variables A),(bound_QC-variables A));

for A being QC-alphabet holds vSUB A = PFuncs ((bound_QC-variables A),(bound_QC-variables A));

registration
end;

registration
end;

definition

let A be QC-alphabet ;

let Sub be CQC_Substitution of A;

Sub is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by PARTFUN1:47;

end;
let Sub be CQC_Substitution of A;

func @ Sub -> PartFunc of (bound_QC-variables A),(bound_QC-variables A) equals :: SUBSTUT1:def 2

Sub;

coherence Sub;

Sub is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by PARTFUN1:47;

:: deftheorem defines @ SUBSTUT1:def 2 :

for A being QC-alphabet

for Sub being CQC_Substitution of A holds @ Sub = Sub;

for A being QC-alphabet

for Sub being CQC_Substitution of A holds @ Sub = Sub;

theorem Th1: :: SUBSTUT1:1

for A being QC-alphabet

for a being object

for Sub being CQC_Substitution of A st a in dom Sub holds

Sub . a in bound_QC-variables A

for a being object

for Sub being CQC_Substitution of A st a in dom Sub holds

Sub . a in bound_QC-variables A

proof end;

definition

let A be QC-alphabet ;

let l be FinSequence of QC-variables A;

let Sub be CQC_Substitution of A;

ex b_{1} being FinSequence of QC-variables A st

( len b_{1} = len l & ( for k being Nat st 1 <= k & k <= len l holds

( ( l . k in dom Sub implies b_{1} . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b_{1} . k = l . k ) ) ) )

for b_{1}, b_{2} being FinSequence of QC-variables A st len b_{1} = len l & ( for k being Nat st 1 <= k & k <= len l holds

( ( l . k in dom Sub implies b_{1} . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b_{1} . k = l . k ) ) ) & len b_{2} = len l & ( for k being Nat st 1 <= k & k <= len l holds

( ( l . k in dom Sub implies b_{2} . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b_{2} . k = l . k ) ) ) holds

b_{1} = b_{2}

end;
let l be FinSequence of QC-variables A;

let Sub be CQC_Substitution of A;

func CQC_Subst (l,Sub) -> FinSequence of QC-variables A 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 ( 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 ) ) ) );

ex b

( len b

( ( l . k in dom Sub implies b

proof end;

uniqueness for b

( ( l . k in dom Sub implies b

( ( l . k in dom Sub implies b

b

proof end;

:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def 3 :

for A being QC-alphabet

for l being FinSequence of QC-variables A

for Sub being CQC_Substitution of A

for b_{4} being FinSequence of QC-variables A holds

( b_{4} = CQC_Subst (l,Sub) iff ( len b_{4} = len l & ( for k being Nat st 1 <= k & k <= len l holds

( ( l . k in dom Sub implies b_{4} . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b_{4} . k = l . k ) ) ) ) );

for A being QC-alphabet

for l being FinSequence of QC-variables A

for Sub being CQC_Substitution of A

for b

( b

( ( l . k in dom Sub implies b

definition

let A be QC-alphabet ;

let l be FinSequence of bound_QC-variables A;

coherence

l is FinSequence of QC-variables A

end;
let l be FinSequence of bound_QC-variables A;

coherence

l is FinSequence of QC-variables A

proof end;

:: deftheorem defines @ SUBSTUT1:def 4 :

for A being QC-alphabet

for l being FinSequence of bound_QC-variables A holds @ l = l;

for A being QC-alphabet

for l being FinSequence of bound_QC-variables A holds @ l = l;

definition

let A be QC-alphabet ;

let l be FinSequence of bound_QC-variables A;

let Sub be CQC_Substitution of A;

CQC_Subst ((@ l),Sub) is FinSequence of bound_QC-variables A

end;
let l be FinSequence of bound_QC-variables A;

let Sub be CQC_Substitution of A;

func CQC_Subst (l,Sub) -> FinSequence of bound_QC-variables A equals :: SUBSTUT1:def 5

CQC_Subst ((@ l),Sub);

coherence CQC_Subst ((@ l),Sub);

CQC_Subst ((@ l),Sub) is FinSequence of bound_QC-variables A

proof end;

:: deftheorem defines CQC_Subst SUBSTUT1:def 5 :

for A being QC-alphabet

for l being FinSequence of bound_QC-variables A

for Sub being CQC_Substitution of A holds CQC_Subst (l,Sub) = CQC_Subst ((@ l),Sub);

for A being QC-alphabet

for l being FinSequence of bound_QC-variables A

for Sub being CQC_Substitution of A holds CQC_Subst (l,Sub) = CQC_Subst ((@ l),Sub);

definition

let A be QC-alphabet ;

let Sub be CQC_Substitution of A;

let X be set ;

:: original: |

redefine func Sub | X -> CQC_Substitution of A;

coherence

Sub | X is CQC_Substitution of A

end;
let Sub be CQC_Substitution of A;

let X be set ;

:: original: |

redefine func Sub | X -> CQC_Substitution of A;

coherence

Sub | X is CQC_Substitution of A

proof end;

registration
end;

definition

let A be QC-alphabet ;

let x be bound_QC-variable of A;

let p be QC-formula of A;

let Sub be CQC_Substitution of A;

Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } is finite CQC_Substitution of A

end;
let x be bound_QC-variable of A;

let p be QC-formula of A;

let Sub be CQC_Substitution of A;

func RestrictSub (x,p,Sub) -> finite CQC_Substitution of A equals :: SUBSTUT1:def 6

Sub | { y where y is bound_QC-variable of A : ( 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 of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;

Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } is finite CQC_Substitution of A

proof end;

:: deftheorem defines RestrictSub SUBSTUT1:def 6 :

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A

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

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A

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

definition

let A be QC-alphabet ;

let l1 be FinSequence of QC-variables A;

{ (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A)

end;
let l1 be FinSequence of QC-variables A;

func Bound_Vars l1 -> Subset of (bound_QC-variables A) equals :: SUBSTUT1:def 7

{ (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ;

coherence { (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ;

{ (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A)

proof end;

:: deftheorem defines Bound_Vars SUBSTUT1:def 7 :

for A being QC-alphabet

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

for A being QC-alphabet

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

definition

let A be QC-alphabet ;

let p be QC-formula of A;

existence

ex b_{1} being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( b_{1} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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 b_{1}, b_{2} being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( b_{1} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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 A),(bool (bound_QC-variables A)) st

( b_{2} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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

b_{1} = b_{2};

end;
let p be QC-formula of A;

func Bound_Vars p -> Subset of (bound_QC-variables A) means :Def8: :: SUBSTUT1:def 8

ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( it = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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 ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( it = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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)} ) ) ) );

existence

ex b

( b

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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 b

( b

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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 A),(bool (bound_QC-variables A)) st

( b

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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

b

proof end;

:: deftheorem Def8 defines Bound_Vars SUBSTUT1:def 8 :

for A being QC-alphabet

for p being QC-formula of A

for b_{3} being Subset of (bound_QC-variables A) holds

( b_{3} = Bound_Vars p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( b_{3} = F . p & ( for p being Element of QC-WFF A

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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)} ) ) ) ) );

for A being QC-alphabet

for p being QC-formula of A

for b

( b

( b

for d1, d2 being Subset of (bound_QC-variables A) holds

( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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 A being QC-alphabet

for p being QC-formula of A holds

( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( 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:3

for A being QC-alphabet

for p being QC-formula of A st p is atomic holds

Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1;

for p being QC-formula of A st p is atomic holds

Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1;

theorem :: SUBSTUT1:4

for A being QC-alphabet

for p being QC-formula of A st p is negative holds

Bound_Vars p = Bound_Vars (the_argument_of p) by Lm1;

for p being QC-formula of A st p is negative holds

Bound_Vars p = Bound_Vars (the_argument_of p) by Lm1;

theorem :: SUBSTUT1:5

for A being QC-alphabet

for p being QC-formula of A st p is conjunctive holds

Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by Lm1;

for p being QC-formula of A 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

for A being QC-alphabet

for p being QC-formula of A st p is universal holds

Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by Lm1;

for p being QC-formula of A st p is universal holds

Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by Lm1;

registration
end;

definition

let A be QC-alphabet ;

let p be QC-formula of A;

{ s where s is QC-symbol of A : x. s in Bound_Vars p } is finite Subset of (QC-symbols A)

end;
let p be QC-formula of A;

func Dom_Bound_Vars p -> finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 9

{ s where s is QC-symbol of A : x. s in Bound_Vars p } ;

coherence { s where s is QC-symbol of A : x. s in Bound_Vars p } ;

{ s where s is QC-symbol of A : x. s in Bound_Vars p } is finite Subset of (QC-symbols A)

proof end;

:: deftheorem defines Dom_Bound_Vars SUBSTUT1:def 9 :

for A being QC-alphabet

for p being QC-formula of A holds Dom_Bound_Vars p = { s where s is QC-symbol of A : x. s in Bound_Vars p } ;

for A being QC-alphabet

for p being QC-formula of A holds Dom_Bound_Vars p = { s where s is QC-symbol of A : x. s in Bound_Vars p } ;

definition

let A be QC-alphabet ;

let finSub be finite CQC_Substitution of A;

{ s where s is QC-symbol of A : x. s in rng finSub } is finite Subset of (QC-symbols A)

end;
let finSub be finite CQC_Substitution of A;

func Sub_Var finSub -> finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 10

{ s where s is QC-symbol of A : x. s in rng finSub } ;

coherence { s where s is QC-symbol of A : x. s in rng finSub } ;

{ s where s is QC-symbol of A : x. s in rng finSub } is finite Subset of (QC-symbols A)

proof end;

:: deftheorem defines Sub_Var SUBSTUT1:def 10 :

for A being QC-alphabet

for finSub being finite CQC_Substitution of A holds Sub_Var finSub = { s where s is QC-symbol of A : x. s in rng finSub } ;

for A being QC-alphabet

for finSub being finite CQC_Substitution of A holds Sub_Var finSub = { s where s is QC-symbol of A : x. s in rng finSub } ;

Lm2: for X, Y being set st card X in card Y holds

Y \ X <> {}

proof end;

definition

let A be QC-alphabet ;

let p be QC-formula of A;

let finSub be finite CQC_Substitution of A;

NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A)

end;
let p be QC-formula of A;

let finSub be finite CQC_Substitution of A;

func NSub (p,finSub) -> non empty Subset of (QC-symbols A) equals :: SUBSTUT1:def 11

NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

coherence NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A)

proof end;

:: deftheorem defines NSub SUBSTUT1:def 11 :

for A being QC-alphabet

for p being QC-formula of A

for finSub being finite CQC_Substitution of A holds NSub (p,finSub) = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

for A being QC-alphabet

for p being QC-formula of A

for finSub being finite CQC_Substitution of A holds NSub (p,finSub) = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

definition

let A be QC-alphabet ;

let finSub be finite CQC_Substitution of A;

let p be QC-formula of A;

coherence

the Element of NSub (p,finSub) is QC-symbol of A ;

end;
let finSub be finite CQC_Substitution of A;

let p be QC-formula of A;

coherence

the Element of NSub (p,finSub) is QC-symbol of A ;

:: deftheorem defines upVar SUBSTUT1:def 12 :

for A being QC-alphabet

for finSub being finite CQC_Substitution of A

for p being QC-formula of A holds upVar (finSub,p) = the Element of NSub (p,finSub);

for A being QC-alphabet

for finSub being finite CQC_Substitution of A

for p being QC-formula of A holds upVar (finSub,p) = the Element of NSub (p,finSub);

definition

let A be QC-alphabet ;

let x be bound_QC-variable of A;

let p be QC-formula of A;

let finSub be finite CQC_Substitution of A;

assume A1: ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) ;

( ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) )

for b_{1} being CQC_Substitution of A holds verum
;

end;
let x be bound_QC-variable of A;

let p be QC-formula of A;

let finSub be finite CQC_Substitution of A;

assume A1: ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) ;

func ExpandSub (x,p,finSub) -> CQC_Substitution of A equals :: SUBSTUT1:def 13

finSub \/ {[x,(x. (upVar (finSub,p)))]} if x in rng finSub

otherwise finSub \/ {[x,x]};

coherence finSub \/ {[x,(x. (upVar (finSub,p)))]} if x in rng finSub

otherwise finSub \/ {[x,x]};

( ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) )

proof end;

consistency for b

:: deftheorem defines ExpandSub SUBSTUT1:def 13 :

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A

for finSub being finite CQC_Substitution of A st ex Sub being CQC_Substitution of A 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]} ) );

for A being QC-alphabet

for x being bound_QC-variable of A

for p being QC-formula of A

for finSub being finite CQC_Substitution of A st ex Sub being CQC_Substitution of A 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 A be QC-alphabet ;

let p be QC-formula of A;

let Sub be CQC_Substitution of A;

let b be object ;

end;
let p be QC-formula of A;

let Sub be CQC_Substitution of A;

let b be object ;

pred p,Sub PQSub b means :: 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 = {} ) );

( ( 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 = {} ) );

:: deftheorem defines PQSub SUBSTUT1:def 14 :

for A being QC-alphabet

for p being QC-formula of A

for Sub being CQC_Substitution of A

for b being object 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 = {} ) ) );

for A being QC-alphabet

for p being QC-formula of A

for Sub being CQC_Substitution of A

for b being object 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

let A be QC-alphabet ;

ex b_{1} being Function st

for a being object holds

( a in b_{1} iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st

( a = [[p,Sub],b] & p,Sub PQSub b ) )

for b_{1}, b_{2} being Function st ( for a being object holds

( a in b_{1} iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st

( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being object holds

( a in b_{2} iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st

( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) holds

b_{1} = b_{2}

end;
func QSub A -> Function means :: SUBSTUT1:def 15

for a being object holds

( a in it iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st

( a = [[p,Sub],b] & p,Sub PQSub b ) );

existence for a being object holds

( a in it iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st

( a = [[p,Sub],b] & p,Sub PQSub b ) );

ex b

for a being object holds

( a in b

( a = [[p,Sub],b] & p,Sub PQSub b ) )

proof end;

uniqueness for b

( a in b

( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being object holds

( a in b

( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) holds

b

proof end;

:: deftheorem defines QSub SUBSTUT1:def 15 :

for A being QC-alphabet

for b_{2} being Function holds

( b_{2} = QSub A iff for a being object holds

( a in b_{2} iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st

( a = [[p,Sub],b] & p,Sub PQSub b ) ) );

for A being QC-alphabet

for b

( b

( a in b

( a = [[p,Sub],b] & p,Sub PQSub b ) ) );

theorem Th7: :: SUBSTUT1:7

for A being QC-alphabet holds

( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat

for p being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A

for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds

[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds

[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A

for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds

[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )

( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat

for p being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A

for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds

[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds

[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A

for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds

[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )

proof end;

definition

let A be QC-alphabet ;

let IT be set ;

end;
let IT be set ;

attr IT is A -Sub-closed means :Def16: :: SUBSTUT1:def 16

( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat

for p being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A

for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT holds

[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds

[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A

for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds

[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) );

( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat

for p being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A

for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT holds

[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds

[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A

for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds

[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) );

:: deftheorem Def16 defines -Sub-closed SUBSTUT1:def 16 :

for A being QC-alphabet

for IT being set holds

( IT is A -Sub-closed iff ( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat

for p being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A

for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT holds

[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds

[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A

for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds

[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) ) );

for A being QC-alphabet

for IT being set holds

( IT is A -Sub-closed iff ( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat

for p being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A

for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT holds

[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds

[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A

for p being FinSequence of [:NAT,(QC-symbols A):]

for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds

[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) ) );

registration

let A be QC-alphabet ;

existence

ex b_{1} being set st

( b_{1} is A -Sub-closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

Lm3: for A being QC-alphabet

for x being bound_QC-variable of A

for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]

proof end;

Lm4: for A being QC-alphabet

for k being Nat

for l being QC-symbol of A

for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]

proof end;

Lm5: for A being QC-alphabet

for k being Nat

for p being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A

for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]

proof end;

definition

let A be QC-alphabet ;

ex b_{1} being non empty set st

( b_{1} is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds

b_{1} c= D ) )

for b_{1}, b_{2} being non empty set st b_{1} is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds

b_{1} c= D ) & b_{2} is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds

b_{2} c= D ) holds

b_{1} = b_{2}

end;
func QC-Sub-WFF A -> non empty set means :Def17: :: SUBSTUT1:def 17

( it is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds

it c= D ) );

existence ( it is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def 17 :

for A being QC-alphabet

for b_{2} being non empty set holds

( b_{2} = QC-Sub-WFF A iff ( b_{2} is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds

b_{2} c= D ) ) );

for A being QC-alphabet

for b

( b

b

theorem Th8: :: SUBSTUT1:8

for A being QC-alphabet

for S being Element of QC-Sub-WFF A ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e]

for S being Element of QC-Sub-WFF A ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e]

proof end;

definition

let A be QC-alphabet ;

let P be QC-pred_symbol of A;

let l be FinSequence of QC-variables A;

let e be Element of vSUB A;

assume A1: the_arity_of P = len l ;

coherence

[(P ! l),e] is Element of QC-Sub-WFF A

end;
let P be QC-pred_symbol of A;

let l be FinSequence of QC-variables A;

let e be Element of vSUB A;

assume A1: the_arity_of P = len l ;

coherence

[(P ! l),e] is Element of QC-Sub-WFF A

proof end;

:: deftheorem Def18 defines Sub_P SUBSTUT1:def 18 :

for A being QC-alphabet

for P being QC-pred_symbol of A

for l being FinSequence of QC-variables A

for e being Element of vSUB A st the_arity_of P = len l holds

Sub_P (P,l,e) = [(P ! l),e];

for A being QC-alphabet

for P being QC-pred_symbol of A

for l being FinSequence of QC-variables A

for e being Element of vSUB A st the_arity_of P = len l holds

Sub_P (P,l,e) = [(P ! l),e];

theorem Th9: :: SUBSTUT1:9

for A being QC-alphabet

for e being Element of vSUB A

for k being Nat

for P being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]

for e being Element of vSUB A

for k being Nat

for P being QC-pred_symbol of k,A

for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]

proof end;

:: deftheorem defines -Sub_VERUM SUBSTUT1:def 19 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is A -Sub_VERUM iff ex e being Element of vSUB A st S = [(VERUM A),e] );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is A -Sub_VERUM iff ex e being Element of vSUB A st S = [(VERUM A),e] );

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

:: original: `1

redefine func S `1 -> Element of QC-WFF A;

coherence

S `1 is Element of QC-WFF A

redefine func S `2 -> Element of vSUB A;

coherence

S `2 is Element of vSUB A

end;
let S be Element of QC-Sub-WFF A;

:: original: `1

redefine func S `1 -> Element of QC-WFF A;

coherence

S `1 is Element of QC-WFF A

proof end;

:: original: `2redefine func S `2 -> Element of vSUB A;

coherence

S `2 is Element of vSUB A

proof end;

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

coherence

[('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A

end;
let S be Element of QC-Sub-WFF A;

coherence

[('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A

proof end;

:: deftheorem defines Sub_not SUBSTUT1:def 20 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds Sub_not S = [('not' (S `1)),(S `2)];

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds Sub_not S = [('not' (S `1)),(S `2)];

definition

let A be QC-alphabet ;

let S, S9 be Element of QC-Sub-WFF A;

assume A1: S `2 = S9 `2 ;

[((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF A

end;
let S, S9 be Element of QC-Sub-WFF A;

assume A1: S `2 = S9 `2 ;

func Sub_& (S,S9) -> Element of QC-Sub-WFF A equals :Def21: :: SUBSTUT1:def 21

[((S `1) '&' (S9 `1)),(S `2)];

coherence [((S `1) '&' (S9 `1)),(S `2)];

[((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF A

proof end;

:: deftheorem Def21 defines Sub_& SUBSTUT1:def 21 :

for A being QC-alphabet

for S, S9 being Element of QC-Sub-WFF A st S `2 = S9 `2 holds

Sub_& (S,S9) = [((S `1) '&' (S9 `1)),(S `2)];

for A being QC-alphabet

for S, S9 being Element of QC-Sub-WFF A st S `2 = S9 `2 holds

Sub_& (S,S9) = [((S `1) '&' (S9 `1)),(S `2)];

definition

let A be QC-alphabet ;

let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

:: original: `1

redefine func B `1 -> Element of QC-Sub-WFF A;

coherence

B `1 is Element of QC-Sub-WFF A by MCART_1:10;

:: original: `2

redefine func B `2 -> Element of bound_QC-variables A;

coherence

B `2 is Element of bound_QC-variables A by MCART_1:10;

end;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

:: original: `1

redefine func B `1 -> Element of QC-Sub-WFF A;

coherence

B `1 is Element of QC-Sub-WFF A by MCART_1:10;

:: original: `2

redefine func B `2 -> Element of bound_QC-variables A;

coherence

B `2 is Element of bound_QC-variables A by MCART_1:10;

definition
end;

:: deftheorem defines quantifiable SUBSTUT1:def 22 :

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] holds

( B is quantifiable iff ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e] );

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] holds

( B is quantifiable iff ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e] );

definition

let A be QC-alphabet ;

let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

assume A1: B is quantifiable ;

ex b_{1} being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b_{1}]
by A1;

end;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

assume A1: B is quantifiable ;

mode second_Q_comp of B -> Element of vSUB A means :Def23: :: SUBSTUT1:def 23

(B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),it];

existence (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),it];

ex b

:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def 23 :

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] st B is quantifiable holds

for b_{3} being Element of vSUB A holds

( b_{3} is second_Q_comp of B iff (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b_{3}] );

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] st B is quantifiable holds

for b

( b

definition

let A be QC-alphabet ;

let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

let SQ be second_Q_comp of B;

assume A1: B is quantifiable ;

[(All ((B `2),((B `1) `1))),SQ] is Element of QC-Sub-WFF A

end;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

let SQ be second_Q_comp of B;

assume A1: B is quantifiable ;

func Sub_All (B,SQ) -> Element of QC-Sub-WFF A equals :Def24: :: SUBSTUT1:def 24

[(All ((B `2),((B `1) `1))),SQ];

coherence [(All ((B `2),((B `1) `1))),SQ];

[(All ((B `2),((B `1) `1))),SQ] is Element of QC-Sub-WFF A

proof end;

:: deftheorem Def24 defines Sub_All SUBSTUT1:def 24 :

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

for SQ being second_Q_comp of B st B is quantifiable holds

Sub_All (B,SQ) = [(All ((B `2),((B `1) `1))),SQ];

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

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 A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

let x be bound_QC-variable of A;

:: original: [

redefine func [S,x] -> Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

coherence

[S,x] is Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

end;
let S be Element of QC-Sub-WFF A;

let x be bound_QC-variable of A;

:: original: [

redefine func [S,x] -> Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

coherence

[S,x] is Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

proof end;

scheme :: SUBSTUT1:sch 1

SubQCInd{ F_{1}() -> QC-alphabet , P_{1}[ Element of QC-Sub-WFF F_{1}()] } :

provided

SubQCInd{ F

provided

A1:
for k being Nat

for P being QC-pred_symbol of k,F_{1}()

for ll being QC-variable_list of k,F_{1}()

for e being Element of vSUB F_{1}() holds P_{1}[ Sub_P (P,ll,e)]
and

A2: for S being Element of QC-Sub-WFF F_{1}() st S is F_{1}() -Sub_VERUM holds

P_{1}[S]
and

A3: for S being Element of QC-Sub-WFF F_{1}() st P_{1}[S] holds

P_{1}[ Sub_not S]
and

A4: for S, S9 being Element of QC-Sub-WFF F_{1}() st S `2 = S9 `2 & P_{1}[S] & P_{1}[S9] holds

P_{1}[ Sub_& (S,S9)]
and

A5: for x being bound_QC-variable of F_{1}()

for S being Element of QC-Sub-WFF F_{1}()

for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P_{1}[S] holds

P_{1}[ Sub_All ([S,x],SQ)]

for P being QC-pred_symbol of k,F

for ll being QC-variable_list of k,F

for e being Element of vSUB F

A2: for S being Element of QC-Sub-WFF F

P

A3: for S being Element of QC-Sub-WFF F

P

A4: for S, S9 being Element of QC-Sub-WFF F

P

A5: for x being bound_QC-variable of F

for S being Element of QC-Sub-WFF F

for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P

P

proof end;

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

end;
let S be Element of QC-Sub-WFF A;

attr S is Sub_atomic means :: SUBSTUT1:def 25

ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e);

ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e);

:: deftheorem defines Sub_atomic SUBSTUT1:def 25 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_atomic iff ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_atomic iff ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e) );

registration

let A be QC-alphabet ;

let k be Nat;

let P be QC-pred_symbol of k,A;

let ll be QC-variable_list of k,A;

let e be Element of vSUB A;

coherence

Sub_P (P,ll,e) is Sub_atomic ;

end;
let k be Nat;

let P be QC-pred_symbol of k,A;

let ll be QC-variable_list of k,A;

let e be Element of vSUB A;

coherence

Sub_P (P,ll,e) is Sub_atomic ;

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

end;
let S be Element of QC-Sub-WFF A;

attr S is Sub_negative means :Def26: :: SUBSTUT1:def 26

ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9;

ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9;

attr S is Sub_conjunctive means :Def27: :: SUBSTUT1:def 27

ex S1, S2 being Element of QC-Sub-WFF A st

( S = Sub_& (S1,S2) & S1 `2 = S2 `2 );

ex S1, S2 being Element of QC-Sub-WFF A st

( S = Sub_& (S1,S2) & S1 `2 = S2 `2 );

:: deftheorem Def26 defines Sub_negative SUBSTUT1:def 26 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_negative iff ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9 );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_negative iff ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9 );

:: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def 27 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_conjunctive iff ex S1, S2 being Element of QC-Sub-WFF A st

( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_conjunctive iff ex S1, S2 being Element of QC-Sub-WFF A st

( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) );

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

end;
let S be Element of QC-Sub-WFF A;

attr S is Sub_universal means :Def28: :: SUBSTUT1:def 28

ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B is quantifiable );

ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B is quantifiable );

:: deftheorem Def28 defines Sub_universal SUBSTUT1:def 28 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_universal iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B is quantifiable ) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is Sub_universal iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B is quantifiable ) );

theorem Th12: :: SUBSTUT1:12

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( S is A -Sub_VERUM or S is Sub_atomic or S is Sub_negative or S is Sub_conjunctive or S is Sub_universal )

for S being Element of QC-Sub-WFF A holds

( S is A -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 A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_atomic ;

ex b_{1} being FinSequence of QC-variables A ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st

( b_{1} = ll & S = Sub_P (P,ll,e) )
by A1;

uniqueness

for b_{1}, b_{2} being FinSequence of QC-variables A st ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st

( b_{1} = ll & S = Sub_P (P,ll,e) ) & ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st

( b_{2} = ll & S = Sub_P (P,ll,e) ) holds

b_{1} = b_{2}

end;
let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_atomic ;

func Sub_the_arguments_of S -> FinSequence of QC-variables A means :Def29: :: SUBSTUT1:def 29

ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st

( it = ll & S = Sub_P (P,ll,e) );

existence ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st

( it = ll & S = Sub_P (P,ll,e) );

ex b

( b

uniqueness

for b

( b

( b

b

proof end;

:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def 29 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_atomic holds

for b_{3} being FinSequence of QC-variables A holds

( b_{3} = Sub_the_arguments_of S iff ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st

( b_{3} = ll & S = Sub_P (P,ll,e) ) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_atomic holds

for b

( b

( b

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_negative ;

ex b_{1} being Element of QC-Sub-WFF A st S = Sub_not b_{1}
by A1;

uniqueness

for b_{1}, b_{2} being Element of QC-Sub-WFF A st S = Sub_not b_{1} & S = Sub_not b_{2} holds

b_{1} = b_{2}

end;
let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_negative ;

func Sub_the_argument_of S -> Element of QC-Sub-WFF A means :Def30: :: SUBSTUT1:def 30

S = Sub_not it;

existence S = Sub_not it;

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def 30 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_negative holds

for b_{3} being Element of QC-Sub-WFF A holds

( b_{3} = Sub_the_argument_of S iff S = Sub_not b_{3} );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_negative holds

for b

( b

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_conjunctive ;

ex b_{1}, S9 being Element of QC-Sub-WFF A st

( S = Sub_& (b_{1},S9) & b_{1} `2 = S9 `2 )
by A1;

uniqueness

for b_{1}, b_{2} being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (b_{1},S9) & b_{1} `2 = S9 `2 ) & ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (b_{2},S9) & b_{2} `2 = S9 `2 ) holds

b_{1} = b_{2}

end;
let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_conjunctive ;

func Sub_the_left_argument_of S -> Element of QC-Sub-WFF A means :Def31: :: SUBSTUT1:def 31

ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (it,S9) & it `2 = S9 `2 );

existence ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (it,S9) & it `2 = S9 `2 );

ex b

( S = Sub_& (b

uniqueness

for b

( S = Sub_& (b

( S = Sub_& (b

b

proof end;

:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def 31 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds

for b_{3} being Element of QC-Sub-WFF A holds

( b_{3} = Sub_the_left_argument_of S iff ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (b_{3},S9) & b_{3} `2 = S9 `2 ) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds

for b

( b

( S = Sub_& (b

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_conjunctive ;

ex b_{1}, S9 being Element of QC-Sub-WFF A st

( S = Sub_& (S9,b_{1}) & S9 `2 = b_{1} `2 )
by A1;

uniqueness

for b_{1}, b_{2} being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (S9,b_{1}) & S9 `2 = b_{1} `2 ) & ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (S9,b_{2}) & S9 `2 = b_{2} `2 ) holds

b_{1} = b_{2}

end;
let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_conjunctive ;

func Sub_the_right_argument_of S -> Element of QC-Sub-WFF A means :Def32: :: SUBSTUT1:def 32

ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (S9,it) & S9 `2 = it `2 );

existence ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (S9,it) & S9 `2 = it `2 );

ex b

( S = Sub_& (S9,b

uniqueness

for b

( S = Sub_& (S9,b

( S = Sub_& (S9,b

b

proof end;

:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def 32 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds

for b_{3} being Element of QC-Sub-WFF A holds

( b_{3} = Sub_the_right_argument_of S iff ex S9 being Element of QC-Sub-WFF A st

( S = Sub_& (S9,b_{3}) & S9 `2 = b_{3} `2 ) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds

for b

( b

( S = Sub_& (S9,b

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_universal ;

ex b_{1} being bound_QC-variable of A ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B `2 = b_{1} & B is quantifiable )

for b_{1}, b_{2} being bound_QC-variable of A st ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B `2 = b_{1} & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B `2 = b_{2} & B is quantifiable ) holds

b_{1} = b_{2}

end;
let S be Element of QC-Sub-WFF A;

assume A1: S is Sub_universal ;

func Sub_the_bound_of S -> bound_QC-variable of A means :: SUBSTUT1:def 33

ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B `2 = it & B is quantifiable );

existence ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B `2 = it & B is quantifiable );

ex b

( S = Sub_All (B,SQ) & B `2 = b

proof end;

uniqueness for b

( S = Sub_All (B,SQ) & B `2 = b

( S = Sub_All (B,SQ) & B `2 = b

b

proof end;

:: deftheorem defines Sub_the_bound_of SUBSTUT1:def 33 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_universal holds

for b_{3} being bound_QC-variable of A holds

( b_{3} = Sub_the_bound_of S iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( S = Sub_All (B,SQ) & B `2 = b_{3} & B is quantifiable ) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_universal holds

for b

( b

( S = Sub_All (B,SQ) & B `2 = b

definition

let A be QC-alphabet ;

let A2 be Element of QC-Sub-WFF A;

assume A1: A2 is Sub_universal ;

ex b_{1} being Element of QC-Sub-WFF A ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( A2 = Sub_All (B,SQ) & B `1 = b_{1} & B is quantifiable )

for b_{1}, b_{2} being Element of QC-Sub-WFF A st ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( A2 = Sub_All (B,SQ) & B `1 = b_{1} & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( A2 = Sub_All (B,SQ) & B `1 = b_{2} & B is quantifiable ) holds

b_{1} = b_{2}

end;
let A2 be Element of QC-Sub-WFF A;

assume A1: A2 is Sub_universal ;

func Sub_the_scope_of A2 -> Element of QC-Sub-WFF A means :Def34: :: SUBSTUT1:def 34

ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( A2 = Sub_All (B,SQ) & B `1 = it & B is quantifiable );

existence ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( A2 = Sub_All (B,SQ) & B `1 = it & B is quantifiable );

ex b

( A2 = Sub_All (B,SQ) & B `1 = b

proof end;

uniqueness for b

( A2 = Sub_All (B,SQ) & B `1 = b

( A2 = Sub_All (B,SQ) & B `1 = b

b

proof end;

:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def 34 :

for A being QC-alphabet

for A2 being Element of QC-Sub-WFF A st A2 is Sub_universal holds

for b_{3} being Element of QC-Sub-WFF A holds

( b_{3} = Sub_the_scope_of A2 iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st

( A2 = Sub_All (B,SQ) & B `1 = b_{3} & B is quantifiable ) );

for A being QC-alphabet

for A2 being Element of QC-Sub-WFF A st A2 is Sub_universal holds

for b

( b

( A2 = Sub_All (B,SQ) & B `1 = b

registration
end;

theorem Th13: :: SUBSTUT1:13

for A being QC-alphabet

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

Sub_& (S1,S2) is Sub_conjunctive ;

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

Sub_& (S1,S2) is Sub_conjunctive ;

theorem Th14: :: SUBSTUT1:14

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

for SQ being second_Q_comp of B st B is quantifiable holds

Sub_All (B,SQ) is Sub_universal ;

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

for SQ being second_Q_comp of B st B is quantifiable holds

Sub_All (B,SQ) is Sub_universal ;

theorem :: SUBSTUT1:15

for A being QC-alphabet

for S, S9 being Element of QC-Sub-WFF A st Sub_not S = Sub_not S9 holds

S = S9

for S, S9 being Element of QC-Sub-WFF A st Sub_not S = Sub_not S9 holds

S = S9

proof end;

theorem :: SUBSTUT1:16

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds Sub_the_argument_of (Sub_not S) = S by Def30;

for S being Element of QC-Sub-WFF A holds Sub_the_argument_of (Sub_not S) = S by Def30;

theorem :: SUBSTUT1:17

for A being QC-alphabet

for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds

( S1 = S19 & S2 = S29 )

for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds

( S1 = S19 & S2 = S29 )

proof end;

theorem Th18: :: SUBSTUT1:18

for A being QC-alphabet

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

Sub_the_left_argument_of (Sub_& (S1,S2)) = S1

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

Sub_the_left_argument_of (Sub_& (S1,S2)) = S1

proof end;

theorem Th19: :: SUBSTUT1:19

for A being QC-alphabet

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

Sub_the_right_argument_of (Sub_& (S1,S2)) = S2

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

Sub_the_right_argument_of (Sub_& (S1,S2)) = S2

proof end;

theorem :: SUBSTUT1:20

for A being QC-alphabet

for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

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

for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

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

for A being QC-alphabet

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

for SQ being second_Q_comp of B st B is quantifiable holds

Sub_the_scope_of (Sub_All (B,SQ)) = B `1

for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]

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{ F_{1}() -> QC-alphabet , P_{1}[ Element of QC-Sub-WFF F_{1}()] } :

provided

SubQCInd2{ F

provided

A1:
for S being Element of QC-Sub-WFF F_{1}() holds

( ( S is Sub_atomic implies P_{1}[S] ) & ( S is F_{1}() -Sub_VERUM implies P_{1}[S] ) & ( S is Sub_negative & P_{1}[ Sub_the_argument_of S] implies P_{1}[S] ) & ( S is Sub_conjunctive & P_{1}[ Sub_the_left_argument_of S] & P_{1}[ Sub_the_right_argument_of S] implies P_{1}[S] ) & ( S is Sub_universal & P_{1}[ Sub_the_scope_of S] implies P_{1}[S] ) )

( ( S is Sub_atomic implies P

proof end;

theorem Th22: :: SUBSTUT1:22

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_negative holds

len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))

for S being Element of QC-Sub-WFF A st S is Sub_negative holds

len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))

proof end;

theorem Th23: :: SUBSTUT1:23

for A being QC-alphabet

for S being Element of QC-Sub-WFF A 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)) )

for S being Element of QC-Sub-WFF A 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

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_universal holds

len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))

for S being Element of QC-Sub-WFF A st S is Sub_universal holds

len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))

proof end;

theorem Th25: :: SUBSTUT1:25

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds

( ( S is A -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,A ) & ( 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 ) )

for S being Element of QC-Sub-WFF A holds

( ( S is A -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,A ) & ( 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

for A being QC-alphabet

for S being Element of QC-Sub-WFF A 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 )

for S being Element of QC-Sub-WFF A 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

for A being QC-alphabet

for S being Element of QC-Sub-WFF A 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 A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )

for S being Element of QC-Sub-WFF A 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 A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )

proof end;

scheme :: SUBSTUT1:sch 3

SubFuncEx{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}( Element of QC-Sub-WFF F_{1}()) -> Element of F_{2}(), F_{5}( Element of F_{2}()) -> Element of F_{2}(), F_{6}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{7}( set , Element of QC-Sub-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}() } :

SubFuncEx{ F

ex F being Function of (QC-Sub-WFF F_{1}()),F_{2}() st

for S being Element of QC-Sub-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( S is F_{1}() -Sub_VERUM implies F . S = F_{3}() ) & ( S is Sub_atomic implies F . S = F_{4}(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F_{5}(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F_{6}(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F_{7}(F_{1}(),S,d1) ) )

for S being Element of QC-Sub-WFF F

for d1, d2 being Element of F

( ( S is F

proof end;

scheme :: SUBSTUT1:sch 4

SubQCFuncUniq{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Function of (QC-Sub-WFF F_{1}()),F_{2}(), F_{4}() -> Function of (QC-Sub-WFF F_{1}()),F_{2}(), F_{5}() -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}(), F_{7}( set ) -> Element of F_{2}(), F_{8}( set , set ) -> Element of F_{2}(), F_{9}( set , set , set ) -> Element of F_{2}() } :

provided

SubQCFuncUniq{ F

provided

A1:
for S being Element of QC-Sub-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( S is F_{1}() -Sub_VERUM implies F_{3}() . S = F_{5}() ) & ( S is Sub_atomic implies F_{3}() . S = F_{6}(S) ) & ( S is Sub_negative & d1 = F_{3}() . (Sub_the_argument_of S) implies F_{3}() . S = F_{7}(d1) ) & ( S is Sub_conjunctive & d1 = F_{3}() . (Sub_the_left_argument_of S) & d2 = F_{3}() . (Sub_the_right_argument_of S) implies F_{3}() . S = F_{8}(d1,d2) ) & ( S is Sub_universal & d1 = F_{3}() . (Sub_the_scope_of S) implies F_{3}() . S = F_{9}(F_{1}(),S,d1) ) )
and

A2: for S being Element of QC-Sub-WFF F_{1}()

for d1, d2 being Element of F_{2}() holds

( ( S is F_{1}() -Sub_VERUM implies F_{4}() . S = F_{5}() ) & ( S is Sub_atomic implies F_{4}() . S = F_{6}(S) ) & ( S is Sub_negative & d1 = F_{4}() . (Sub_the_argument_of S) implies F_{4}() . S = F_{7}(d1) ) & ( S is Sub_conjunctive & d1 = F_{4}() . (Sub_the_left_argument_of S) & d2 = F_{4}() . (Sub_the_right_argument_of S) implies F_{4}() . S = F_{8}(d1,d2) ) & ( S is Sub_universal & d1 = F_{4}() . (Sub_the_scope_of S) implies F_{4}() . S = F_{9}(F_{1}(),S,d1) ) )

for d1, d2 being Element of F

( ( S is F

A2: for S being Element of QC-Sub-WFF F

for d1, d2 being Element of F

( ( S is F

proof end;

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

coherence

S is Element of [:(QC-WFF A),(vSUB A):]

end;
let S be Element of QC-Sub-WFF A;

coherence

S is Element of [:(QC-WFF A),(vSUB A):]

proof end;

:: deftheorem defines @ SUBSTUT1:def 35 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds @ S = S;

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds @ S = S;

definition

let A be QC-alphabet ;

let Z be Element of [:(QC-WFF A),(vSUB A):];

:: original: `1

redefine func Z `1 -> Element of QC-WFF A;

coherence

Z `1 is Element of QC-WFF A

redefine func Z `2 -> CQC_Substitution of A;

coherence

Z `2 is CQC_Substitution of A

end;
let Z be Element of [:(QC-WFF A),(vSUB A):];

:: original: `1

redefine func Z `1 -> Element of QC-WFF A;

coherence

Z `1 is Element of QC-WFF A

proof end;

:: original: `2redefine func Z `2 -> CQC_Substitution of A;

coherence

Z `2 is CQC_Substitution of A

proof end;

definition

let A be QC-alphabet ;

let Z be Element of [:(QC-WFF A),(vSUB A):];

( ( 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 of A ) & ( 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 of A ) ) ;

consistency

for b_{1} being bound_QC-variable of A holds verum
;

end;
let Z be Element of [:(QC-WFF A),(vSUB A):];

func S_Bound Z -> bound_QC-variable of A 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 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);

( ( 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 of A ) & ( 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 of A ) ) ;

consistency

for b

:: deftheorem defines S_Bound SUBSTUT1:def 36 :

for A being QC-alphabet

for Z being Element of [:(QC-WFF A),(vSUB A):] 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) ) );

for A being QC-alphabet

for Z being Element of [:(QC-WFF A),(vSUB A):] 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 A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

let p be QC-formula of A;

coherence

All ((S_Bound (@ S)),p) is Element of QC-WFF A ;

end;
let S be Element of QC-Sub-WFF A;

let p be QC-formula of A;

coherence

All ((S_Bound (@ S)),p) is Element of QC-WFF A ;

:: deftheorem defines Quant SUBSTUT1:def 37 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A

for p being QC-formula of A holds Quant (S,p) = All ((S_Bound (@ S)),p);

for A being QC-alphabet

for S being Element of QC-Sub-WFF A

for p being QC-formula of A holds Quant (S,p) = All ((S_Bound (@ S)),p);

Lm6: for A being QC-alphabet

for F1, F2 being Function of (QC-Sub-WFF A),(QC-WFF A) st ( for S being Element of QC-Sub-WFF A holds

( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( 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 A holds

( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( 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;

:: (Ebb et al, Chapter III, Definition 8.1/8.2)

definition

let A be QC-alphabet ;

let S be Element of QC-Sub-WFF A;

ex b_{1} being Element of QC-WFF A ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st

( b_{1} = F . S & ( for S9 being Element of QC-Sub-WFF A holds

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) )

for b_{1}, b_{2} being Element of QC-WFF A st ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st

( b_{1} = F . S & ( for S9 being Element of QC-Sub-WFF A holds

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) & ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st

( b_{2} = F . S & ( for S9 being Element of QC-Sub-WFF A holds

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) holds

b_{1} = b_{2}
by Lm6;

end;
let S be Element of QC-Sub-WFF A;

func CQC_Sub S -> Element of QC-WFF A means :Def38: :: SUBSTUT1:def 38

ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st

( it = F . S & ( for S9 being Element of QC-Sub-WFF A holds

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) );

existence ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st

( it = F . S & ( for S9 being Element of QC-Sub-WFF A holds

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) );

ex b

( b

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) )

proof end;

uniqueness for b

( b

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) & ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st

( b

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) holds

b

:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def 38 :

for A being QC-alphabet

for S being Element of QC-Sub-WFF A

for b_{3} being Element of QC-WFF A holds

( b_{3} = CQC_Sub S iff ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st

( b_{3} = F . S & ( for S9 being Element of QC-Sub-WFF A holds

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) );

for A being QC-alphabet

for S being Element of QC-Sub-WFF A

for b

( b

( b

( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) );

theorem Th28: :: SUBSTUT1:28

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_negative holds

CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S))

for S being Element of QC-Sub-WFF A st S is Sub_negative holds

CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S))

proof end;

theorem Th29: :: SUBSTUT1:29

for A being QC-alphabet

for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)

for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)

proof end;

theorem Th30: :: SUBSTUT1:30

for A being QC-alphabet

for S being Element of QC-Sub-WFF A 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))

for S being Element of QC-Sub-WFF A 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

for A being QC-alphabet

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds

CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)

proof end;

theorem Th32: :: SUBSTUT1:32

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is Sub_universal holds

CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S)))

for S being Element of QC-Sub-WFF A st S is Sub_universal holds

CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S)))

proof end;

definition

let A be QC-alphabet ;

{ S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } is Subset of (QC-Sub-WFF A)

end;
func CQC-Sub-WFF A -> Subset of (QC-Sub-WFF A) equals :: SUBSTUT1:def 39

{ S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ;

coherence { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ;

{ S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } is Subset of (QC-Sub-WFF A)

proof end;

:: deftheorem defines CQC-Sub-WFF SUBSTUT1:def 39 :

for A being QC-alphabet holds CQC-Sub-WFF A = { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ;

for A being QC-alphabet holds CQC-Sub-WFF A = { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ;

theorem Th33: :: SUBSTUT1:33

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds

CQC_Sub S is Element of CQC-WFF A

for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds

CQC_Sub S is Element of CQC-WFF A

proof end;

Lm7: for A being QC-alphabet

for k being Nat

for P being QC-pred_symbol of k,A

for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P

proof end;

theorem Th34: :: SUBSTUT1:34

for A being QC-alphabet

for k being Nat

for h being FinSequence holds

( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )

for k being Nat

for h being FinSequence holds

( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )

proof end;

theorem Th35: :: SUBSTUT1:35

for A being QC-alphabet

for k being Nat

for P being QC-pred_symbol of k,A

for ll being CQC-variable_list of k,A

for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A

for k being Nat

for P being QC-pred_symbol of k,A

for ll being CQC-variable_list of k,A

for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A

proof end;

theorem Th36: :: SUBSTUT1:36

for A being QC-alphabet

for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds

CQC_Sub (Sub_not S) is Element of CQC-WFF A

for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds

CQC_Sub (Sub_not S) is Element of CQC-WFF A

proof end;

theorem Th37: :: SUBSTUT1:37

for A being QC-alphabet

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A holds

CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A

for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A holds

CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A

proof end;

theorem Th38: :: SUBSTUT1:38

for A being QC-alphabet

for x being bound_QC-variable of A

for S being Element of QC-Sub-WFF A

for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds

CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A

for x being bound_QC-variable of A

for S being Element of QC-Sub-WFF A

for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds

CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A

proof end;

scheme :: SUBSTUT1:sch 5

SubCQCInd{ F_{1}() -> QC-alphabet , P_{1}[ set ] } :

provided

SubCQCInd{ F

provided

A1:
for S, S9 being Element of CQC-Sub-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for SQ being second_Q_comp of [S,x]

for k being Nat

for ll being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}()

for e being Element of vSUB F_{1}() holds

( P_{1}[ Sub_P (P,ll,e)] & ( S is F_{1}() -Sub_VERUM implies P_{1}[S] ) & ( P_{1}[S] implies P_{1}[ Sub_not S] ) & ( S `2 = S9 `2 & P_{1}[S] & P_{1}[S9] implies P_{1}[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & P_{1}[S] implies P_{1}[ Sub_All ([S,x],SQ)] ) )

for x being bound_QC-variable of F

for SQ being second_Q_comp of [S,x]

for k being Nat

for ll being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

for e being Element of vSUB F

( P

proof end;

definition

let A be QC-alphabet ;

let S be Element of CQC-Sub-WFF A;

:: original: CQC_Sub

redefine func CQC_Sub S -> Element of CQC-WFF A;

coherence

CQC_Sub S is Element of CQC-WFF A

end;
let S be Element of CQC-Sub-WFF A;

:: original: CQC_Sub

redefine func CQC_Sub S -> Element of CQC-WFF A;

coherence

CQC_Sub S is Element of CQC-WFF A

proof end;

theorem :: SUBSTUT1:39

for A being QC-alphabet

for Sub being CQC_Substitution of A holds rng (@ Sub) c= bound_QC-variables A ;

for Sub being CQC_Substitution of A holds rng (@ Sub) c= bound_QC-variables A ;