:: The Subformula Tree of a Formula of the First Order Language :: by Oleg Okhotnikov :: :: Received October 2, 1995 :: Copyright (c) 1995-2021 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;