:: Substitution in First-Order Formulas -- Part II. {T}he Construction of First-Order Formulas
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users


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 )
proof end;

Lm1: for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for k, l being 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 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 Nat
for P being QC-pred_symbol of k,Al
for k, l being 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 )
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 )
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;

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}
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))
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
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]))
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] )
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 )
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 )
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
proof end;
end;

notation
let Al be QC-alphabet ;
let x, y be bound_QC-variable of Al;
synonym Sbst (x,y) for Al .--> x;
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
proof end;
end;

definition
let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
let x, y be bound_QC-variable of Al;
func p . (x,y) -> Element of CQC-WFF Al equals :: SUBSTUT2:def 1
 CQC_Sub [p,(Sbst (x,y))];
coherence
CQC_Sub [p,(Sbst (x,y))] is Element of CQC-WFF Al ;
end;

:: 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))];

scheme :: SUBSTUT2:sch 1
CQCInd1{ F1() -> QC-alphabet , P1[ set ] } :
for p being Element of CQC-WFF F1() holds P1[p]
provided
A1: for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds
P1[p] and
A2: for k being Nat st ( for p being Element of CQC-WFF F1() st QuantNbr p = k holds
P1[p] ) holds
for p being Element of CQC-WFF F1() st QuantNbr p = k + 1 holds
P1[p]
proof end;

scheme :: SUBSTUT2:sch 2
CQCInd2{ F1() -> QC-alphabet , P1[ set ] } :
for p being Element of CQC-WFF F1() holds P1[p]
provided
A1: for p being Element of CQC-WFF F1() st QuantNbr p <= 0 holds
P1[p] and
A2: for k being Nat st ( for p being Element of CQC-WFF F1() st QuantNbr p <= k holds
P1[p] ) holds
for p being Element of CQC-WFF F1() st QuantNbr p <= k + 1 holds
P1[p]
proof end;

theorem :: SUBSTUT2:13
for Al being QC-alphabet
for x, y being bound_QC-variable of Al holds (VERUM Al) . (x,y) = VERUM Al
proof end;

theorem :: SUBSTUT2:14
for Al being QC-alphabet
for k being 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 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
proof end;
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]
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))) ) )
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])
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])
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)) ) )
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])
proof end;

definition
let Al be QC-alphabet ;
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) is Function of (CQC-Sub-WFF Al),(vSUB Al)
proof end;
end;

:: deftheorem defines CFQ SUBSTUT2:def 2 :
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;
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] is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] ;
end;

:: 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];

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;
func Qsc (p,x,Sub) -> second_Q_comp of QScope (p,x,Sub) equals :: SUBSTUT2:def 4
Sub;
coherence
Sub is second_Q_comp of QScope (p,x,Sub)
proof end;
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;

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 )
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])
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])
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])
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 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{ F1() -> QC-alphabet , P1[ set ] } :
for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds
P1[p]
provided
A1: for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( P1[ VERUM F1()] & P1[P ! l] & ( P1[r] implies P1[ 'not' r] ) & ( P1[r] & P1[s] implies P1[r '&' s] ) )
proof end;

definition
let Al be QC-alphabet ;
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 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
ex b1 being FinSequence st
( 1 <= len b1 & b1 . 1 = G & b1 . (len b1) = H & ( for k being Nat st 1 <= k & k < len b1 holds
ex G1, H1 being Element of QC-WFF Al st
( b1 . k = G1 & b1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
proof end;
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 b4 being FinSequence holds
( b4 is PATH of G,H iff ( 1 <= len b4 & b4 . 1 = G & b4 . (len b4) = H & ( for k being Nat st 1 <= k & k < len b4 holds
ex G1, H1 being Element of QC-WFF Al st
( b4 . k = G1 & b4 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );

theorem :: SUBSTUT2:27
for Al being QC-alphabet
for i being 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 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 i, n being Nat
for p, q 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 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 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
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
proof end;

theorem :: SUBSTUT2:34
for Al being QC-alphabet
for p being Element of CQC-WFF Al st 1 <= QuantNbr p holds
ex q being Element of CQC-WFF Al st
( q is_subformula_of p & QuantNbr q = 1 ) by Th33;