:: by Patrick Braselmann and Peter Koepke

::

:: Received September 25, 2004

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

begin

theorem Th1: :: SUBSTUT2:1

for Al being QC-alphabet

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = VERUM Al & S `2 = Sub )

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = VERUM Al & S `2 = Sub )

proof end;

Lm1: for Al being QC-alphabet

for k being Element of NAT

for P being QC-pred_symbol of k,Al

for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds

k = l

proof end;

theorem Th2: :: SUBSTUT2:2

for Al being QC-alphabet

for k being Element of NAT

for P being QC-pred_symbol of k,Al

for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

for k being Element of NAT

for P being QC-pred_symbol of k,Al

for ll being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = P ! ll & S `2 = Sub )

proof end;

theorem :: SUBSTUT2:3

for Al being QC-alphabet

for k being Element of NAT

for P being QC-pred_symbol of k,Al

for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds

k = l by Lm1;

for k being Element of NAT

for P being QC-pred_symbol of k,Al

for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds

k = l by Lm1;

theorem Th4: :: SUBSTUT2:4

for Al being QC-alphabet

for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = 'not' p & S `2 = Sub )

for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = 'not' p & S `2 = Sub )

proof end;

theorem Th5: :: SUBSTUT2:5

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

proof end;

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

let Sub be CQC_Substitution of Al;

:: original: [

redefine func [p,Sub] -> Element of [:(QC-WFF Al),(vSUB Al):];

coherence

[p,Sub] is Element of [:(QC-WFF Al),(vSUB Al):] by ZFMISC_1:def 2;

end;
let p be Element of CQC-WFF Al;

let Sub be CQC_Substitution of Al;

:: original: [

redefine func [p,Sub] -> Element of [:(QC-WFF Al),(vSUB Al):];

coherence

[p,Sub] is Element of [:(QC-WFF Al),(vSUB Al):] by ZFMISC_1:def 2;

theorem Th6: :: SUBSTUT2:6

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds dom (RestrictSub (x,(All (x,p)),Sub)) misses {x}

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds dom (RestrictSub (x,(All (x,p)),Sub)) misses {x}

proof end;

theorem Th7: :: SUBSTUT2:7

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))

proof end;

theorem Th8: :: SUBSTUT2:8

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

proof end;

theorem Th9: :: SUBSTUT2:9

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))

proof end;

theorem Th10: :: SUBSTUT2:10

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al

for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds

( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )

proof end;

theorem Th11: :: SUBSTUT2:11

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = All (x,p) & S `2 = Sub )

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = All (x,p) & S `2 = Sub )

proof end;

theorem Th12: :: SUBSTUT2:12

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub )

for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub )

proof end;

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

let Sub be CQC_Substitution of Al;

:: original: [

redefine func [p,Sub] -> Element of CQC-Sub-WFF Al;

coherence

[p,Sub] is Element of CQC-Sub-WFF Al

end;
let p be Element of CQC-WFF Al;

let Sub be CQC_Substitution of Al;

:: original: [

redefine func [p,Sub] -> Element of CQC-Sub-WFF Al;

coherence

[p,Sub] is Element of CQC-Sub-WFF Al

proof end;

notation
end;

definition

let Al be QC-alphabet ;

let x, y be bound_QC-variable of Al;

:: original: Sbst

redefine func Sbst (x,y) -> CQC_Substitution of Al;

coherence

Sbst (y,) is CQC_Substitution of Al

end;
let x, y be bound_QC-variable of Al;

:: original: Sbst

redefine func Sbst (x,y) -> CQC_Substitution of Al;

coherence

Sbst (y,) is CQC_Substitution of Al

proof end;

begin

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

let x, y be bound_QC-variable of Al;

coherence

CQC_Sub [p,(Sbst (x,y))] is Element of CQC-WFF Al ;

end;
let p be Element of CQC-WFF Al;

let x, y be bound_QC-variable of Al;

coherence

CQC_Sub [p,(Sbst (x,y))] is Element of CQC-WFF Al ;

:: deftheorem defines . SUBSTUT2:def 1 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds p . (x,y) = CQC_Sub [p,(Sbst (x,y))];

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds p . (x,y) = CQC_Sub [p,(Sbst (x,y))];

scheme :: SUBSTUT2:sch 1

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

provided

CQCInd1{ F

provided

A1:
for p being Element of CQC-WFF F_{1}() st QuantNbr p = 0 holds

P_{1}[p]
and

A2: for k being Element of NAT st ( for p being Element of CQC-WFF F_{1}() st QuantNbr p = k holds

P_{1}[p] ) holds

for p being Element of CQC-WFF F_{1}() st QuantNbr p = k + 1 holds

P_{1}[p]

P

A2: for k being Element of NAT st ( for p being Element of CQC-WFF F

P

for p being Element of CQC-WFF F

P

proof end;

scheme :: SUBSTUT2:sch 2

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

provided

CQCInd2{ F

provided

A1:
for p being Element of CQC-WFF F_{1}() st QuantNbr p <= 0 holds

P_{1}[p]
and

A2: for k being Element of NAT st ( for p being Element of CQC-WFF F_{1}() st QuantNbr p <= k holds

P_{1}[p] ) holds

for p being Element of CQC-WFF F_{1}() st QuantNbr p <= k + 1 holds

P_{1}[p]

P

A2: for k being Element of NAT st ( for p being Element of CQC-WFF F

P

for p being Element of CQC-WFF F

P

proof end;

theorem :: SUBSTUT2:14

for Al being QC-alphabet

for k being Element of NAT

for x, y being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

for k being Element of NAT

for x, y being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

proof end;

theorem Th15: :: SUBSTUT2:15

for Al being QC-alphabet

for k being Element of NAT

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])

for k being Element of NAT

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al

for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])

proof end;

definition

let Al be QC-alphabet ;

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

:: original: `2

redefine func S `2 -> CQC_Substitution of Al;

coherence

S `2 is CQC_Substitution of Al

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

:: original: `2

redefine func S `2 -> CQC_Substitution of Al;

coherence

S `2 is CQC_Substitution of Al

proof end;

theorem Th16: :: SUBSTUT2:16

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub]

for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub]

proof end;

theorem :: SUBSTUT2:17

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds

( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) )

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds

( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) )

proof end;

theorem Th18: :: SUBSTUT2:18

for Al being QC-alphabet

for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub])

for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub])

proof end;

theorem Th19: :: SUBSTUT2:19

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al holds [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub])

for p, q being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al holds [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub])

proof end;

theorem :: SUBSTUT2:20

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds

( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) )

for p, q being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds

( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) )

proof end;

theorem Th21: :: SUBSTUT2:21

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])

for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])

proof end;

definition

let Al be QC-alphabet ;

(QSub Al) | (CQC-Sub-WFF Al) is Function of (CQC-Sub-WFF Al),(vSUB Al)

end;
func CFQ Al -> Function of (CQC-Sub-WFF Al),(vSUB Al) equals :: SUBSTUT2:def 2

(QSub Al) | (CQC-Sub-WFF Al);

coherence (QSub Al) | (CQC-Sub-WFF Al);

(QSub Al) | (CQC-Sub-WFF Al) is Function of (CQC-Sub-WFF Al),(vSUB Al)

proof end;

:: deftheorem defines CFQ SUBSTUT2:def 2 :

for Al being QC-alphabet holds CFQ Al = (QSub Al) | (CQC-Sub-WFF Al);

for Al being QC-alphabet holds CFQ Al = (QSub Al) | (CQC-Sub-WFF Al);

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

let Sub be CQC_Substitution of Al;

[[p,((CFQ Al) . [(All (x,p)),Sub])],x] is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] ;

end;
let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

let Sub be CQC_Substitution of Al;

func QScope (p,x,Sub) -> CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] equals :: SUBSTUT2:def 3

[[p,((CFQ Al) . [(All (x,p)),Sub])],x];

coherence [[p,((CFQ Al) . [(All (x,p)),Sub])],x];

[[p,((CFQ Al) . [(All (x,p)),Sub])],x] is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] ;

:: deftheorem defines QScope SUBSTUT2:def 3 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds QScope (p,x,Sub) = [[p,((CFQ Al) . [(All (x,p)),Sub])],x];

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds QScope (p,x,Sub) = [[p,((CFQ Al) . [(All (x,p)),Sub])],x];

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

let Sub be CQC_Substitution of Al;

coherence

Sub is second_Q_comp of QScope (p,x,Sub)

end;
let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

let Sub be CQC_Substitution of Al;

coherence

Sub is second_Q_comp of QScope (p,x,Sub)

proof end;

:: deftheorem defines Qsc SUBSTUT2:def 4 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds Qsc (p,x,Sub) = Sub;

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds Qsc (p,x,Sub) = Sub;

theorem Th22: :: SUBSTUT2:22

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds

( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable )

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al holds

( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable )

proof end;

theorem Th23: :: SUBSTUT2:23

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

proof end;

theorem Th24: :: SUBSTUT2:24

for Al being QC-alphabet

for Sub being CQC_Substitution of Al holds QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub])

for Sub being CQC_Substitution of Al holds QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub])

proof end;

theorem :: SUBSTUT2:25

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub])

for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub])

proof end;

theorem :: SUBSTUT2:26

for Al being QC-alphabet

for p being Element of CQC-WFF Al st p is atomic holds

ex k being Element of NAT ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll

for p being Element of CQC-WFF Al st p is atomic holds

ex k being Element of NAT ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll

proof end;

scheme :: SUBSTUT2:sch 3

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

provided

CQCInd3{ F

provided

A1:
for r, s being Element of CQC-WFF F_{1}()

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

for k being Element of NAT

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

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

( P_{1}[ VERUM F_{1}()] & P_{1}[P ! l] & ( P_{1}[r] implies P_{1}[ 'not' r] ) & ( P_{1}[r] & P_{1}[s] implies P_{1}[r '&' s] ) )

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( P

proof end;

begin

definition

let Al be QC-alphabet ;

let G, H be QC-formula of Al;

assume A1: G is_subformula_of H ;

ex b_{1} being FinSequence st

( 1 <= len b_{1} & b_{1} . 1 = G & b_{1} . (len b_{1}) = H & ( for k being Element of NAT st 1 <= k & k < len b_{1} holds

ex G1, H1 being Element of QC-WFF Al st

( b_{1} . k = G1 & b_{1} . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )

end;
let G, H be QC-formula of Al;

assume A1: G is_subformula_of H ;

mode PATH of G,H -> FinSequence means :Def5: :: SUBSTUT2:def 5

( 1 <= len it & it . 1 = G & it . (len it) = H & ( for k being Element of NAT st 1 <= k & k < len it holds

ex G1, H1 being Element of QC-WFF Al st

( it . k = G1 & it . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) );

existence ( 1 <= len it & it . 1 = G & it . (len it) = H & ( for k being Element of NAT st 1 <= k & k < len it holds

ex G1, H1 being Element of QC-WFF Al st

( it . k = G1 & it . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) );

ex b

( 1 <= len b

ex G1, H1 being Element of QC-WFF Al st

( b

proof end;

:: deftheorem Def5 defines PATH SUBSTUT2:def 5 :

for Al being QC-alphabet

for G, H being QC-formula of Al st G is_subformula_of H holds

for b_{4} being FinSequence holds

( b_{4} is PATH of G,H iff ( 1 <= len b_{4} & b_{4} . 1 = G & b_{4} . (len b_{4}) = H & ( for k being Element of NAT st 1 <= k & k < len b_{4} holds

ex G1, H1 being Element of QC-WFF Al st

( b_{4} . k = G1 & b_{4} . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );

for Al being QC-alphabet

for G, H being QC-formula of Al st G is_subformula_of H holds

for b

( b

ex G1, H1 being Element of QC-WFF Al st

( b

theorem :: SUBSTUT2:27

for Al being QC-alphabet

for i being Element of NAT

for F1, F2 being QC-formula of Al

for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds

ex F3 being QC-formula of Al st

( F3 = L . i & F3 is_subformula_of F2 )

for i being Element of NAT

for F1, F2 being QC-formula of Al

for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds

ex F3 being QC-formula of Al st

( F3 = L . i & F3 is_subformula_of F2 )

proof end;

theorem Th28: :: SUBSTUT2:28

for Al being QC-alphabet

for i being Element of NAT

for p being Element of CQC-WFF Al

for F1 being QC-formula of Al

for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds

L . i is Element of CQC-WFF Al

for i being Element of NAT

for p being Element of CQC-WFF Al

for F1 being QC-formula of Al

for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds

L . i is Element of CQC-WFF Al

proof end;

theorem Th29: :: SUBSTUT2:29

for Al being QC-alphabet

for n, i being Element of NAT

for q, p being Element of CQC-WFF Al

for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds

ex r being Element of CQC-WFF Al st

( r = L . i & QuantNbr r <= n )

for n, i being Element of NAT

for q, p being Element of CQC-WFF Al

for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds

ex r being Element of CQC-WFF Al st

( r = L . i & QuantNbr r <= n )

proof end;

theorem :: SUBSTUT2:30

for Al being QC-alphabet

for n being Element of NAT

for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds

QuantNbr q <= n

for n being Element of NAT

for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds

QuantNbr q <= n

proof end;

theorem :: SUBSTUT2:31

for Al being QC-alphabet

for n being Element of NAT

for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds

QuantNbr q = n ) holds

n = 0

for n being Element of NAT

for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds

QuantNbr q = n ) holds

n = 0

proof end;

theorem :: SUBSTUT2:32

for Al being QC-alphabet

for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds

for x being bound_QC-variable of Al

for r being Element of CQC-WFF Al holds q <> All (x,r) ) holds

QuantNbr p = 0

for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds

for x being bound_QC-variable of Al

for r being Element of CQC-WFF Al holds q <> All (x,r) ) holds

QuantNbr p = 0

proof end;

theorem Th33: :: SUBSTUT2:33

for Al being QC-alphabet

for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds

QuantNbr q <> 1 ) holds

QuantNbr p = 0

for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds

QuantNbr q <> 1 ) holds

QuantNbr p = 0

proof end;

theorem :: SUBSTUT2:34