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

theorem Th1: :: SUBSTUT2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = VERUM & S `2 = Sub )
proof end;

Lm1: for k being Nat
for P being QC-pred_symbol of k
for k, l being Nat st P is QC-pred_symbol of k & P is QC-pred_symbol of l holds
k = l
proof end;

theorem Th2: :: SUBSTUT2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = P ! ll & S `2 = Sub )
proof end;

theorem :: SUBSTUT2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for k, l being Nat st P is QC-pred_symbol of k & P is QC-pred_symbol of l holds
k = l by Lm1;

theorem Th4: :: SUBSTUT2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ) holds
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = 'not' p & S `2 = Sub )
proof end;

theorem Th5: :: SUBSTUT2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF st ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = q & S `2 = Sub ) ) holds
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p '&' q & S `2 = Sub )
proof end;

definition
let p be Element of CQC-WFF ;
let Sub be CQC_Substitution;
:: original: [
redefine func [p,Sub] -> Element of [:QC-WFF ,vSUB :];
coherence
[p,Sub] is Element of [:QC-WFF ,vSUB :]
by ZFMISC_1:def 2;
end;

theorem Th6: :: SUBSTUT2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution holds dom (RestrictSub x,(All x,p),Sub) misses {x}
proof end;

theorem Th7: :: SUBSTUT2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution
for S being Element of CQC-Sub-WFF 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 st S1 = [(All x,p),Sub] )
proof end;

theorem Th11: :: SUBSTUT2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable st ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ) holds
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = All x,p & S `2 = Sub )
proof end;

theorem Th12: :: SUBSTUT2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub )
proof end;

definition
let p be Element of CQC-WFF ;
let Sub be CQC_Substitution;
:: original: [
redefine func [p,Sub] -> Element of CQC-Sub-WFF ;
coherence
[p,Sub] is Element of CQC-Sub-WFF
proof end;
end;

definition
let x, y be bound_QC-variable;
func Sbst x,y -> CQC_Substitution equals :: SUBSTUT2:def 1
x .--> y;
coherence
x .--> y is CQC_Substitution
proof end;
end;

:: deftheorem defines Sbst SUBSTUT2:def 1 :
for x, y being bound_QC-variable holds Sbst x,y = x .--> y;

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

:: deftheorem defines . SUBSTUT2:def 2 :
for p being Element of CQC-WFF
for x, y being bound_QC-variable holds p . x,y = CQC_Sub [p,(Sbst x,y)];

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

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

theorem :: SUBSTUT2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being bound_QC-variable holds VERUM . x,y = VERUM
proof end;

theorem :: SUBSTUT2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for x, y being bound_QC-variable
for P being QC-pred_symbol of k
for l being CQC-variable_list of k 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for l being CQC-variable_list of k
for Sub being CQC_Substitution holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
proof end;

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

theorem Th16: :: SUBSTUT2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for Sub being CQC_Substitution holds [('not' p),Sub] = Sub_not [p,Sub]
proof end;

theorem :: SUBSTUT2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x, y being bound_QC-variable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds
for Sub being CQC_Substitution holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub])
proof end;

theorem Th19: :: SUBSTUT2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for Sub being CQC_Substitution holds [(p '&' q),Sub] = CQCSub_& [p,Sub],[q,Sub]
proof end;

theorem :: SUBSTUT2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for x, y being bound_QC-variable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF st ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) holds
for Sub being CQC_Substitution holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])
proof end;

definition
func CFQ -> Function of CQC-Sub-WFF , vSUB equals :: SUBSTUT2:def 3
QSub | CQC-Sub-WFF ;
coherence
QSub | CQC-Sub-WFF is Function of CQC-Sub-WFF , vSUB
proof end;
end;

:: deftheorem defines CFQ SUBSTUT2:def 3 :
CFQ = QSub | CQC-Sub-WFF ;

definition
let p be Element of CQC-WFF ;
let x be bound_QC-variable;
let Sub be CQC_Substitution;
func QScope p,x,Sub -> CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :] equals :: SUBSTUT2:def 4
[[p,(CFQ . [(All x,p),Sub])],x];
coherence
[[p,(CFQ . [(All x,p),Sub])],x] is CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
;
end;

:: deftheorem defines QScope SUBSTUT2:def 4 :
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution holds QScope p,x,Sub = [[p,(CFQ . [(All x,p),Sub])],x];

definition
let p be Element of CQC-WFF ;
let x be bound_QC-variable;
let Sub be CQC_Substitution;
func Qsc p,x,Sub -> second_Q_comp of QScope p,x,Sub equals :: SUBSTUT2:def 5
Sub;
coherence
Sub is second_Q_comp of QScope p,x,Sub
proof end;
end;

:: deftheorem defines Qsc SUBSTUT2:def 5 :
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution holds Qsc p,x,Sub = Sub;

theorem Th22: :: SUBSTUT2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable st ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds
for Sub being CQC_Substitution holds QuantNbr (All x,p) = QuantNbr (CQC_Sub [(All x,p),Sub])
proof end;

theorem Th24: :: SUBSTUT2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Sub being CQC_Substitution holds QuantNbr VERUM = QuantNbr (CQC_Sub [VERUM ,Sub])
proof end;

theorem :: SUBSTUT2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub])
proof end;

theorem :: SUBSTUT2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st p is atomic holds
ex k being Nat ex P being QC-pred_symbol of k ex ll being CQC-variable_list of k st p = P ! ll
proof end;

scheme :: SUBSTUT2:sch 3
CQCInd3{ P1[ set ] } :
for p being Element of CQC-WFF st QuantNbr p = 0 holds
P1[p]
provided
A1: for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( P1[ VERUM ] & P1[P ! l] & ( P1[r] implies P1[ 'not' r] ) & ( P1[r] & P1[s] implies P1[r '&' s] ) )
proof end;

definition
let G, H be QC-formula;
assume A1: G is_subformula_of H ;
mode PATH of G,H -> FinSequence means :Def6: :: SUBSTUT2:def 6
( 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 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 st
( b1 . k = G1 & b1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
proof end;
end;

:: deftheorem Def6 defines PATH SUBSTUT2:def 6 :
for G, H being QC-formula st G is_subformula_of H holds
for b3 being FinSequence holds
( b3 is PATH of G,H iff ( 1 <= len b3 & b3 . 1 = G & b3 . (len b3) = H & ( for k being Nat st 1 <= k & k < len b3 holds
ex G1, H1 being Element of QC-WFF st
( b3 . k = G1 & b3 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );

theorem :: SUBSTUT2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for F1, F2 being QC-formula
for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds
ex F3 being QC-formula st
( F3 = L . i & F3 is_subformula_of F2 )
proof end;

theorem Th28: :: SUBSTUT2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for p being Element of CQC-WFF
for F1 being QC-formula
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
proof end;

theorem Th29: :: SUBSTUT2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for q, p being Element of CQC-WFF
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 st
( r = L . i & QuantNbr r <= n )
proof end;

theorem :: SUBSTUT2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being Element of CQC-WFF st QuantNbr p = n & q is_subformula_of p holds
QuantNbr q <= n
proof end;

theorem :: SUBSTUT2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p being Element of CQC-WFF st ( for q being Element of CQC-WFF st q is_subformula_of p holds
QuantNbr q = n ) holds
n = 0
proof end;

theorem :: SUBSTUT2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st ( for q being Element of CQC-WFF st q is_subformula_of p holds
for x being bound_QC-variable
for r being Element of CQC-WFF holds q <> All x,r ) holds
QuantNbr p = 0
proof end;

theorem Th33: :: SUBSTUT2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st ( for q being Element of CQC-WFF st q is_subformula_of p holds
QuantNbr q <> 1 ) holds
QuantNbr p = 0
proof end;

theorem :: SUBSTUT2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st 1 <= QuantNbr p holds
ex q being Element of CQC-WFF st
( q is_subformula_of p & QuantNbr q = 1 ) by Th33;