:: The Subformula Tree of a Formula of the First Order Language :: by Oleg Okhotnikov :: :: Received October 2, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users begin theorem Th1: :: QC_LANG4:1 for A being QC-alphabet for F, G being Element of QC-WFF A st F is_subformula_of G holds len (@ F) <= len (@ G) proofend; theorem :: QC_LANG4:2 for A being QC-alphabet for F, G being Element of QC-WFF A st F is_subformula_of G & len (@ F) = len (@ G) holds F = G proofend; definition let A be QC-alphabet ; let p be Element of QC-WFF A; func list_of_immediate_constituents p -> FinSequence of QC-WFF A equals :Def1: :: 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)*>; coherence ( ( ( p = VERUM A or p is atomic ) implies <*> (QC-WFF A) is FinSequence of QC-WFF A ) & ( p is negative implies <*(the_argument_of p)*> is FinSequence of QC-WFF A ) & ( p is conjunctive implies <*(the_left_argument_of p),(the_right_argument_of p)*> is FinSequence of QC-WFF A ) & ( p = VERUM A or p is atomic or p is negative or p is conjunctive or <*(the_scope_of p)*> is FinSequence of QC-WFF A ) ) ; consistency for b1 being FinSequence of QC-WFF A holds ( ( ( p = VERUM A or p is atomic ) & p is negative implies ( b1 = <*> (QC-WFF A) iff b1 = <*(the_argument_of p)*> ) ) & ( ( p = VERUM A or p is atomic ) & p is conjunctive implies ( b1 = <*> (QC-WFF A) iff b1 = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) & ( p is negative & p is conjunctive implies ( b1 = <*(the_argument_of p)*> iff b1 = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) ) by QC_LANG1:20; end; :: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def_1_:_ for A being QC-alphabet for p being Element of QC-WFF A holds ( ( ( p = VERUM A or p is atomic ) implies list_of_immediate_constituents p = <*> (QC-WFF A) ) & ( p is negative implies list_of_immediate_constituents p = <*(the_argument_of p)*> ) & ( p is conjunctive implies list_of_immediate_constituents p = <*(the_left_argument_of p),(the_right_argument_of p)*> ) & ( p = VERUM A or p is atomic or p is negative or p is conjunctive or list_of_immediate_constituents p = <*(the_scope_of p)*> ) ); theorem Th3: :: QC_LANG4:3 for A being QC-alphabet for k being Element of NAT for F, G being Element of QC-WFF A st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds G is_immediate_constituent_of F proofend; theorem Th4: :: QC_LANG4:4 for A being QC-alphabet for F being Element of QC-WFF A holds rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } proofend; definition let A be QC-alphabet ; let p be Element of QC-WFF A; func tree_of_subformulae p -> finite DecoratedTree of QC-WFF A means :Def2: :: QC_LANG4:def 2 ( it . {} = p & ( for x being Element of dom it holds succ (it,x) = list_of_immediate_constituents (it . x) ) ); existence ex b1 being finite DecoratedTree of QC-WFF A st ( b1 . {} = p & ( for x being Element of dom b1 holds succ (b1,x) = list_of_immediate_constituents (b1 . x) ) ) proofend; uniqueness for b1, b2 being finite DecoratedTree of QC-WFF A st b1 . {} = p & ( for x being Element of dom b1 holds succ (b1,x) = list_of_immediate_constituents (b1 . x) ) & b2 . {} = p & ( for x being Element of dom b2 holds succ (b2,x) = list_of_immediate_constituents (b2 . x) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def_2_:_ for A being QC-alphabet for p being Element of QC-WFF A for b3 being finite DecoratedTree of QC-WFF A holds ( b3 = tree_of_subformulae p iff ( b3 . {} = p & ( for x being Element of dom b3 holds succ (b3,x) = list_of_immediate_constituents (b3 . x) ) ) ); theorem Th5: :: QC_LANG4:5 for A being QC-alphabet for F being Element of QC-WFF A holds F in rng (tree_of_subformulae F) proofend; theorem Th6: :: QC_LANG4:6 for A being QC-alphabet for n being Element of NAT for F being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds ex G being Element of QC-WFF A st ( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) proofend; theorem Th7: :: QC_LANG4:7 for A being QC-alphabet for H, F being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) holds ( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Element of NAT st ( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) ) proofend; theorem Th8: :: QC_LANG4:8 for A being QC-alphabet for G, F, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G holds H in rng (tree_of_subformulae F) proofend; theorem Th9: :: QC_LANG4:9 for A being QC-alphabet for G, F, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_subformula_of G holds H in rng (tree_of_subformulae F) proofend; theorem Th10: :: QC_LANG4:10 for A being QC-alphabet for G, F being Element of QC-WFF A holds ( G in rng (tree_of_subformulae F) iff G is_subformula_of F ) proofend; theorem :: QC_LANG4:11 for A being QC-alphabet for F being Element of QC-WFF A holds rng (tree_of_subformulae F) = Subformulae F proofend; theorem :: QC_LANG4:12 for A being QC-alphabet for F being Element of QC-WFF A for t9, t being Element of dom (tree_of_subformulae F) st t9 in succ t holds (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t proofend; theorem Th13: :: QC_LANG4:13 for A being QC-alphabet for F being Element of QC-WFF A for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_prefix_of t9 holds (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t proofend; theorem Th14: :: QC_LANG4:14 for A being QC-alphabet for F being Element of QC-WFF A for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) proofend; theorem Th15: :: QC_LANG4:15 for A being QC-alphabet for F being Element of QC-WFF A for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t proofend; theorem Th16: :: QC_LANG4:16 for A being QC-alphabet for F being Element of QC-WFF A for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t proofend; theorem :: QC_LANG4:17 for A being QC-alphabet for F being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) holds ( (tree_of_subformulae F) . t = F iff t = {} ) proofend; theorem Th18: :: QC_LANG4:18 for A being QC-alphabet for F being Element of QC-WFF A for t, t9 being Element of dom (tree_of_subformulae F) st t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 holds not t,t9 are_c=-comparable proofend; definition let A be QC-alphabet ; let F, G be Element of QC-WFF A; funcF -entry_points_in_subformula_tree_of G -> AntiChain_of_Prefixes of dom (tree_of_subformulae F) means :Def3: :: 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 ); existence ex b1 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st for t being Element of dom (tree_of_subformulae F) holds ( t in b1 iff (tree_of_subformulae F) . t = G ) proofend; uniqueness for b1, b2 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st ( for t being Element of dom (tree_of_subformulae F) holds ( t in b1 iff (tree_of_subformulae F) . t = G ) ) & ( for t being Element of dom (tree_of_subformulae F) holds ( t in b2 iff (tree_of_subformulae F) . t = G ) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def_3_:_ for A being QC-alphabet for F, G being Element of QC-WFF A for b4 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) holds ( b4 = F -entry_points_in_subformula_tree_of G iff for t being Element of dom (tree_of_subformulae F) holds ( t in b4 iff (tree_of_subformulae F) . t = G ) ); theorem Th19: :: QC_LANG4:19 for A being QC-alphabet for F, G being Element of QC-WFF A holds 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 } proofend; theorem Th20: :: QC_LANG4:20 for A being QC-alphabet for G, F being Element of QC-WFF A holds ( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} ) proofend; theorem Th21: :: QC_LANG4:21 for A being QC-alphabet for m being Element of NAT for F being Element of QC-WFF A for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 ) proofend; theorem Th22: :: QC_LANG4:22 for A being QC-alphabet for m being Element of NAT for F being Element of QC-WFF A for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) proofend; theorem Th23: :: QC_LANG4:23 for A being QC-alphabet for m being Element of NAT for F being Element of QC-WFF A for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds ( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) proofend; theorem Th24: :: QC_LANG4:24 for A being QC-alphabet for F being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is negative holds ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) ) proofend; Lm1: for x, y being set holds dom <*x,y*> = Seg 2 proofend; theorem Th25: :: QC_LANG4:25 for A being QC-alphabet for F being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is conjunctive holds ( 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) ) proofend; theorem Th26: :: QC_LANG4:26 for A being QC-alphabet for F being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is universal holds ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) ) proofend; theorem Th27: :: QC_LANG4:27 for A being QC-alphabet for F, G, H being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds t ^ s in F -entry_points_in_subformula_tree_of H proofend; theorem Th28: :: QC_LANG4:28 for A being QC-alphabet for F, G, H being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) for s being FinSequence st t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H holds s in G -entry_points_in_subformula_tree_of H proofend; theorem Th29: :: QC_LANG4:29 for A being QC-alphabet for F, G, H being Element of QC-WFF A 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 proofend; theorem Th30: :: QC_LANG4:30 for A being QC-alphabet for F being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t) proofend; theorem Th31: :: QC_LANG4:31 for A being QC-alphabet for F, G being Element of QC-WFF A for t being Element of dom (tree_of_subformulae F) holds ( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G ) proofend; theorem :: QC_LANG4:32 for A being QC-alphabet for F, G being Element of QC-WFF A holds 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 } proofend; theorem :: QC_LANG4:33 for A being QC-alphabet for F, G, H being Element of QC-WFF A for C being Chain of dom (tree_of_subformulae F) 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 } & not G is_subformula_of H holds H is_subformula_of G proofend; definition let A be QC-alphabet ; let F be Element of QC-WFF A; mode Subformula of F -> Element of QC-WFF A means :Def4: :: QC_LANG4:def 4 it is_subformula_of F; existence ex b1 being Element of QC-WFF A st b1 is_subformula_of F ; end; :: deftheorem Def4 defines Subformula QC_LANG4:def_4_:_ for A being QC-alphabet for F, b3 being Element of QC-WFF A holds ( b3 is Subformula of F iff b3 is_subformula_of F ); definition let A be QC-alphabet ; 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: :: QC_LANG4:def 5 (tree_of_subformulae F) . it = G; existence ex b1 being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . b1 = G proofend; end; :: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def_5_:_ for A being QC-alphabet for F being Element of QC-WFF A for G being Subformula of F for b4 being Element of dom (tree_of_subformulae F) holds ( b4 is Entry_Point_in_Subformula_Tree of G iff (tree_of_subformulae F) . b4 = G ); theorem :: QC_LANG4:34 for A being QC-alphabet for F being Element of QC-WFF A for G being Subformula of F for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds not t,t9 are_c=-comparable proofend; definition let A be QC-alphabet ; 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; coherence F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F) proofend; end; :: deftheorem defines entry_points_in_subformula_tree QC_LANG4:def_6_:_ for A being QC-alphabet for F being Element of QC-WFF A for G being Subformula of F holds entry_points_in_subformula_tree G = F -entry_points_in_subformula_tree_of G; theorem Th35: :: QC_LANG4:35 for A being QC-alphabet for F being Element of QC-WFF A for G being Subformula of F for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G proofend; theorem Th36: :: QC_LANG4:36 for A being QC-alphabet for F being Element of QC-WFF A for G being Subformula of F holds entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t } proofend; theorem Th37: :: QC_LANG4:37 for A being QC-alphabet for F being Element of QC-WFF A for G1, G2 being Subformula of F for t1 being Entry_Point_in_Subformula_Tree of G1 for s being Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds t1 ^ s is Entry_Point_in_Subformula_Tree of G2 proofend; theorem :: QC_LANG4:38 for A being QC-alphabet for F being Element of QC-WFF A for G2, G1 being Subformula of F for t1 being Entry_Point_in_Subformula_Tree of G1 for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds s in G1 -entry_points_in_subformula_tree_of G2 proofend; theorem Th39: :: QC_LANG4:39 for A being QC-alphabet for F being Element of QC-WFF A for G1, G2 being Subformula of F 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 ) } proofend; theorem :: QC_LANG4:40 for A being QC-alphabet for F being Element of QC-WFF A for G1, G2 being Subformula of F 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 proofend; theorem :: QC_LANG4:41 for A being QC-alphabet for F being Element of QC-WFF A for G1, G2 being Subformula of F st ex t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 holds G2 is_subformula_of G1 proofend; theorem :: QC_LANG4:42 for A being QC-alphabet for F being Element of QC-WFF A for G2, G1 being Subformula of F st G2 is_subformula_of G1 holds for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 proofend;