:: The Subformula Tree of a Formula of the First Order Language
:: by Oleg Okhotnikov
::
:: Received October 2, 1995
:: Copyright (c) 1995-2017 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;
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 :: QC_LANG4:1
F is_subformula_of G implies len @ F <= len @ G;
theorem :: QC_LANG4:2
F is_subformula_of G & len @ F = len @ G implies F = G;
definition
let A;
let p be Element of QC-WFF(A);
func list_of_immediate_constituents(p) -> FinSequence of QC-WFF(A) equals
:: QC_LANG4:def 1
<*> 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 *>;
end;
theorem :: QC_LANG4:3
k in dom list_of_immediate_constituents(F) & G = (
list_of_immediate_constituents(F)).k implies G is_immediate_constituent_of F;
theorem :: QC_LANG4:4
rng list_of_immediate_constituents(F) = { G where G is Element
of QC-WFF(A) : G is_immediate_constituent_of F };
definition
let A;
let p be Element of QC-WFF(A);
func tree_of_subformulae(p) -> finite DecoratedTree of QC-WFF(A) means
:: QC_LANG4:def 2
it.{} = p & for x being Element of dom it holds succ(it,x) =
list_of_immediate_constituents(it.x);
end;
reserve t, t9, t99 for Element of dom tree_of_subformulae(F);
theorem :: QC_LANG4:5
F in rng tree_of_subformulae(F);
theorem :: QC_LANG4:6
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;
theorem :: QC_LANG4:7
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*>);
theorem :: QC_LANG4:8
G in rng tree_of_subformulae(F) & H is_immediate_constituent_of
G implies H in rng tree_of_subformulae(F);
theorem :: QC_LANG4:9
G in rng tree_of_subformulae(F) & H is_subformula_of G implies H
in rng tree_of_subformulae(F);
theorem :: QC_LANG4:10
G in rng tree_of_subformulae(F) iff G is_subformula_of F;
theorem :: QC_LANG4:11
rng tree_of_subformulae(F) = Subformulae(F);
theorem :: QC_LANG4:12
t9 in succ t implies (tree_of_subformulae(F)).t9
is_immediate_constituent_of (tree_of_subformulae(F)).t;
reserve x for set;
theorem :: QC_LANG4:13
t is_a_prefix_of t9 implies (tree_of_subformulae(F)).t9
is_subformula_of (tree_of_subformulae(F)).t;
theorem :: QC_LANG4:14
t is_a_proper_prefix_of t9 implies len @((tree_of_subformulae(F)
).t9) < len @((tree_of_subformulae(F)).t);
theorem :: QC_LANG4:15
t is_a_proper_prefix_of t9 implies (tree_of_subformulae(F)).t9
<> (tree_of_subformulae(F)).t;
theorem :: QC_LANG4:16
t is_a_proper_prefix_of t9 implies (tree_of_subformulae(F)).t9
is_proper_subformula_of (tree_of_subformulae(F)).t;
theorem :: QC_LANG4:17
(tree_of_subformulae(F)).t = F iff t = {};
theorem :: QC_LANG4:18
t <> t9 & (tree_of_subformulae(F)).t = (tree_of_subformulae(F)).
t9 implies not t,t9 are_c=-comparable;
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
:: QC_LANG4:def 3
for t being Element of dom
tree_of_subformulae(F) holds t in it iff (tree_of_subformulae(F)).t = G;
end;
theorem :: QC_LANG4:19
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 };
theorem :: QC_LANG4:20
G is_subformula_of F iff F-entry_points_in_subformula_tree_of G <> {};
theorem :: QC_LANG4:21
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
;
theorem :: QC_LANG4:22
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;
theorem :: QC_LANG4:23
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;
theorem :: QC_LANG4:24
(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;
reserve x,y for set;
theorem :: QC_LANG4:25
(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;
theorem :: QC_LANG4:26
(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;
reserve t for Element of dom tree_of_subformulae(F),
s for Element of dom tree_of_subformulae(G);
theorem :: QC_LANG4:27
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;
reserve t for Element of dom tree_of_subformulae(F),
s for FinSequence;
theorem :: QC_LANG4:28
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;
theorem :: QC_LANG4:29
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;
theorem :: QC_LANG4:30
(tree_of_subformulae(F))|t = tree_of_subformulae(( tree_of_subformulae(F)).t)
;
theorem :: QC_LANG4:31
t in F-entry_points_in_subformula_tree_of G iff (
tree_of_subformulae(F))|t = tree_of_subformulae(G);
theorem :: QC_LANG4:32
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) };
reserve C for Chain of dom tree_of_subformulae(F);
theorem :: QC_LANG4:33
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;
definition
let A;
let F be Element of QC-WFF(A);
mode Subformula of F -> Element of QC-WFF(A) means
:: QC_LANG4:def 4
it is_subformula_of F;
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
:: QC_LANG4:def 5
(tree_of_subformulae(F)).it = G;
end;
reserve G for Subformula of F;
reserve t, t9 for Entry_Point_in_Subformula_Tree of G;
theorem :: QC_LANG4:34
t <> t9 implies not t,t9 are_c=-comparable;
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
:: QC_LANG4:def 6
F-entry_points_in_subformula_tree_of G;
end;
theorem :: QC_LANG4:35
t in entry_points_in_subformula_tree(G);
theorem :: QC_LANG4:36
entry_points_in_subformula_tree(G) = { t where t is
Entry_Point_in_Subformula_Tree of G : t = t };
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 :: QC_LANG4:37
s in G1-entry_points_in_subformula_tree_of G2 implies t1^s is
Entry_Point_in_Subformula_Tree of G2;
reserve s for FinSequence;
theorem :: QC_LANG4:38
t1^s is Entry_Point_in_Subformula_Tree of G2 implies s in G1
-entry_points_in_subformula_tree_of G2;
theorem :: QC_LANG4:39
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 };
theorem :: QC_LANG4:40
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)
;
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 :: QC_LANG4:41
(ex t1,t2 st t1 is_a_prefix_of t2) implies G2 is_subformula_of G1;
theorem :: QC_LANG4:42
G2 is_subformula_of G1 implies for t1 ex t2 st t1 is_a_prefix_of t2;