:: The Subformula Tree of a Formula of the First Order Language
:: by Oleg Okhotnikov
::
:: Received October 2, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FINSEQ_1, RELAT_1, TREES_1, XBOOLE_0, ARYTM_3,
XXREAL_0, ORDINAL4, CARD_1, FUNCT_1, TARSKI, TREES_2, TREES_9, ORDINAL1,
NAT_1, FINSET_1, QC_LANG1, ZF_LANG, CLASSES2, TREES_4, QC_LANG4;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FINSET_1, FINSEQ_1,
FINSEQ_4, TREES_1, TREES_2, TREES_4, TREES_9, QC_LANG1, QC_LANG2,
XXREAL_0;
constructors BINOP_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_4, TREES_4, TREES_9,
QC_LANG2, RELSET_1, XTUPLE_0, NUMBERS;
registrations ORDINAL1, XREAL_0, NAT_1, FINSEQ_1, TREES_2, TREES_A, TREES_9,
CARD_1, RELAT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, TREES_2, TREES_4;
equalities XBOOLE_0, TREES_2;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, TREES_1, TREES_2, TREES_9,
GRFUNC_1, QC_LANG1, QC_LANG2, XBOOLE_0, FINSEQ_6, XREAL_1, XXREAL_0,
ORDINAL1;
schemes NAT_1, TREES_2, FINSEQ_1, TREES_9;
begin
reserve A for QC-alphabet;
reserve n,k,m for Nat;
reserve F,G,G9,H,H9 for Element of QC-WFF(A);
theorem Th1:
F is_subformula_of G implies len @ F <= len @ G
proof
assume
A1: F is_subformula_of G;
per cases;
suppose
F = G;
hence thesis;
end;
suppose
F <> G;
then F is_proper_subformula_of G by A1,QC_LANG2:def 21;
hence thesis by QC_LANG2:54;
end;
end;
theorem
F is_subformula_of G & len @ F = len @ G implies F = G by QC_LANG2:54,def 21;
definition
let A;
let p be Element of QC-WFF(A);
func list_of_immediate_constituents(p) -> FinSequence of QC-WFF(A) equals
:Def1:
<*> QC-WFF(A) if p = VERUM(A) or
p is atomic, <* the_argument_of p *> if p is
negative, <* the_left_argument_of p, the_right_argument_of p *> if p is
conjunctive otherwise <* the_scope_of p *>;
coherence;
consistency by QC_LANG1:20;
end;
theorem Th3:
k in dom list_of_immediate_constituents(F) & G = (
list_of_immediate_constituents(F)).k implies G is_immediate_constituent_of F
proof
assume that
A1: k in dom list_of_immediate_constituents(F) and
A2: G = (list_of_immediate_constituents(F)).k;
A3: list_of_immediate_constituents(F) <> <*>QC-WFF(A) by A1;
A4: F <> VERUM(A) & not F is atomic by Def1,A3;
per cases by A4,QC_LANG1:9;
suppose
A5: F is negative;
then
A6: list_of_immediate_constituents(F) = <* the_argument_of F *> by Def1;
then k in Seg 1 by A1,FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:2,TARSKI:def 1;
then G = the_argument_of F by A2,A6;
hence thesis by A5,QC_LANG2:48;
end;
suppose
A7: F is universal;
then
A8: not F is conjunctive by QC_LANG1:20;
(not F is atomic)& not F is negative by A7,QC_LANG1:20;
then
A9: list_of_immediate_constituents(F) = <* the_scope_of F *>
by A8,Def1,A4;
then k in Seg 1 by A1,FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:2,TARSKI:def 1;
then G = the_scope_of F by A2,A9;
hence thesis by A7,QC_LANG2:50;
end;
suppose
A10: F is conjunctive;
A13: list_of_immediate_constituents(F) = <* the_left_argument_of F,
the_right_argument_of F *> by A10,Def1;
len <* the_left_argument_of F, the_right_argument_of F *> = 2 by
FINSEQ_1:44;
then
A14: k in {1,2} by A1,A13,FINSEQ_1:2,def 3;
now
per cases by A14,TARSKI:def 2;
suppose
k = 1;
hence thesis by A2,A10,A13,QC_LANG2:49;
end;
suppose
k = 2;
hence thesis by A2,A10,A13,QC_LANG2:49;
end;
end;
hence thesis;
end;
suppose
A15: F is universal;
then
A16: not F is conjunctive by QC_LANG1:20;
(not F is atomic)& not F is negative by A15,QC_LANG1:20;
then
A17: list_of_immediate_constituents(F) = <* the_scope_of F *>
by A16,Def1,A4;
then k in Seg 1 by A1,FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:2,TARSKI:def 1;
then G = the_scope_of F by A2,A17;
hence thesis by A15,QC_LANG2:50;
end;
end;
theorem Th4:
rng list_of_immediate_constituents(F) = { G where G is Element
of QC-WFF(A) : G is_immediate_constituent_of F }
proof
thus rng list_of_immediate_constituents(F) c= { G where G is Element of
QC-WFF(A) : G is_immediate_constituent_of F }
proof
let y be object;
assume
A1: y in rng list_of_immediate_constituents(F);
rng list_of_immediate_constituents(F) c= QC-WFF(A) by FINSEQ_1:def 4;
then reconsider G = y as Element of QC-WFF(A) by A1;
ex x being object st x in dom list_of_immediate_constituents(F) & y = (
list_of_immediate_constituents(F)).x by A1,FUNCT_1:def 3;
then G is_immediate_constituent_of F by Th3;
hence thesis;
end;
thus { G where G is Element of QC-WFF(A) :
G is_immediate_constituent_of F } c=
rng list_of_immediate_constituents(F)
proof
let x be object;
assume
x in { G where G is Element of QC-WFF(A) :
G is_immediate_constituent_of F };
then consider G such that
A2: x = G and
A3: G is_immediate_constituent_of F;
ex n st n in dom list_of_immediate_constituents(F) & G = (
list_of_immediate_constituents(F)).n
proof
A4: F <> VERUM(A) by A3,QC_LANG2:41;
per cases by A3,A4,QC_LANG1:9,QC_LANG2:47;
suppose
F is negative;
then
A5: list_of_immediate_constituents(F) = <* the_argument_of F *> & G =
the_argument_of F by A3,Def1,QC_LANG2:48;
consider n such that
A6: n = 1;
dom <* the_argument_of F *> = Seg 1 & <* the_argument_of F *>.n =
the_argument_of F by A6,FINSEQ_1:def 8;
hence thesis by A6,A5,FINSEQ_1:3;
end;
suppose
A7: F is conjunctive;
A8: <* the_left_argument_of F, the_right_argument_of F *>.2 =
the_right_argument_of F;
len <* the_left_argument_of F, the_right_argument_of F *> = 2 by
FINSEQ_1:44;
then
A9: dom <* the_left_argument_of F, the_right_argument_of F *> = Seg 2
by FINSEQ_1:def 3;
A10: list_of_immediate_constituents(F) = <* the_left_argument_of F,
the_right_argument_of F *> by A7,Def1;
A11: <* the_left_argument_of F, the_right_argument_of F *>.1 =
the_left_argument_of F;
now
per cases by A3,A7,QC_LANG2:49;
suppose
A12: G = the_left_argument_of F;
1 in {1,2} by TARSKI:def 2;
hence thesis by A10,A11,A9,A12,FINSEQ_1:2;
end;
suppose
G = the_right_argument_of F;
hence thesis by A10,A8,A9,FINSEQ_1:3;
end;
end;
hence thesis;
end;
suppose
A13: F is universal;
then
A14: not F is conjunctive by QC_LANG1:20;
( not F is atomic)& not F is negative by A13,QC_LANG1:20;
then
A15: list_of_immediate_constituents(F) = <* the_scope_of F *> by A14,Def1,A4
;
consider n such that
A16: n = 1;
A17: G = the_scope_of F by A3,A13,QC_LANG2:50;
dom <* the_scope_of F *> = Seg 1 & <* the_scope_of F *>.n =
the_scope_of F by A16,FINSEQ_1:def 8;
hence thesis by A15,A16,A17,FINSEQ_1:3;
end;
end;
hence thesis by A2,FUNCT_1:def 3;
end;
end;
definition
let A;
let p be Element of QC-WFF(A);
func tree_of_subformulae(p) -> finite DecoratedTree of QC-WFF(A) means
:Def2:
it.{} = p & for x being Element of dom it holds succ(it,x) =
list_of_immediate_constituents(it.x);
existence
proof
deffunc F(Element of QC-WFF(A)) = len @ $1;
deffunc G(Element of QC-WFF(A)) = list_of_immediate_constituents $1;
consider W being finite-branching DecoratedTree of QC-WFF(A) such that
A1: W.{} = p & for x being Element of dom W, w being Element of QC-WFF(A)
st w = W.x holds succ(W,x) = G(w)
from TREES_9:sch 2;
A2: for t,t9 being Element of dom W, d being Element of QC-WFF(A) st t9 in
succ t & d = W.t9 holds F(d) < F(W.t)
proof
let t,t9 be Element of dom W, d be Element of QC-WFF(A) such that
A3: t9 in succ t and
A4: d = W.t9;
consider n such that
A5: t9 = t^<*n*> and
t^<*n*> in dom W by A3;
A6: W.t9 = succ(W,t).(n+1) by A5,TREES_9:40
.= (list_of_immediate_constituents(W.t)).(n+1) by A1;
dom list_of_immediate_constituents(W.t) = dom succ(W,t) by A1
.= dom (t succ) by TREES_9:38;
then n+1 in dom list_of_immediate_constituents(W.t) by A5,TREES_9:39;
hence thesis by A4,A6,Th3,QC_LANG2:51;
end;
W is finite from TREES_9:sch 3(A2);
then reconsider W as finite DecoratedTree of QC-WFF(A);
take W;
thus thesis by A1;
end;
uniqueness
proof
let t1, t2 be finite DecoratedTree of QC-WFF(A);
A7: for t1, t2 being finite DecoratedTree of QC-WFF(A) st
( t1.{} = p & for
x being Element of dom t1 holds succ(t1,x) = list_of_immediate_constituents(t1.
x) ) & ( t2.{} = p & for x being Element of dom t2 holds succ(t2,x) =
list_of_immediate_constituents(t2.x) ) holds t1 c= t2
proof
let t1, t2 be finite DecoratedTree of QC-WFF(A);
assume that
A8: t1.{} = p and
A9: for x being Element of dom t1 holds succ(t1,x) =
list_of_immediate_constituents(t1.x) and
A10: t2.{} = p and
A11: for x being Element of dom t2 holds succ(t2,x) =
list_of_immediate_constituents(t2.x);
defpred P[set] means $1 in dom t2 & t1.$1 = t2.$1;
A12: for t being Element of dom t1, n st P[t] & t^<*n*> in dom t1 holds
P[t^<*n*>]
proof
let t be Element of dom t1, n;
assume that
A13: P[t] and
A14: t^<*n*> in dom t1;
reconsider t9 = t as Element of dom t2 by A13;
A15: succ(t1,t) = list_of_immediate_constituents(t2.t9) by A9,A13
.= succ(t2,t9) by A11;
t^<*n*> in succ t by A14;
then n < card succ t by TREES_9:7;
then n < len (t succ) by TREES_9:def 5;
then n < len succ(t1,t) by TREES_9:28;
then n < len (t9 succ) by A15,TREES_9:28;
then n < card succ t9 by TREES_9:def 5;
then
A16: t9^<*n*> in succ t9 by TREES_9:7;
hence t^<*n*> in dom t2;
thus t1.(t^<*n*>) = succ(t2,t9).(n+1) by A14,A15,TREES_9:40
.= t2.(t^<*n*>) by A16,TREES_9:40;
end;
A17: P[{}] by A8,A10,TREES_1:22;
A18: for t being Element of dom t1 holds P[t] from TREES_2:sch 1(A17,A12
);
then for t being object st t in dom t1 holds t in dom t2;
then
A19: dom t1 c= dom t2;
for x being object st x in dom t1 holds t1.x = t2.x by A18;
hence thesis by A19,GRFUNC_1:2;
end;
assume ( t1.{} = p & for x being Element of dom t1 holds succ(t1,x) =
list_of_immediate_constituents(t1.x) )&( t2.{} = p & for x being Element of dom
t2 holds succ(t2,x) = list_of_immediate_constituents(t2.x) );
then t1 c= t2 & t2 c= t1 by A7;
hence thesis;
end;
end;
reserve t, t9, t99 for Element of dom tree_of_subformulae(F);
theorem Th5:
F in rng tree_of_subformulae(F)
proof
(tree_of_subformulae(F)).{} = F & {} in dom tree_of_subformulae(F) by Def2,
TREES_1:22;
hence thesis by FUNCT_1:def 3;
end;
theorem Th6:
t^<*n*> in dom tree_of_subformulae(F) implies ex G st G = (
tree_of_subformulae(F)).(t^<*n*>) & G is_immediate_constituent_of (
tree_of_subformulae(F)).t
proof
A1: succ t = {t^<*k*>: t^<*k*> in dom tree_of_subformulae(F)};
assume t^<*n*> in dom tree_of_subformulae(F);
then consider t9 such that
A2: t9 = t^<*n*>;
A3: rng list_of_immediate_constituents((tree_of_subformulae(F)).t) = { G1
where G1 is Element of QC-WFF(A) : G1 is_immediate_constituent_of (
tree_of_subformulae(F)).t } by Th4;
consider G such that
A4: G = (tree_of_subformulae(F)).t9;
t9 in {t^<*k*>: t^<*k*> in dom tree_of_subformulae(F)} by A2;
then G in rng succ((tree_of_subformulae(F)),t) by A4,A1,TREES_9:41;
then G in rng list_of_immediate_constituents((tree_of_subformulae(F)).t) by
Def2;
hence thesis by A2,A4,A3;
end;
theorem Th7:
H is_immediate_constituent_of (tree_of_subformulae(F)).t iff ex
n st t^<*n*> in dom tree_of_subformulae(F) & H = (tree_of_subformulae(F)).(t^<*
n*>)
proof
now
set G = (tree_of_subformulae(F)).t;
assume H is_immediate_constituent_of (tree_of_subformulae(F)).t;
then H in {H1 where H1 is Element of QC-WFF(A) : H1
is_immediate_constituent_of G };
then
A1: H in rng list_of_immediate_constituents(G) by Th4;
succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) by Def2;
then consider t9 such that
A2: H = (tree_of_subformulae(F)).t9 and
A3: t9 in succ t by A1,TREES_9:42;
ex n st t9 = t^<*n*> & t^<*n*> in dom tree_of_subformulae(F) by A3;
hence ex n st t^<*n*> in dom tree_of_subformulae(F) & H = (
tree_of_subformulae(F)).(t^<*n*>) by A2;
end;
hence H is_immediate_constituent_of (tree_of_subformulae(F)).t implies ex n
st t^<*n*> in dom tree_of_subformulae(F) & H = (tree_of_subformulae(F)).(t^<*n
*>);
given n such that
A4: t^<*n*> in dom tree_of_subformulae(F) and
A5: H = (tree_of_subformulae(F)).(t^<*n*>);
ex G st G = (tree_of_subformulae(F)).(t^<*n*>) & G
is_immediate_constituent_of (tree_of_subformulae(F)).t by A4,Th6;
hence thesis by A5;
end;
theorem Th8:
G in rng tree_of_subformulae(F) & H is_immediate_constituent_of
G implies H in rng tree_of_subformulae(F)
proof
assume that
A1: G in rng tree_of_subformulae(F) and
A2: H is_immediate_constituent_of G;
consider x being object such that
A3: x in dom tree_of_subformulae(F) and
A4: G = (tree_of_subformulae(F)).x by A1,FUNCT_1:def 3;
consider t such that
A5: t = x by A3;
ex n st t^<*n*> in dom tree_of_subformulae(F) & H = ( tree_of_subformulae
(F)).(t^<*n*>) by A2,A4,A5,Th7;
hence thesis by FUNCT_1:def 3;
end;
theorem Th9:
G in rng tree_of_subformulae(F) & H is_subformula_of G implies H
in rng tree_of_subformulae(F)
proof
assume that
A1: G in rng tree_of_subformulae(F) and
A2: H is_subformula_of G;
consider n being Nat, L being FinSequence such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = H and
A6: L.n = G and
A7: for k being Nat st 1 <= k & k < n ex H1,G1 being Element of QC-WFF(A) st
L.k = H1
& L.(k+1) = G1 & H1 is_immediate_constituent_of G1 by A2,QC_LANG2:def 20;
defpred P[Nat] means ex H9 st H9 = L.($1+1) & ($1+1) in dom L & H9 in rng
tree_of_subformulae(F);
A8: for k being Nat st k <> 0 & P[k] ex m being Nat st m < k & P[m]
proof
A9: Seg n = dom L by A4,FINSEQ_1:def 3;
let k be Nat;
assume that
A10: k <> 0 and
A11: P[k];
consider m being Nat such that
A12: m+1 = k by A10,NAT_1:6;
0 < k by A10;
then
A13: 0+1 <= k by NAT_1:13;
Seg len L = dom L by FINSEQ_1:def 3;
then
A14: k+1 <= n by A4,A11,FINSEQ_1:1;
then k in NAT & k < n by NAT_1:13,ORDINAL1:def 12;
then
A15: ex H1,G1 being Element of QC-WFF(A) st L.k = H1 & L.(k+1) = G1 & H1
is_immediate_constituent_of G1 by A7,A13;
k <= n by A14,NAT_1:13;
then
A16: k in dom L by A13,A9,FINSEQ_1:1;
m < k by A12,NAT_1:13;
hence thesis by A11,A12,A15,A16,Th8;
end;
A17: ex k being Nat st P[k]
proof
0 <> n by A3;
then
A18: ex k being Nat st k+1 = n by NAT_1:6;
Seg n = dom L by A4,FINSEQ_1:def 3;
hence thesis by A1,A6,A18,FINSEQ_1:3;
end;
P[0] from NAT_1:sch 7(A17,A8);
hence thesis by A5;
end;
theorem Th10:
G in rng tree_of_subformulae(F) iff G is_subformula_of F
proof
now
set T = dom tree_of_subformulae(F);
defpred P[set] means ex H st (tree_of_subformulae(F)).$1 = H & H
is_subformula_of F;
assume G in rng tree_of_subformulae(F);
then consider t being object such that
A1: t in dom tree_of_subformulae(F) and
A2: (tree_of_subformulae(F)).t = G by FUNCT_1:def 3;
reconsider t as Element of T by A1;
A3: for t being Element of T, n st P[t] & t^<*n*> in T holds P[t^<*n*>]
proof
let t be Element of T, n;
assume that
A4: P[t] and
A5: t^<*n*> in T;
(tree_of_subformulae(F)).(t^<*n*>) is Element of QC-WFF(A)
by A5,FUNCT_1:102;
then consider H9 such that
A6: (tree_of_subformulae(F)).(t^<*n*>) = H9;
consider H such that
A7: (tree_of_subformulae(F)).t = H and
A8: H is_subformula_of F by A4;
ex G9 st G9 = (tree_of_subformulae(F)).(t^<*n*>) & G9
is_immediate_constituent_of (tree_of_subformulae(F)).t by A5,Th6;
then H9 is_subformula_of H by A7,A6,QC_LANG2:52;
hence thesis by A8,A6,QC_LANG2:57;
end;
A9: P[{}]
by Def2;
for t being Element of T holds P[t] from TREES_2:sch 1(A9,A3);
then ex H st (tree_of_subformulae(F)).t = H & H is_subformula_of F;
hence G is_subformula_of F by A2;
end;
hence G in rng tree_of_subformulae(F) implies G is_subformula_of F;
assume G is_subformula_of F;
hence thesis by Th5,Th9;
end;
theorem
rng tree_of_subformulae(F) = Subformulae(F)
proof
thus rng tree_of_subformulae(F) c= Subformulae(F)
proof
let y be object;
assume
A1: y in rng tree_of_subformulae(F);
then y is Element of QC-WFF(A) by RELAT_1:167;
then consider G such that
A2: G = y;
G is_subformula_of F by A1,A2,Th10;
hence thesis by A2,QC_LANG2:def 22;
end;
thus Subformulae(F) c= rng tree_of_subformulae(F)
proof
let y be object;
assume y in Subformulae(F);
then ex G st G = y & G is_subformula_of F by QC_LANG2:def 22;
hence thesis by Th10;
end;
end;
theorem
t9 in succ t implies (tree_of_subformulae(F)).t9
is_immediate_constituent_of (tree_of_subformulae(F)).t
proof
assume t9 in succ t;
then ex n st t9 = t^<*n*> & t^<*n*> in dom tree_of_subformulae(F);
hence thesis by Th7;
end;
reserve x for set;
theorem Th13:
t is_a_prefix_of t9 implies (tree_of_subformulae(F)).t9
is_subformula_of (tree_of_subformulae(F)).t
proof
assume t is_a_prefix_of t9;
then consider r being FinSequence such that
A1: t9 = t^r by TREES_1:1;
reconsider r as FinSequence of NAT by A1,FINSEQ_1:36;
consider n such that
A2: n = len r;
defpred P[set,object] means ex G being QC-formula of A,
m,k1 being Nat, r1 being
FinSequence st G = $2 & m = $1 & m+k1 = n+1 & r1 = r|Seg k1 & G = (
tree_of_subformulae(F)).(t^r1);
A3: for k be Nat st k in Seg(n+1) ex x being object st P[k,x]
proof
let k be Nat;
assume k in Seg(n+1);
then k <= n+1 by FINSEQ_1:1;
then consider k1 being Nat such that
A4: k+k1 = n+1 by NAT_1:10;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
r|Seg k1 is FinSequence by FINSEQ_1:15;
then consider r1 being FinSequence such that
A5: r1 = r|Seg k1;
t^r1 in dom tree_of_subformulae(F)
proof
ex q being FinSequence st q = r|Seg k1 & q is_a_prefix_of r
by TREES_9:32;
hence thesis by A1,A5,FINSEQ_6:13,TREES_1:20;
end;
then reconsider t1 = t^r1 as Element of dom tree_of_subformulae(F);
consider G being QC-formula of A such that
A6: G = (tree_of_subformulae(F)).t1;
take G,G,k,k1,r1;
thus thesis by A4,A5,A6;
end;
ex L being FinSequence st dom L = Seg(n+1) & for k be Nat st k in Seg(n
+1) holds P[k,L.k] from FINSEQ_1:sch 1(A3);
then consider L being FinSequence such that
A7: dom L = Seg (n+1) and
A8: for k be Nat st k in Seg (n+1) holds ex G being QC-formula of A, m,k1
being Nat, r1 being FinSequence st G = L.k & m = k & m+k1 = n+1 & r1 = r|Seg k1
& G = (tree_of_subformulae(F)).(t^r1);
A9: len L = n+1 by A7,FINSEQ_1:def 3;
A10: for k st 1 <= k & k <= n+1 ex G being QC-formula of A,
k1 being Nat, r1
being FinSequence st G = L.k & k+k1 = n+1 & r1 = r|Seg k1 & G = (
tree_of_subformulae(F)).(t^r1)
proof
let k;
assume 1 <= k & k <= n+1;
then k in Seg (n+1) by FINSEQ_1:1;
then
ex G being QC-formula of A, m,k1 being Nat,
r1 being FinSequence st G = L.k
& m = k & m+k1 = n+1 & r1 = r|Seg k1 & G = ( tree_of_subformulae(F)).(t^r1) by
A8;
hence thesis;
end;
A11: for k st 1 <= k & k < n+1 ex H1,G1 being Element of QC-WFF(A)
st L.k = H1
& L.(k+1) = G1 & H1 is_immediate_constituent_of G1
proof
let k;
assume that
A12: 1 <= k and
A13: k < n+1;
consider H1 being QC-formula of A, k1 being Nat,
r1 being FinSequence such that
A14: H1 = L.k and
A15: k+k1 = n+1 and
A16: r1 = r|Seg k1 and
A17: H1 = (tree_of_subformulae(F)).(t^r1) by A10,A12,A13;
1 <= k+1 & k+1 <= n+1 by A12,A13,NAT_1:13;
then consider
G1 being QC-formula of A,
k2 being Nat, r2 being FinSequence such that
A18: G1 = L.(k+1) and
A19: (k+1)+k2 = n+1 and
A20: r2 = r|Seg k2 and
A21: G1 = (tree_of_subformulae(F)).(t^r2) by A10;
reconsider k1,k2 as Element of NAT by ORDINAL1:def 12;
k1+1 <= n+1 by A12,A15,XREAL_1:6;
then k2+1 <= len r by A2,A15,A19,XREAL_1:6;
then consider m being Element of NAT such that
A22: r1 = r2^<*m*> by A15,A16,A19,A20,TREES_9:33;
t^r2 in dom tree_of_subformulae(F)
proof
ex q being FinSequence st q = r|Seg k2 & q is_a_prefix_of r
by TREES_9:32;
hence thesis by A1,A20,FINSEQ_6:13,TREES_1:20;
end;
then reconsider t2 = t^r2 as Element of dom tree_of_subformulae(F);
A23: t2^<*m*> = t^r1 by A22,FINSEQ_1:32;
t2^<*m*> in dom tree_of_subformulae(F)
proof
ex q being FinSequence st q = r|Seg k1 & q is_a_prefix_of r
by TREES_9:32;
hence thesis by A1,A16,A23,FINSEQ_6:13,TREES_1:20;
end;
then H1 is_immediate_constituent_of G1 by A17,A21,A23,Th7;
hence thesis by A14,A18;
end;
A24: 0+1 <= n+1 by NAT_1:13;
then consider
G being QC-formula of A, k1 being Nat, r1 being FinSequence such that
A25: G = L.1 and
A26: 1+k1 = n+1 and
A27: r1 = r|Seg k1 and
A28: G = (tree_of_subformulae(F)).(t^r1) by A10;
A29: L.(n+1) = (tree_of_subformulae(F)).t
proof
consider G being QC-formula of A,
k1 being Nat, r1 being FinSequence such that
A30: G = L.(n+1) and
A31: (n+1)+k1 = n+1 & r1 = r|Seg k1 and
A32: G = (tree_of_subformulae(F)).(t^r1) by A24,A10;
r1 = {} by A31;
hence thesis by A30,A32,FINSEQ_1:34;
end;
dom r = Seg k1 by A2,A26,FINSEQ_1:def 3;
then t9 = t^r1 by A1,A27;
hence thesis by A24,A9,A25,A28,A29,A11,QC_LANG2:def 20;
end;
theorem Th14:
t is_a_proper_prefix_of t9 implies len @((tree_of_subformulae(F)
).t9) < len @((tree_of_subformulae(F)).t)
proof
set G = (tree_of_subformulae(F)).t;
set H = (tree_of_subformulae(F)).t9;
assume
A1: t is_a_proper_prefix_of t9;
then
A2: t is_a_prefix_of t9;
A3: now
consider r being FinSequence such that
A4: t9 = t^r by A2,TREES_1:1;
reconsider r as FinSequence of NAT by A4,FINSEQ_1:36;
A5: 1 <= len r
proof
reconsider t1 = {} as Element of dom tree_of_subformulae(F) by TREES_1:22
;
r <> {} & t1 is_a_prefix_of r by A1,A4,FINSEQ_1:34;
then
A6: t1 is_a_proper_prefix_of r;
len t1 = 0;
then 0 < len r by A6,TREES_1:6;
then 0+1 <= len r by NAT_1:13;
hence thesis;
end;
defpred P[set,object] means
ex t1 being Element of dom tree_of_subformulae(F)
, r1 being FinSequence, m being Nat st m = $1 & r1 = r|Seg m & t1 = t^r1 & $2 =
(tree_of_subformulae(F)).t1;
A7: for k be Nat st k in Seg len r ex x being object st P[k,x]
proof
let k be Nat such that
k in Seg len r;
r|Seg k is FinSequence by FINSEQ_1:15;
then consider r1 being FinSequence such that
A8: r1 = r|Seg k;
r1 is_a_prefix_of r by A8,TREES_1:def 1;
then t^r1 in dom tree_of_subformulae(F) by A4,FINSEQ_6:13,TREES_1:20;
then consider t1 being Element of dom tree_of_subformulae(F) such that
A9: t1 = t^r1;
ex x st x = (tree_of_subformulae(F)).t1;
hence thesis by A8,A9;
end;
ex L being FinSequence st dom L = Seg len r & for k be Nat st k in
Seg len r holds P[k,L.k] from FINSEQ_1:sch 1(A7);
then consider L being FinSequence such that
dom L = Seg len r and
A10: for k be Nat st k in Seg len r holds ex t1 being Element of dom
tree_of_subformulae(F), r1 being FinSequence, m being Nat st m = k & r1 = r|Seg
m & t1 = t^r1 & L.k = (tree_of_subformulae(F)).t1;
for k st 1 <= k & k <= len r holds ex t1 being Element of dom
tree_of_subformulae(F), r1 being FinSequence st r1 = r|Seg k & t1 = t^r1 & L.k
= (tree_of_subformulae(F)).t1
proof
let k;
assume 1 <= k & k <= len r;
then k in Seg len r by FINSEQ_1:1;
then ex t1 being Element of dom tree_of_subformulae(F), r1 being
FinSequence, m being Nat st m = k & r1 = r|Seg m & t1 = t^r1 & L.k = (
tree_of_subformulae(F)).t1 by A10;
hence thesis;
end;
then consider t1 being Element of dom tree_of_subformulae(F), r1 being
FinSequence such that
A11: r1 = r|Seg 1 and
A12: t1 = t^r1 and
L.1 = (tree_of_subformulae(F)).t1 by A5;
set H1 = (tree_of_subformulae(F)).t1;
A13: H1 is_immediate_constituent_of G
proof
ex m being Element of NAT st r1 = <*m*> by A5,A11,TREES_9:34;
hence thesis by A12,Th7;
end;
r1 is_a_prefix_of r by A11,TREES_1:def 1;
then t1 is_a_prefix_of t9 by A4,A12,FINSEQ_6:13;
then
A14: len @ H <= len @ H1 by Th1,Th13;
assume len @ H = len @ G;
hence contradiction by A14,A13,QC_LANG2:51;
end;
len @ H <= len @ G by A2,Th1,Th13;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th15:
t is_a_proper_prefix_of t9 implies (tree_of_subformulae(F)).t9
<> (tree_of_subformulae(F)).t
proof
set G = (tree_of_subformulae(F)).t;
set H = (tree_of_subformulae(F)).t9;
assume t is_a_proper_prefix_of t9;
then len @H < len @G by Th14;
hence thesis;
end;
theorem Th16:
t is_a_proper_prefix_of t9 implies (tree_of_subformulae(F)).t9
is_proper_subformula_of (tree_of_subformulae(F)).t
proof
set G = (tree_of_subformulae(F)).t;
set H = (tree_of_subformulae(F)).t9;
assume
A1: t is_a_proper_prefix_of t9;
then t is_a_prefix_of t9;
then
A2: H is_subformula_of G by Th13;
H <> G by A1,Th15;
hence thesis by A2,QC_LANG2:def 21;
end;
theorem
(tree_of_subformulae(F)).t = F iff t = {}
proof
now
reconsider t1 = {} as Element of dom tree_of_subformulae(F) by TREES_1:22;
assume
A1: (tree_of_subformulae(F)).t = F;
A2: t1 is_a_prefix_of t;
assume t <> {};
then t1 is_a_proper_prefix_of t by A2;
then (tree_of_subformulae(F)).t is_proper_subformula_of (
tree_of_subformulae(F)).t1 by Th16;
hence contradiction by A1,Def2;
end;
hence (tree_of_subformulae(F)).t = F implies t = {};
assume t = {};
hence thesis by Def2;
end;
theorem Th18:
t <> t9 & (tree_of_subformulae(F)).t = (tree_of_subformulae(F)).
t9 implies not t,t9 are_c=-comparable
proof
assume that
A1: t <> t9 and
A2: (tree_of_subformulae(F)).t = (tree_of_subformulae(F)).t9;
assume
A3: t,t9 are_c=-comparable;
per cases by A3;
suppose
t is_a_prefix_of t9;
then t is_a_proper_prefix_of t9 by A1;
hence contradiction by A2,Th16;
end;
suppose
t9 is_a_prefix_of t;
then t9 is_a_proper_prefix_of t by A1;
hence contradiction by A2,Th16;
end;
end;
definition
let A;
let F, G be Element of QC-WFF(A);
func F-entry_points_in_subformula_tree_of G -> AntiChain_of_Prefixes of dom
tree_of_subformulae(F) means
:Def3:
for t being Element of dom
tree_of_subformulae(F) holds t in it iff (tree_of_subformulae(F)).t = G;
existence
proof
consider X being set such that
A1: X = { t where t is Element of dom tree_of_subformulae(F) : (
tree_of_subformulae(F)).t = G };
A2: X is AntiChain_of_Prefixes of dom tree_of_subformulae(F)
proof
A3: for p1,p2 being FinSequence st p1 in X & p2 in X & p1 <> p2 holds
not p1,p2 are_c=-comparable
proof
let p1,p2 be FinSequence;
assume that
A4: p1 in X & p2 in X and
A5: p1 <> p2;
(ex t1 being Element of dom tree_of_subformulae(F) st t1 = p1 & (
tree_of_subformulae(F)).t1 = G )& ex t2 being Element of dom
tree_of_subformulae(F) st t2 = p2 & (tree_of_subformulae(F)).t2 = G by A1,A4;
hence thesis by A5,Th18;
end;
for x being set st x in X holds x is FinSequence
proof
let x be set;
assume x in X;
then ex t being Element of dom tree_of_subformulae(F) st t = x & (
tree_of_subformulae(F)).t = G by A1;
hence thesis;
end;
then reconsider X as AntiChain_of_Prefixes by A3,TREES_1:def 10;
X c= dom tree_of_subformulae(F)
proof
let x be object;
assume x in X;
then ex t being Element of dom tree_of_subformulae(F) st t = x & (
tree_of_subformulae(F)).t = G by A1;
hence thesis;
end;
hence thesis by TREES_1:def 11;
end;
for t being Element of dom tree_of_subformulae(F) holds t in X iff (
tree_of_subformulae(F)).t = G
proof
let t be Element of dom tree_of_subformulae(F);
thus t in X iff (tree_of_subformulae(F)).t = G
proof
now
assume t in X;
then ex t9 being Element of dom tree_of_subformulae(F) st t9 = t & (
tree_of_subformulae(F)).t9 = G by A1;
hence (tree_of_subformulae(F)).t = G;
end;
hence t in X implies (tree_of_subformulae(F)).t = G;
assume (tree_of_subformulae(F)).t = G;
hence thesis by A1;
end;
end;
hence thesis by A2;
end;
uniqueness
proof
let P1,P2 be AntiChain_of_Prefixes of dom tree_of_subformulae(F);
assume
A6: for t being Element of dom tree_of_subformulae(F) holds t in P1
iff (tree_of_subformulae(F)).t = G;
assume
A7: for t being Element of dom tree_of_subformulae(F) holds t in P2
iff (tree_of_subformulae(F)).t = G;
thus P1 c= P2
proof
let x be object such that
A8: x in P1;
P1 c= dom tree_of_subformulae(F) by TREES_1:def 11;
then reconsider t = x as Element of dom tree_of_subformulae(F) by A8;
(tree_of_subformulae(F)).t = G by A6,A8;
hence thesis by A7;
end;
thus P2 c= P1
proof
let x be object such that
A9: x in P2;
P2 c= dom tree_of_subformulae(F) by TREES_1:def 11;
then reconsider t = x as Element of dom tree_of_subformulae(F) by A9;
(tree_of_subformulae(F)).t = G by A7,A9;
hence thesis by A6;
end;
end;
end;
theorem Th19:
F-entry_points_in_subformula_tree_of G = { t where t is Element
of dom tree_of_subformulae(F) : (tree_of_subformulae(F)).t = G }
proof
thus F-entry_points_in_subformula_tree_of G c= { t where t is Element of dom
tree_of_subformulae(F) : (tree_of_subformulae(F)).t = G }
proof
let x be object;
assume
A1: x in F-entry_points_in_subformula_tree_of G;
F-entry_points_in_subformula_tree_of G c= dom tree_of_subformulae(F)
by TREES_1:def 11;
then reconsider t9 = x as Element of dom tree_of_subformulae(F) by A1;
(tree_of_subformulae(F)).t9 = G by A1,Def3;
hence thesis;
end;
thus { t where t is Element of dom tree_of_subformulae(F) : (
tree_of_subformulae(F)).t = G } c= F-entry_points_in_subformula_tree_of G
proof
let x be object;
assume x in { t where t is Element of dom tree_of_subformulae(F) : (
tree_of_subformulae(F)).t = G };
then ex t9 st t9 = x & (tree_of_subformulae(F)).t9 = G;
hence thesis by Def3;
end;
end;
theorem Th20:
G is_subformula_of F iff F-entry_points_in_subformula_tree_of G <> {}
proof
now
assume G is_subformula_of F;
then G in rng tree_of_subformulae(F) by Th10;
then ex x being object st x in dom tree_of_subformulae(F) & G = (
tree_of_subformulae(F)).x by FUNCT_1:def 3;
hence F-entry_points_in_subformula_tree_of G <> {} by Def3;
end;
hence G is_subformula_of F implies F-entry_points_in_subformula_tree_of G <>
{};
assume F-entry_points_in_subformula_tree_of G <> {};
then consider x being object such that
A1: x in F-entry_points_in_subformula_tree_of G by XBOOLE_0:def 1;
x in { t where t is Element of dom tree_of_subformulae(F) : (
tree_of_subformulae(F)).t = G } by A1,Th19;
then ex t st x = t & (tree_of_subformulae(F)).t = G;
then G in rng tree_of_subformulae(F) by FUNCT_1:def 3;
hence thesis by Th10;
end;
theorem Th21:
t9 = t^<*m*> & (tree_of_subformulae(F)).t is negative implies (
tree_of_subformulae(F)).t9 = the_argument_of (tree_of_subformulae(F)).t & m = 0
proof
set G = (tree_of_subformulae(F)).t;
set H = (tree_of_subformulae(F)).t9;
assume that
A1: t9 = t^<*m*> and
A2: G is negative;
A3: dom <* the_argument_of G *> = Seg 1 by FINSEQ_1:def 8;
A4: succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) & ex
q being Element of dom tree_of_subformulae(F) st q = t & succ(
tree_of_subformulae(F),t) = tree_of_subformulae(F)*(q succ) by Def2,
TREES_9:def 6;
list_of_immediate_constituents(G) = <* the_argument_of G *> by A2,Def1;
then dom <* the_argument_of G *> = dom (t succ) by A4,TREES_9:37;
then m+1 in dom <* the_argument_of G *> by A1,TREES_9:39;
then
A5: m+1 = 0+1 by A3,FINSEQ_1:2,TARSKI:def 1;
H is_immediate_constituent_of G by A1,Th7;
hence thesis by A2,A5,QC_LANG2:48;
end;
theorem Th22:
t9 = t^<*m*> & (tree_of_subformulae(F)).t is conjunctive implies
(tree_of_subformulae(F)).t9 = the_left_argument_of (tree_of_subformulae(F)).t &
m = 0 or (tree_of_subformulae(F)).t9 = the_right_argument_of (
tree_of_subformulae(F)).t & m = 1
proof
set G = (tree_of_subformulae(F)).t;
set H = (tree_of_subformulae(F)).t9;
assume that
A1: t9 = t^<*m*> and
A2: G is conjunctive;
A3: list_of_immediate_constituents(G) = <* the_left_argument_of G,
the_right_argument_of G *> by A2,Def1;
len <* the_left_argument_of G, the_right_argument_of G *> = 2 by FINSEQ_1:44;
then
A4: dom <* the_left_argument_of G, the_right_argument_of G *> = Seg 2 by
FINSEQ_1:def 3;
A5: succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) by Def2;
ex q being Element of dom tree_of_subformulae(F) st q = t & succ(
tree_of_subformulae(F),t) = tree_of_subformulae(F)*(q succ) by TREES_9:def 6;
then
dom <* the_left_argument_of G, the_right_argument_of G *> = dom (t succ)
by A5,A3,TREES_9:37;
then
m+1 in dom <* the_left_argument_of G, the_right_argument_of G *> by A1,
TREES_9:39;
then
A6: m+1 = 0+1 or m+1 = 1+1 by A4,FINSEQ_1:2,TARSKI:def 2;
per cases by A6;
suppose
A7: m = 0;
H = succ(tree_of_subformulae(F),t).(m+1) by A1,TREES_9:40
.= the_left_argument_of G by A5,A3,A7;
hence thesis by A7;
end;
suppose
A8: m = 1;
H = succ(tree_of_subformulae(F),t).(m+1) by A1,TREES_9:40
.= the_right_argument_of G by A5,A3,A8;
hence thesis by A8;
end;
end;
theorem Th23:
t9 = t^<*m*> & (tree_of_subformulae(F)).t is universal implies (
tree_of_subformulae(F)).t9 = the_scope_of (tree_of_subformulae(F)).t & m = 0
proof
set G = (tree_of_subformulae(F)).t;
set H = (tree_of_subformulae(F)).t9;
assume that
A1: t9 = t^<*m*> and
A2: G is universal;
A3: dom <* the_scope_of G *> = Seg 1 by FINSEQ_1:def 8;
A4: succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) & ex
q being Element of dom tree_of_subformulae(F) st q = t & succ(
tree_of_subformulae(F),t) = tree_of_subformulae(F)*(q succ) by Def2,
TREES_9:def 6;
VERUM(A) is not universal by QC_LANG1:20; then
A5: G <> VERUM(A) by A2;
G is non atomic non negative non conjunctive by A2,QC_LANG1:20;
then list_of_immediate_constituents(G) = <* the_scope_of G *> by Def1,A5;
then dom <* the_scope_of G *> = dom (t succ) by A4,TREES_9:37;
then m+1 in dom <* the_scope_of G *> by A1,TREES_9:39;
then
A6: m+1 = 0+1 by A3,FINSEQ_1:2,TARSKI:def 1;
H is_immediate_constituent_of G by A1,Th7;
hence thesis by A2,A6,QC_LANG2:50;
end;
theorem Th24:
(tree_of_subformulae(F)).t is negative implies t^<*0*> in dom
tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0*>) = the_argument_of (
tree_of_subformulae(F)).t
proof
set G = (tree_of_subformulae(F)).t;
consider H such that
A1: H = the_argument_of G;
assume
A2: G is negative;
then H is_immediate_constituent_of G by A1,QC_LANG2:48;
then consider m such that
A3: t^<*m*> in dom tree_of_subformulae(F) and
H = (tree_of_subformulae(F)).(t^<*m*>) by Th7;
m = 0 by A2,A3,Th21;
hence thesis by A2,A3,Th21;
end;
reserve x,y for set;
Lm1: dom <* x, y *> = Seg 2
proof
thus dom <* x, y *> = Seg len <* x, y *> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44;
end;
theorem Th25:
(tree_of_subformulae(F)).t is conjunctive implies t^<*0*> in dom
tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0*>) =
the_left_argument_of (tree_of_subformulae(F)).t & t^<*1*> in dom
tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*1*>) =
the_right_argument_of (tree_of_subformulae(F)).t
proof
set G = (tree_of_subformulae(F)).t;
assume
A1: G is conjunctive;
(tree_of_subformulae(F))*(t succ) = (succ(tree_of_subformulae(F),t))
proof
ex q being Element of dom tree_of_subformulae(F) st q = t & succ(
tree_of_subformulae(F),t) = (tree_of_subformulae(F))*(q succ) by TREES_9:def 6;
hence thesis;
end;
then
A2: dom (t succ) = dom (succ(tree_of_subformulae(F),t)) by TREES_9:37
.= dom (list_of_immediate_constituents(G)) by Def2
.= dom <* the_left_argument_of G, the_right_argument_of G *> by A1,Def1
.= {1,2} by Lm1,FINSEQ_1:2;
A3: 0+1 in {1,2} by TARSKI:def 2;
then t^<*0*> in dom tree_of_subformulae(F) by A2,TREES_9:39;
then
(tree_of_subformulae(F)).(t^<*0*>) = (succ(tree_of_subformulae(F),t)).(0
+1) by TREES_9:40
.= (list_of_immediate_constituents(G)).1 by Def2
.= <* the_left_argument_of G, the_right_argument_of G *>.1 by A1,Def1
.= the_left_argument_of G;
hence
t^<*0*> in dom tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0
*>) = the_left_argument_of (tree_of_subformulae(F)).t by A2,A3,TREES_9:39;
A4: 1+1 in {1,2} by TARSKI:def 2;
then t^<*1*> in dom tree_of_subformulae(F) by A2,TREES_9:39;
then
(tree_of_subformulae(F)).(t^<*1*>) = (succ(tree_of_subformulae(F),t)).(
1+1) by TREES_9:40
.= (list_of_immediate_constituents(G)).2 by Def2
.= <* the_left_argument_of G, the_right_argument_of G *>.2 by A1,Def1
.= the_right_argument_of G;
hence thesis by A2,A4,TREES_9:39;
end;
theorem Th26:
(tree_of_subformulae(F)).t is universal implies t^<*0*> in dom
tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0*>) = the_scope_of (
tree_of_subformulae(F)).t
proof
set G = (tree_of_subformulae(F)).t;
consider H such that
A1: H = the_scope_of G;
assume
A2: G is universal;
then H is_immediate_constituent_of G by A1,QC_LANG2:50;
then consider m such that
A3: t^<*m*> in dom tree_of_subformulae(F) and
H = (tree_of_subformulae(F)).(t^<*m*>) by Th7;
m = 0 by A2,A3,Th23;
hence thesis by A2,A3,Th23;
end;
reserve t for Element of dom tree_of_subformulae(F),
s for Element of dom tree_of_subformulae(G);
theorem Th27:
t in F-entry_points_in_subformula_tree_of G & s in G
-entry_points_in_subformula_tree_of H implies t^s in F
-entry_points_in_subformula_tree_of H
proof
defpred P[Nat] means for F,G,H,t,s holds G = (tree_of_subformulae
(F)).t & H = (tree_of_subformulae(G)).s & len s = $1 implies t^s in F
-entry_points_in_subformula_tree_of H;
A1: for k st P[k] holds P[k + 1]
proof
let k such that
A2: P[k];
thus P[k + 1]
proof
A3: 1 in {1} by TARSKI:def 1;
let F,G,H,t,s;
assume that
A4: G = (tree_of_subformulae(F)).t and
A5: H = (tree_of_subformulae(G)).s and
A6: len s = k+1;
consider v being FinSequence, x being set such that
A7: s = v^<*x*> and
A8: len v = k by A6,TREES_2:3;
reconsider u = <*x*> as FinSequence of NAT by A7,FINSEQ_1:36;
A9: rng u c= NAT by FINSEQ_1:def 4;
dom u = Seg 1 & u.1 = x by FINSEQ_1:def 8;
then x in rng u by A3,FINSEQ_1:2,FUNCT_1:def 3;
then reconsider m = x as Element of NAT by A9;
reconsider v as FinSequence of NAT by A7,FINSEQ_1:36;
reconsider s9 = v as Element of dom tree_of_subformulae(G) by A7,
TREES_1:21;
consider H9 such that
A10: H9 = (tree_of_subformulae(G)).s9;
A11: t^s9 in F-entry_points_in_subformula_tree_of H9 by A2,A4,A8,A10;
F-entry_points_in_subformula_tree_of H9 c= dom tree_of_subformulae(
F) by TREES_1:def 11;
then consider t9 being Element of dom tree_of_subformulae(F) such that
A12: t9 = t^s9 by A11;
A13: H9 = (tree_of_subformulae(F)).t9 by A11,A12,Def3;
A14: s = s9^<*m*> by A7;
then
A15: H is_immediate_constituent_of H9 by A5,A10,Th7;
A16: H = (tree_of_subformulae(F)).(t9^<*m*>) & t9^<*m*> in dom
tree_of_subformulae(F)
proof
A17: H9 <> VERUM(A) by A15,QC_LANG2:41;
now
per cases by A15,A17,QC_LANG1:9,QC_LANG2:47;
suppose
A18: H9 is negative;
then H = the_argument_of H9 & m = 0 by A5,A14,A10,Th21;
hence thesis by A13,A18,Th24;
end;
suppose
A19: H9 is conjunctive;
then H = the_left_argument_of H9 & m = 0 or H =
the_right_argument_of H9 & m = 1 by A5,A14,A10,Th22;
hence thesis by A13,A19,Th25;
end;
suppose
A20: H9 is universal;
then H = the_scope_of H9 & m = 0 by A5,A14,A10,Th23;
hence thesis by A13,A20,Th26;
end;
end;
hence thesis;
end;
t^s = t9^<*m*> by A7,A12,FINSEQ_1:32;
hence thesis by A16,Def3;
end;
end;
A21: P[0]
proof
let F,G,H,t,s;
assume that
A22: G = (tree_of_subformulae(F)).t and
A23: H = (tree_of_subformulae(G)).s and
A24: len s = 0;
A25: s = {} by A24;
then
A26: t^s = t by FINSEQ_1:34;
H = G by A23,A25,Def2;
hence thesis by A22,A26,Def3;
end;
for k holds P[k] from NAT_1:sch 2(A21,A1);
then
A27: G = (tree_of_subformulae(F)).t & H = (tree_of_subformulae(G)).s & len s
= len s implies t^s in F-entry_points_in_subformula_tree_of H;
assume t in F-entry_points_in_subformula_tree_of G & s in G
-entry_points_in_subformula_tree_of H;
hence thesis by A27,Def3;
end;
reserve t for Element of dom tree_of_subformulae(F),
s for FinSequence;
theorem Th28:
t in F-entry_points_in_subformula_tree_of G & t^s in F
-entry_points_in_subformula_tree_of H implies s in G
-entry_points_in_subformula_tree_of H
proof
defpred P[Nat] means for F,G,H,t,s holds G = (tree_of_subformulae
(F)).t & t^s in F-entry_points_in_subformula_tree_of H & len s = $1 implies s
in G-entry_points_in_subformula_tree_of H;
A1: for k st P[k] holds P[k + 1]
proof
let k such that
A2: P[k];
thus P[k + 1]
proof
let F,G,H,t,s;
assume that
A3: G = (tree_of_subformulae(F)).t and
A4: t^s in F-entry_points_in_subformula_tree_of H and
A5: len s = k+1;
consider v being FinSequence, x being set such that
A6: s = v^<*x*> and
A7: len v = k by A5,TREES_2:3;
F-entry_points_in_subformula_tree_of H = { t1 where t1 is Element
of dom tree_of_subformulae(F) : (tree_of_subformulae(F)).t1 = H } by Th19;
then consider t99 such that
A8: t99 = t^s and
A9: (tree_of_subformulae(F)).t99 = H by A4;
reconsider s1 = s as FinSequence of NAT by A8,FINSEQ_1:36;
A10: s1 = v^<*x*> by A6;
then reconsider u = <*x*> as FinSequence of NAT by FINSEQ_1:36;
reconsider v as FinSequence of NAT by A10,FINSEQ_1:36;
A11: rng u c= NAT by FINSEQ_1:def 4;
A12: 1 in {1} by TARSKI:def 1;
dom u = Seg 1 & u.1 = x by FINSEQ_1:def 8;
then x in rng u by A12,FINSEQ_1:2,FUNCT_1:def 3;
then reconsider m = x as Element of NAT by A11;
consider t9 being FinSequence of NAT such that
A13: t9 = t^v;
A14: t99 = t9^<*m*> by A6,A8,A13,FINSEQ_1:32;
then t9 is_a_prefix_of t99 by TREES_1:1;
then reconsider t9 as Element of dom tree_of_subformulae(F) by TREES_1:20
;
consider H9 such that
A15: H9 = (tree_of_subformulae(F)).t9;
t^v in F-entry_points_in_subformula_tree_of H9 by A13,A15,Def3;
then
A16: v in G-entry_points_in_subformula_tree_of H9 by A2,A3,A7;
G-entry_points_in_subformula_tree_of H9 = { v1 where v1 is Element
of dom tree_of_subformulae(G) : (tree_of_subformulae(G)).v1 = H9 } by Th19;
then
A17: ex v1 being Element of dom tree_of_subformulae(G) st v = v1 & (
tree_of_subformulae(G)).v1 = H9 by A16;
then reconsider v as Element of dom tree_of_subformulae(G);
A18: H is_immediate_constituent_of H9 by A9,A14,A15,Th7;
H = (tree_of_subformulae(G)).(v^<*m*>) & v^<*m*> in dom
tree_of_subformulae(G)
proof
A19: H9 <> VERUM(A) by A18,QC_LANG2:41;
now
per cases by A18,A19,QC_LANG1:9,QC_LANG2:47;
suppose
A20: H9 is negative;
then H = the_argument_of H9 & m = 0 by A9,A14,A15,Th21;
hence thesis by A17,A20,Th24;
end;
suppose
A21: H9 is conjunctive;
then H = the_left_argument_of H9 & m = 0 or H =
the_right_argument_of H9 & m = 1 by A9,A14,A15,Th22;
hence thesis by A17,A21,Th25;
end;
suppose
A22: H9 is universal;
then H = the_scope_of H9 & m = 0 by A9,A14,A15,Th23;
hence thesis by A17,A22,Th26;
end;
end;
hence thesis;
end;
hence thesis by A6,Def3;
end;
end;
A23: P[0]
proof
let F,G,H,t,s;
assume that
A24: G = (tree_of_subformulae(F)).t and
A25: t^s in F-entry_points_in_subformula_tree_of H and
A26: len s = 0;
A27: s = {} by A26;
then reconsider s9 = s as Element of dom tree_of_subformulae(G) by
TREES_1:22;
A28: G = (tree_of_subformulae(G)).s9 by A27,Def2;
F-entry_points_in_subformula_tree_of H = { t1 where t1 is Element of
dom tree_of_subformulae(F) : (tree_of_subformulae(F)).t1 = H } by Th19;
then ex t9 st t9 = t^s & (tree_of_subformulae(F)).t9 = H by A25;
then H = G by A24,A27,FINSEQ_1:34;
hence thesis by A28,Def3;
end;
for k holds P[k] from NAT_1:sch 2(A23,A1);
then
A29: G = (tree_of_subformulae(F)).t & t^s in F
-entry_points_in_subformula_tree_of H & len s = len s implies s in G
-entry_points_in_subformula_tree_of H;
assume t in F-entry_points_in_subformula_tree_of G & t^s in F
-entry_points_in_subformula_tree_of H;
hence thesis by A29,Def3;
end;
theorem Th29:
for F,G,H holds { t^s where t is Element of dom
tree_of_subformulae(F), s is Element of dom tree_of_subformulae(G) : t in F
-entry_points_in_subformula_tree_of G & s in G
-entry_points_in_subformula_tree_of H } c= F-entry_points_in_subformula_tree_of
H
proof
let F,G,H;
let x be object;
assume x in { t^s where t is Element of dom tree_of_subformulae(F), s is
Element of dom tree_of_subformulae(G) : t in F
-entry_points_in_subformula_tree_of G & s in G
-entry_points_in_subformula_tree_of H };
then
ex t being Element of dom tree_of_subformulae(F), s being Element of dom
tree_of_subformulae(G) st x = t^s & t in F -entry_points_in_subformula_tree_of
G & s in G -entry_points_in_subformula_tree_of H;
hence thesis by Th27;
end;
theorem Th30:
(tree_of_subformulae(F))|t = tree_of_subformulae(( tree_of_subformulae(F)).t)
proof
set T1 = (tree_of_subformulae(F))|t;
set T2 = tree_of_subformulae((tree_of_subformulae(F)).t);
thus
A1: dom T1 = dom T2
proof
let p be FinSequence of NAT;
now
consider G such that
A2: G = (tree_of_subformulae(F)).t;
A3: t in F-entry_points_in_subformula_tree_of G by A2,Def3;
consider t9 being FinSequence of NAT such that
A4: t9 = t^p;
assume p in dom T1;
then p in (dom tree_of_subformulae(F))|t by TREES_2:def 10;
then reconsider t9 as Element of dom tree_of_subformulae(F) by A4,
TREES_1:def 6;
consider H such that
A5: H = (tree_of_subformulae(F)).t9;
A6: G-entry_points_in_subformula_tree_of H c= dom T2 by A2,TREES_1:def 11;
t9 in F-entry_points_in_subformula_tree_of H by A5,Def3;
then p in G-entry_points_in_subformula_tree_of H by A3,A4,Th28;
hence p in dom T2 by A6;
end;
hence p in dom T1 implies p in dom T2;
now
consider G such that
A7: G = (tree_of_subformulae(F)).t;
assume p in dom T2;
then reconsider s = p as Element of dom tree_of_subformulae(G) by A7;
consider H such that
A8: H = (tree_of_subformulae(G)).s;
A9: s in G-entry_points_in_subformula_tree_of H by A8,Def3;
A10: F-entry_points_in_subformula_tree_of H c= dom tree_of_subformulae(F
) by TREES_1:def 11;
t in F-entry_points_in_subformula_tree_of G by A7,Def3;
then t^s in F-entry_points_in_subformula_tree_of H by A9,Th27;
then s in (dom tree_of_subformulae(F))|t by A10,TREES_1:def 6;
hence p in dom T1 by TREES_2:def 10;
end;
hence thesis;
end;
now
let p be Node of T1;
consider G such that
A11: G = (tree_of_subformulae(F)).t;
reconsider s = p as Element of dom tree_of_subformulae(G) by A1,A11;
A12: dom T1 = (dom tree_of_subformulae(F))|t by TREES_2:def 10;
then reconsider t9= t^s as Element of dom tree_of_subformulae(F) by
TREES_1:def 6;
consider H such that
A13: H = T1.p;
A14: t in F-entry_points_in_subformula_tree_of G by A11,Def3;
T1.p = (tree_of_subformulae(F)).(t^p) by A12,TREES_2:def 10;
then t9 in F-entry_points_in_subformula_tree_of H by A13,Def3;
then s in G-entry_points_in_subformula_tree_of H by A14,Th28;
hence T1.p = T2.p by A11,A13,Def3;
end;
hence for p being Node of T1 holds T1.p = T2.p;
end;
theorem Th31:
t in F-entry_points_in_subformula_tree_of G iff (
tree_of_subformulae(F))|t = tree_of_subformulae(G)
proof
now
assume t in F-entry_points_in_subformula_tree_of G;
then (tree_of_subformulae(F)).t = G by Def3;
hence (tree_of_subformulae(F))|t = tree_of_subformulae(G) by Th30;
end;
hence t in F-entry_points_in_subformula_tree_of G implies (
tree_of_subformulae(F))|t = tree_of_subformulae(G);
now
assume (tree_of_subformulae(F))|t = tree_of_subformulae(G);
then
A1: (tree_of_subformulae(F)).t = (tree_of_subformulae(G)).{} by TREES_9:35;
(tree_of_subformulae(G)).{} = G by Def2;
hence t in F-entry_points_in_subformula_tree_of G by A1,Def3;
end;
hence thesis;
end;
theorem
F-entry_points_in_subformula_tree_of G = { t where t is Element of dom
tree_of_subformulae(F) : (tree_of_subformulae(F))|t = tree_of_subformulae(G) }
proof
thus F-entry_points_in_subformula_tree_of G c= { t where t is Element of dom
tree_of_subformulae(F) : (tree_of_subformulae(F))|t = tree_of_subformulae(G) }
proof
let x be object;
assume
A1: x in F-entry_points_in_subformula_tree_of G;
F-entry_points_in_subformula_tree_of G c= dom tree_of_subformulae(F)
by TREES_1:def 11;
then reconsider t9 = x as Element of dom tree_of_subformulae(F) by A1;
(tree_of_subformulae(F))|t9 = tree_of_subformulae(G) by A1,Th31;
hence thesis;
end;
thus { t where t is Element of dom tree_of_subformulae(F) : (
tree_of_subformulae(F))|t = tree_of_subformulae(G) } c= F
-entry_points_in_subformula_tree_of G
proof
let x be object;
assume x in { t where t is Element of dom tree_of_subformulae(F) : (
tree_of_subformulae(F))|t = tree_of_subformulae(G) };
then
ex t9 st t9 = x & (tree_of_subformulae(F))|t9 = tree_of_subformulae(G);
hence thesis by Th31;
end;
end;
reserve C for Chain of dom tree_of_subformulae(F);
theorem
for F,G,H,C st G in { (tree_of_subformulae(F)).t where t is Element of
dom tree_of_subformulae(F) : t in C } & H in { (tree_of_subformulae(F)).t where
t is Element of dom tree_of_subformulae(F) : t in C } holds G is_subformula_of
H or H is_subformula_of G
proof
let F,G,H,C;
assume that
A1: G in { (tree_of_subformulae(F)).t where t is Element of dom
tree_of_subformulae(F) : t in C } and
A2: H in { (tree_of_subformulae(F)).t where t is Element of dom
tree_of_subformulae(F) : t in C };
consider t9 such that
A3: G = (tree_of_subformulae(F)).t9 and
A4: t9 in C by A1;
consider t99 such that
A5: H = (tree_of_subformulae(F)).t99 and
A6: t99 in C by A2;
A7: t9,t99 are_c=-comparable by A4,A6,TREES_2:def 3;
per cases by A7;
suppose
t9 is_a_prefix_of t99;
hence thesis by A3,A5,Th13;
end;
suppose
t99 is_a_prefix_of t9;
hence thesis by A3,A5,Th13;
end;
end;
definition
let A;
let F be Element of QC-WFF(A);
mode Subformula of F -> Element of QC-WFF(A) means
:Def4:
it is_subformula_of F;
existence;
end;
definition
let A;
let F be Element of QC-WFF(A);
let G be Subformula of F;
mode Entry_Point_in_Subformula_Tree of G -> Element of dom
tree_of_subformulae(F) means
:Def5:
(tree_of_subformulae(F)).it = G;
existence
proof
G is_subformula_of F by Def4;
then G in rng tree_of_subformulae(F) by Th10;
then ex x being object st x in dom tree_of_subformulae(F) & (
tree_of_subformulae(F)).x = G by FUNCT_1:def 3;
hence thesis;
end;
end;
reserve G for Subformula of F;
reserve t, t9 for Entry_Point_in_Subformula_Tree of G;
theorem
t <> t9 implies not t,t9 are_c=-comparable
proof
assume
A1: t <> t9;
(tree_of_subformulae(F)).t = G & (tree_of_subformulae(F)).t9 = G by Def5;
hence thesis by A1,Th18;
end;
definition
let A;
let F be Element of QC-WFF(A);
let G be Subformula of F;
func entry_points_in_subformula_tree(G) -> non empty AntiChain_of_Prefixes
of dom tree_of_subformulae(F) equals
F-entry_points_in_subformula_tree_of G;
coherence
by Def4,Th20;
end;
theorem Th35:
t in entry_points_in_subformula_tree(G)
proof
(tree_of_subformulae(F)).t = G by Def5;
hence thesis by Def3;
end;
theorem Th36:
entry_points_in_subformula_tree(G) = { t where t is
Entry_Point_in_Subformula_Tree of G : t = t }
proof
thus entry_points_in_subformula_tree(G) c= { t where t is
Entry_Point_in_Subformula_Tree of G : t = t }
proof
let x be object;
assume x in entry_points_in_subformula_tree(G);
then x in { t where t is Element of dom tree_of_subformulae(F) : (
tree_of_subformulae(F)).t = G } by Th19;
then consider t9 being Element of dom tree_of_subformulae(F) such that
A1: t9 = x and
A2: (tree_of_subformulae(F)).t9 = G;
reconsider t9 as Entry_Point_in_Subformula_Tree of G by A2,Def5;
t9 = t9;
hence thesis by A1;
end;
thus { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c=
entry_points_in_subformula_tree(G)
proof
let x be object;
assume x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t };
then ex t st t = x & t = t;
hence thesis by Th35;
end;
end;
reserve G1, G2 for Subformula of F,
t1 for Entry_Point_in_Subformula_Tree of G1,
s for Element of dom tree_of_subformulae(G1);
theorem Th37:
s in G1-entry_points_in_subformula_tree_of G2 implies t1^s is
Entry_Point_in_Subformula_Tree of G2
proof
(tree_of_subformulae(F)).t1 = G1 by Def5;
then
A1: t1 in F-entry_points_in_subformula_tree_of G1 by Def3;
assume s in G1-entry_points_in_subformula_tree_of G2;
then
A2: t1^s in F-entry_points_in_subformula_tree_of G2 by A1,Th27;
F-entry_points_in_subformula_tree_of G2 c= dom tree_of_subformulae(F) by
TREES_1:def 11;
then reconsider t9 = t1^s as Element of dom tree_of_subformulae(F) by A2;
(tree_of_subformulae(F)).t9 = G2 by A2,Def3;
hence thesis by Def5;
end;
reserve s for FinSequence;
theorem
t1^s is Entry_Point_in_Subformula_Tree of G2 implies s in G1
-entry_points_in_subformula_tree_of G2
proof
consider t9 being FinSequence such that
A1: t9 = t1^s;
(tree_of_subformulae(F)).t1 = G1 by Def5;
then
A2: t1 in F-entry_points_in_subformula_tree_of G1 by Def3;
assume t1^s is Entry_Point_in_Subformula_Tree of G2;
then
t9 in { t2 where t2 is Entry_Point_in_Subformula_Tree of G2 : t2 = t2 }
by A1;
then t9 in entry_points_in_subformula_tree(G2) by Th36;
hence thesis by A2,A1,Th28;
end;
theorem Th39:
for F,G1,G2 holds { t^s where t is
Entry_Point_in_Subformula_Tree of G1, s is Element of dom tree_of_subformulae(
G1) : s in G1-entry_points_in_subformula_tree_of G2 } = { t^s where t is
Element of dom tree_of_subformulae(F), s is Element of dom tree_of_subformulae(
G1) : t in F-entry_points_in_subformula_tree_of G1 & s in G1
-entry_points_in_subformula_tree_of G2 }
proof
let F,G1,G2;
thus { t^s where t is Entry_Point_in_Subformula_Tree of G1, s is Element of
dom tree_of_subformulae(G1) : s in G1-entry_points_in_subformula_tree_of G2 }
c= { t^s where t is Element of dom tree_of_subformulae(F), s is Element of dom
tree_of_subformulae(G1) : t in F-entry_points_in_subformula_tree_of G1 & s in
G1-entry_points_in_subformula_tree_of G2 }
proof
let x be object;
assume x in { t^s where t is Entry_Point_in_Subformula_Tree of G1, s is
Element of dom tree_of_subformulae(G1) : s in G1
-entry_points_in_subformula_tree_of G2 };
then consider
t1 being Entry_Point_in_Subformula_Tree of G1, s1 being Element
of dom tree_of_subformulae(G1) such that
A1: x = t1^s1 & s1 in G1-entry_points_in_subformula_tree_of G2;
(tree_of_subformulae(F)).t1 = G1 by Def5;
then t1 in F-entry_points_in_subformula_tree_of G1 by Def3;
hence thesis by A1;
end;
thus { t^s where t is Element of dom tree_of_subformulae(F), s is Element of
dom tree_of_subformulae(G1) : t in F-entry_points_in_subformula_tree_of G1 & s
in G1-entry_points_in_subformula_tree_of G2 } c= { t^s where t is
Entry_Point_in_Subformula_Tree of G1, s is Element of dom tree_of_subformulae(
G1) : s in G1-entry_points_in_subformula_tree_of G2 }
proof
let x be object;
assume x in { t^s where t is Element of dom tree_of_subformulae(F), s is
Element of dom tree_of_subformulae(G1) : t in F
-entry_points_in_subformula_tree_of G1 & s in G1
-entry_points_in_subformula_tree_of G2 };
then consider
t1 being Element of dom tree_of_subformulae(F), s1 being Element
of dom tree_of_subformulae(G1) such that
A2: x = t1^s1 and
A3: t1 in F-entry_points_in_subformula_tree_of G1 and
A4: s1 in G1-entry_points_in_subformula_tree_of G2;
(tree_of_subformulae(F)).t1 = G1 by A3,Def3;
then reconsider t1 as Entry_Point_in_Subformula_Tree of G1 by Def5;
x = t1^s1 by A2;
hence thesis by A4;
end;
end;
theorem
for F,G1,G2 holds { t^s where t is Entry_Point_in_Subformula_Tree of
G1, s is Element of dom tree_of_subformulae(G1) : s in G1
-entry_points_in_subformula_tree_of G2 } c= entry_points_in_subformula_tree(G2)
proof
let F,G1,G2;
{ t^s where t is Entry_Point_in_Subformula_Tree of G1, s is Element of
dom tree_of_subformulae(G1) : s in G1-entry_points_in_subformula_tree_of G2 } =
{ t^s where t is Element of dom tree_of_subformulae(F), s is Element of dom
tree_of_subformulae(G1) : t in F-entry_points_in_subformula_tree_of G1 & s in
G1-entry_points_in_subformula_tree_of G2 } by Th39;
hence thesis by Th29;
end;
reserve G1, G2 for Subformula of F,
t1 for Entry_Point_in_Subformula_Tree of G1,
t2 for Entry_Point_in_Subformula_Tree of G2;
theorem
(ex t1,t2 st t1 is_a_prefix_of t2) implies G2 is_subformula_of G1
proof
given t1,t2 such that
A1: t1 is_a_prefix_of t2;
(tree_of_subformulae(F)).t1 = G1 & (tree_of_subformulae(F)).t2 = G2 by Def5;
hence thesis by A1,Th13;
end;
theorem
G2 is_subformula_of G1 implies for t1 ex t2 st t1 is_a_prefix_of t2
proof
assume
A1: G2 is_subformula_of G1;
now
let t1;
consider H being Element of QC-WFF(A) such that
A2: H = G2;
reconsider H as Subformula of G1 by A1,A2,Def4;
set s = the Entry_Point_in_Subformula_Tree of H;
(tree_of_subformulae(G1)).s = H by Def5;
then s in G1-entry_points_in_subformula_tree_of G2 by A2,Def3;
then t1^s is Entry_Point_in_Subformula_Tree of G2 by Th37;
then consider t2 such that
A3: t2 = t1^s;
take t2;
thus t1 is_a_prefix_of t2 by A3,TREES_1:1;
end;
hence thesis;
end;