:: QC_LANG4 semantic presentation 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) proof let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A st F is_subformula_of G holds len (@ F) <= len (@ G) let F, G be Element of QC-WFF A; ::_thesis: ( F is_subformula_of G implies len (@ F) <= len (@ G) ) assume A1: F is_subformula_of G ; ::_thesis: len (@ F) <= len (@ G) percases ( F = G or F <> G ) ; suppose F = G ; ::_thesis: len (@ F) <= len (@ G) hence len (@ F) <= len (@ G) ; ::_thesis: verum end; suppose F <> G ; ::_thesis: len (@ F) <= len (@ G) then F is_proper_subformula_of G by A1, QC_LANG2:def_21; hence len (@ F) <= len (@ G) by QC_LANG2:54; ::_thesis: verum end; end; end; 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 proof let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A st F is_subformula_of G & len (@ F) = len (@ G) holds F = G let F, G be Element of QC-WFF A; ::_thesis: ( F is_subformula_of G & len (@ F) = len (@ G) implies F = G ) assume that A1: F is_subformula_of G and A2: len (@ F) = len (@ G) ; ::_thesis: F = G now__::_thesis:_not_F_<>_G assume F <> G ; ::_thesis: contradiction then F is_proper_subformula_of G by A1, QC_LANG2:def_21; hence contradiction by A2, QC_LANG2:54; ::_thesis: verum end; hence F = G ; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let k be Element of NAT ; ::_thesis: 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 let F, G be Element of QC-WFF A; ::_thesis: ( k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k implies G is_immediate_constituent_of F ) assume that A1: k in dom (list_of_immediate_constituents F) and A2: G = (list_of_immediate_constituents F) . k ; ::_thesis: G is_immediate_constituent_of F A3: list_of_immediate_constituents F <> <*> (QC-WFF A) by A1; A4: ( F <> VERUM A & not F is atomic ) by Def1, A3; percases ( F is negative or F is universal or F is conjunctive or F is universal ) by A4, QC_LANG1:9; supposeA5: F is negative ; ::_thesis: G is_immediate_constituent_of F 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, FINSEQ_1:def_8; hence G is_immediate_constituent_of F by A5, QC_LANG2:48; ::_thesis: verum end; supposeA7: F is universal ; ::_thesis: G is_immediate_constituent_of F 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, FINSEQ_1:def_8; hence G is_immediate_constituent_of F by A7, QC_LANG2:50; ::_thesis: verum end; supposeA10: F is conjunctive ; ::_thesis: G is_immediate_constituent_of F A11: <*(the_left_argument_of F),(the_right_argument_of F)*> . 2 = the_right_argument_of F by FINSEQ_1:44; A12: <*(the_left_argument_of F),(the_right_argument_of F)*> . 1 = the_left_argument_of F by FINSEQ_1:44; 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, FINSEQ_1:def_3; now__::_thesis:_G_is_immediate_constituent_of_F percases ( k = 1 or k = 2 ) by A14, TARSKI:def_2; suppose k = 1 ; ::_thesis: G is_immediate_constituent_of F hence G is_immediate_constituent_of F by A2, A10, A13, A12, QC_LANG2:49; ::_thesis: verum end; suppose k = 2 ; ::_thesis: G is_immediate_constituent_of F hence G is_immediate_constituent_of F by A2, A10, A13, A11, QC_LANG2:49; ::_thesis: verum end; end; end; hence G is_immediate_constituent_of F ; ::_thesis: verum end; supposeA15: F is universal ; ::_thesis: G is_immediate_constituent_of F 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, FINSEQ_1:def_8; hence G is_immediate_constituent_of F by A15, QC_LANG2:50; ::_thesis: verum end; end; end; 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 } proof let A be QC-alphabet ; ::_thesis: 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 } let F be Element of QC-WFF A; ::_thesis: rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } thus rng (list_of_immediate_constituents F) c= { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } :: according to XBOOLE_0:def_10 ::_thesis: { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } c= rng (list_of_immediate_constituents F) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (list_of_immediate_constituents F) or y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } ) assume A1: y in rng (list_of_immediate_constituents F) ; ::_thesis: y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of 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 set 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 y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } ; ::_thesis: verum end; thus { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } c= rng (list_of_immediate_constituents F) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } or x in rng (list_of_immediate_constituents F) ) assume x in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } ; ::_thesis: x in rng (list_of_immediate_constituents F) then consider G being Element of QC-WFF A such that A2: x = G and A3: G is_immediate_constituent_of F ; ex n being Element of NAT 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; percases ( F is negative or F is conjunctive or F is universal ) by A3, A4, QC_LANG1:9, QC_LANG2:47; suppose F is negative ; ::_thesis: ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) then A5: ( list_of_immediate_constituents F = <*(the_argument_of F)*> & G = the_argument_of F ) by A3, Def1, QC_LANG2:48; consider n being Element of NAT 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 ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A6, A5, FINSEQ_1:3; ::_thesis: verum end; supposeA7: F is conjunctive ; ::_thesis: ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) A8: <*(the_left_argument_of F),(the_right_argument_of F)*> . 2 = the_right_argument_of F by FINSEQ_1:44; 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 by FINSEQ_1:44; now__::_thesis:_ex_n_being_Element_of_NAT_st_ (_n_in_dom_(list_of_immediate_constituents_F)_&_G_=_(list_of_immediate_constituents_F)_._n_) percases ( G = the_left_argument_of F or G = the_right_argument_of F ) by A3, A7, QC_LANG2:49; supposeA12: G = the_left_argument_of F ; ::_thesis: ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) 1 in {1,2} by TARSKI:def_2; hence ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A10, A11, A9, A12, FINSEQ_1:2; ::_thesis: verum end; suppose G = the_right_argument_of F ; ::_thesis: ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) hence ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A10, A8, A9, FINSEQ_1:3; ::_thesis: verum end; end; end; hence ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) ; ::_thesis: verum end; supposeA13: F is universal ; ::_thesis: ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) 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 being Element of NAT 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 ex n being Element of NAT st ( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A15, A16, A17, FINSEQ_1:3; ::_thesis: verum end; end; end; hence x in rng (list_of_immediate_constituents F) by A2, FUNCT_1:def_3; ::_thesis: verum end; end; 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) ) ) proof deffunc H1( Element of QC-WFF A) -> Element of NAT = len (@ $1); deffunc H2( Element of QC-WFF A) -> FinSequence 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 for w being Element of QC-WFF A st w = W . x holds succ (W,x) = H2(w) ) ) from TREES_9:sch_2(); A2: for t, t9 being Element of dom W for d being Element of QC-WFF A st t9 in succ t & d = W . t9 holds H1(d) < H1(W . t) proof let t, t9 be Element of dom W; ::_thesis: for d being Element of QC-WFF A st t9 in succ t & d = W . t9 holds H1(d) < H1(W . t) let d be Element of QC-WFF A; ::_thesis: ( t9 in succ t & d = W . t9 implies H1(d) < H1(W . t) ) assume that A3: t9 in succ t and A4: d = W . t9 ; ::_thesis: H1(d) < H1(W . t) consider n being Element of NAT 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 H1(d) < H1(W . t) by A4, A6, Th3, QC_LANG2:51; ::_thesis: verum end; W is finite from TREES_9:sch_3(A2); then reconsider W = W as finite DecoratedTree of QC-WFF A ; take W ; ::_thesis: ( W . {} = p & ( for x being Element of dom W holds succ (W,x) = list_of_immediate_constituents (W . x) ) ) thus ( W . {} = p & ( for x being Element of dom W holds succ (W,x) = list_of_immediate_constituents (W . x) ) ) by A1; ::_thesis: verum end; 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 proof let t1, t2 be finite DecoratedTree of QC-WFF A; ::_thesis: ( 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) ) implies t1 = t2 ) 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; ::_thesis: ( 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) ) implies t1 c= t2 ) 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) ; ::_thesis: t1 c= t2 defpred S1[ set ] means ( $1 in dom t2 & t1 . $1 = t2 . $1 ); A12: for t being Element of dom t1 for n being Element of NAT st S1[t] & t ^ <*n*> in dom t1 holds S1[t ^ <*n*>] proof let t be Element of dom t1; ::_thesis: for n being Element of NAT st S1[t] & t ^ <*n*> in dom t1 holds S1[t ^ <*n*>] let n be Element of NAT ; ::_thesis: ( S1[t] & t ^ <*n*> in dom t1 implies S1[t ^ <*n*>] ) assume that A13: S1[t] and A14: t ^ <*n*> in dom t1 ; ::_thesis: S1[t ^ <*n*>] 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 ; ::_thesis: t1 . (t ^ <*n*>) = t2 . (t ^ <*n*>) thus t1 . (t ^ <*n*>) = (succ (t2,t9)) . (n + 1) by A14, A15, TREES_9:40 .= t2 . (t ^ <*n*>) by A16, TREES_9:40 ; ::_thesis: verum end; A17: S1[ {} ] by A8, A10, TREES_1:22; A18: for t being Element of dom t1 holds S1[t] from TREES_2:sch_1(A17, A12); then for t being set st t in dom t1 holds t in dom t2 ; then A19: dom t1 c= dom t2 by TARSKI:def_3; for x being set st x in dom t1 holds t1 . x = t2 . x by A18; hence t1 c= t2 by A19, GRFUNC_1:2; ::_thesis: verum 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) ) ) ; ::_thesis: t1 = t2 then ( t1 c= t2 & t2 c= t1 ) by A7; hence t1 = t2 by XBOOLE_0:def_10; ::_thesis: verum end; 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) proof let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds F in rng (tree_of_subformulae F) let F be Element of QC-WFF A; ::_thesis: F in rng (tree_of_subformulae F) ( (tree_of_subformulae F) . {} = F & {} in dom (tree_of_subformulae F) ) by Def2, TREES_1:22; hence F in rng (tree_of_subformulae F) by FUNCT_1:def_3; ::_thesis: verum end; 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 ) proof let A be QC-alphabet ; ::_thesis: 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 ) let n be Element of NAT ; ::_thesis: 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 ) let F be Element of QC-WFF A; ::_thesis: 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 ) let t be Element of dom (tree_of_subformulae F); ::_thesis: ( t ^ <*n*> in dom (tree_of_subformulae F) implies 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 ) ) A1: succ t = { (t ^ <*k*>) where k is Element of NAT : t ^ <*k*> in dom (tree_of_subformulae F) } ; assume t ^ <*n*> in dom (tree_of_subformulae F) ; ::_thesis: 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 ) then consider t9 being Element of dom (tree_of_subformulae F) 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 being Element of QC-WFF A such that A4: G = (tree_of_subformulae F) . t9 ; t9 in { (t ^ <*k*>) where k is Element of NAT : 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 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 ) by A2, A4, A3; ::_thesis: verum end; 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*>) ) ) proof let A be QC-alphabet ; ::_thesis: 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*>) ) ) let H, F be Element of QC-WFF A; ::_thesis: 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*>) ) ) let t be Element of dom (tree_of_subformulae F); ::_thesis: ( 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*>) ) ) now__::_thesis:_(_H_is_immediate_constituent_of_(tree_of_subformulae_F)_._t_implies_ex_n_being_Element_of_NAT_st_ (_t_^_<*n*>_in_dom_(tree_of_subformulae_F)_&_H_=_(tree_of_subformulae_F)_._(t_^_<*n*>)_)_) set G = (tree_of_subformulae F) . t; assume H is_immediate_constituent_of (tree_of_subformulae F) . t ; ::_thesis: ex n being Element of NAT st ( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) then H in { H1 where H1 is Element of QC-WFF A : H1 is_immediate_constituent_of (tree_of_subformulae F) . t } ; then A1: H in rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Th4; succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) by Def2; then consider t9 being Element of dom (tree_of_subformulae F) such that A2: H = (tree_of_subformulae F) . t9 and A3: t9 in succ t by A1, TREES_9:42; ex n being Element of NAT st ( t9 = t ^ <*n*> & t ^ <*n*> in dom (tree_of_subformulae F) ) by A3; hence ex n being Element of NAT st ( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) by A2; ::_thesis: verum end; hence ( H is_immediate_constituent_of (tree_of_subformulae F) . t implies ex n being Element of NAT st ( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) ) ; ::_thesis: ( ex n being Element of NAT st ( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) implies H is_immediate_constituent_of (tree_of_subformulae F) . t ) given n being Element of NAT such that A4: t ^ <*n*> in dom (tree_of_subformulae F) and A5: H = (tree_of_subformulae F) . (t ^ <*n*>) ; ::_thesis: H is_immediate_constituent_of (tree_of_subformulae F) . t 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 ) by A4, Th6; hence H is_immediate_constituent_of (tree_of_subformulae F) . t by A5; ::_thesis: verum end; 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) proof let A be QC-alphabet ; ::_thesis: 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) let G, F, H be Element of QC-WFF A; ::_thesis: ( G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G implies H in rng (tree_of_subformulae F) ) assume that A1: G in rng (tree_of_subformulae F) and A2: H is_immediate_constituent_of G ; ::_thesis: H in rng (tree_of_subformulae F) consider x being set 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 being Element of dom (tree_of_subformulae F) such that A5: t = x by A3; ex n being Element of NAT st ( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) by A2, A4, A5, Th7; hence H in rng (tree_of_subformulae F) by FUNCT_1:def_3; ::_thesis: verum end; 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) proof let A be QC-alphabet ; ::_thesis: 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) let G, F, H be Element of QC-WFF A; ::_thesis: ( G in rng (tree_of_subformulae F) & H is_subformula_of G implies H in rng (tree_of_subformulae F) ) assume that A1: G in rng (tree_of_subformulae F) and A2: H is_subformula_of G ; ::_thesis: H in rng (tree_of_subformulae F) consider n being Element of 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 Element of NAT st 1 <= k & k < n holds 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 S1[ Nat] means ex H9 being Element of QC-WFF A 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 & S1[k] holds ex m being Nat st ( m < k & S1[m] ) proof A9: Seg n = dom L by A4, FINSEQ_1:def_3; let k be Nat; ::_thesis: ( k <> 0 & S1[k] implies ex m being Nat st ( m < k & S1[m] ) ) assume that A10: k <> 0 and A11: S1[k] ; ::_thesis: ex m being Nat st ( m < k & S1[m] ) consider m being Nat such that A12: m + 1 = k by A10, NAT_1:6; 0 < k by A10, NAT_1:3; 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 ex m being Nat st ( m < k & S1[m] ) by A11, A12, A15, A16, Th8; ::_thesis: verum end; A17: ex k being Nat st S1[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 ex k being Nat st S1[k] by A1, A6, A18, FINSEQ_1:3; ::_thesis: verum end; S1[ 0 ] from NAT_1:sch_7(A17, A8); hence H in rng (tree_of_subformulae F) by A5; ::_thesis: verum end; 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 ) proof let A be QC-alphabet ; ::_thesis: for G, F being Element of QC-WFF A holds ( G in rng (tree_of_subformulae F) iff G is_subformula_of F ) let G, F be Element of QC-WFF A; ::_thesis: ( G in rng (tree_of_subformulae F) iff G is_subformula_of F ) now__::_thesis:_(_G_in_rng_(tree_of_subformulae_F)_implies_G_is_subformula_of_F_) set T = dom (tree_of_subformulae F); defpred S1[ set ] means ex H being Element of QC-WFF A st ( (tree_of_subformulae F) . $1 = H & H is_subformula_of F ); assume G in rng (tree_of_subformulae F) ; ::_thesis: G is_subformula_of F then consider t being set 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 = t as Element of dom (tree_of_subformulae F) by A1; A3: for t being Element of dom (tree_of_subformulae F) for n being Element of NAT st S1[t] & t ^ <*n*> in dom (tree_of_subformulae F) holds S1[t ^ <*n*>] proof let t be Element of dom (tree_of_subformulae F); ::_thesis: for n being Element of NAT st S1[t] & t ^ <*n*> in dom (tree_of_subformulae F) holds S1[t ^ <*n*>] let n be Element of NAT ; ::_thesis: ( S1[t] & t ^ <*n*> in dom (tree_of_subformulae F) implies S1[t ^ <*n*>] ) assume that A4: S1[t] and A5: t ^ <*n*> in dom (tree_of_subformulae F) ; ::_thesis: S1[t ^ <*n*>] (tree_of_subformulae F) . (t ^ <*n*>) is Element of QC-WFF A by A5, FUNCT_1:102; then consider H9 being Element of QC-WFF A such that A6: (tree_of_subformulae F) . (t ^ <*n*>) = H9 ; consider H being Element of QC-WFF A such that A7: (tree_of_subformulae F) . t = H and A8: H is_subformula_of F by A4; ex G9 being Element of QC-WFF A 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 S1[t ^ <*n*>] by A8, A6, QC_LANG2:57; ::_thesis: verum end; A9: S1[ {} ] proof take F ; ::_thesis: ( (tree_of_subformulae F) . {} = F & F is_subformula_of F ) thus ( (tree_of_subformulae F) . {} = F & F is_subformula_of F ) by Def2; ::_thesis: verum end; for t being Element of dom (tree_of_subformulae F) holds S1[t] from TREES_2:sch_1(A9, A3); then ex H being Element of QC-WFF A st ( (tree_of_subformulae F) . t = H & H is_subformula_of F ) ; hence G is_subformula_of F by A2; ::_thesis: verum end; hence ( G in rng (tree_of_subformulae F) implies G is_subformula_of F ) ; ::_thesis: ( G is_subformula_of F implies G in rng (tree_of_subformulae F) ) assume G is_subformula_of F ; ::_thesis: G in rng (tree_of_subformulae F) hence G in rng (tree_of_subformulae F) by Th5, Th9; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds rng (tree_of_subformulae F) = Subformulae F let F be Element of QC-WFF A; ::_thesis: rng (tree_of_subformulae F) = Subformulae F thus rng (tree_of_subformulae F) c= Subformulae F :: according to XBOOLE_0:def_10 ::_thesis: Subformulae F c= rng (tree_of_subformulae F) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (tree_of_subformulae F) or y in Subformulae F ) assume A1: y in rng (tree_of_subformulae F) ; ::_thesis: y in Subformulae F then y is Element of QC-WFF A by RELAT_1:167; then consider G being Element of QC-WFF A such that A2: G = y ; G is_subformula_of F by A1, A2, Th10; hence y in Subformulae F by A2, QC_LANG2:def_22; ::_thesis: verum end; thus Subformulae F c= rng (tree_of_subformulae F) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Subformulae F or y in rng (tree_of_subformulae F) ) assume y in Subformulae F ; ::_thesis: y in rng (tree_of_subformulae F) then ex G being Element of QC-WFF A st ( G = y & G is_subformula_of F ) by QC_LANG2:def_22; hence y in rng (tree_of_subformulae F) by Th10; ::_thesis: verum end; end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( t9 in succ t implies (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t ) assume t9 in succ t ; ::_thesis: (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t then ex n being Element of NAT st ( t9 = t ^ <*n*> & t ^ <*n*> in dom (tree_of_subformulae F) ) ; hence (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by Th7; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_prefix_of t9 implies (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t ) assume t is_a_prefix_of t9 ; ::_thesis: (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t then consider r being FinSequence such that A1: t9 = t ^ r by TREES_1:1; reconsider r = r as FinSequence of NAT by A1, FINSEQ_1:36; consider n being Element of NAT such that A2: n = len r ; defpred S1[ set , set ] means ex G being QC-formula of A ex m, k1 being Nat ex 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 being Nat st k in Seg (n + 1) holds ex x being set st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (n + 1) implies ex x being set st S1[k,x] ) assume k in Seg (n + 1) ; ::_thesis: ex x being set st S1[k,x] 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 = 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 t ^ r1 in dom (tree_of_subformulae F) by A1, A5, FINSEQ_6:13, TREES_1:20; ::_thesis: verum 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 ; ::_thesis: S1[k,G] take G ; ::_thesis: ex m, k1 being Nat ex r1 being FinSequence st ( G = G & m = k & m + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) take k ; ::_thesis: ex k1 being Nat ex r1 being FinSequence st ( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) take k1 ; ::_thesis: ex r1 being FinSequence st ( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) take r1 ; ::_thesis: ( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) thus ( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) by A4, A5, A6; ::_thesis: verum end; ex L being FinSequence st ( dom L = Seg (n + 1) & ( for k being Nat st k in Seg (n + 1) holds S1[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 being Nat st k in Seg (n + 1) holds ex G being QC-formula of A ex m, k1 being Nat ex 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 being Element of NAT st 1 <= k & k <= n + 1 holds ex G being QC-formula of A ex k1 being Nat ex 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 be Element of NAT ; ::_thesis: ( 1 <= k & k <= n + 1 implies ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st ( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) ) assume ( 1 <= k & k <= n + 1 ) ; ::_thesis: ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st ( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) then k in Seg (n + 1) by FINSEQ_1:1; then ex G being QC-formula of A ex m, k1 being Nat ex 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 ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st ( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) ; ::_thesis: verum end; A11: for k being Element of NAT st 1 <= k & k < n + 1 holds 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 be Element of NAT ; ::_thesis: ( 1 <= k & k < n + 1 implies ex H1, G1 being Element of QC-WFF A st ( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) ) assume that A12: 1 <= k and A13: k < n + 1 ; ::_thesis: ex H1, G1 being Element of QC-WFF A st ( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) 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 = k1, k2 = 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 t ^ r2 in dom (tree_of_subformulae F) by A1, A20, FINSEQ_6:13, TREES_1:20; ::_thesis: verum 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 t2 ^ <*m*> in dom (tree_of_subformulae F) by A1, A16, A23, FINSEQ_6:13, TREES_1:20; ::_thesis: verum end; then H1 is_immediate_constituent_of G1 by A17, A21, A23, Th7; hence ex H1, G1 being Element of QC-WFF A st ( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A14, A18; ::_thesis: verum end; 0 < n + 1 by NAT_1:3; then 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 L . (n + 1) = (tree_of_subformulae F) . t by A30, A32, FINSEQ_1:34; ::_thesis: verum end; dom r = Seg k1 by A2, A26, FINSEQ_1:def_3; then t9 = t ^ r1 by A1, A27, RELAT_1:69; hence (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t by A24, A9, A25, A28, A29, A11, QC_LANG2:def_20; ::_thesis: verum end; 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)) proof let A be QC-alphabet ; ::_thesis: 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)) let F be Element of QC-WFF A; ::_thesis: 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)) let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_proper_prefix_of t9 implies len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) ) set G = (tree_of_subformulae F) . t; set H = (tree_of_subformulae F) . t9; assume A1: t is_a_proper_prefix_of t9 ; ::_thesis: len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) then A2: t is_a_prefix_of t9 by XBOOLE_0:def_8; A3: now__::_thesis:_not_len_(@_((tree_of_subformulae_F)_._t9))_=_len_(@_((tree_of_subformulae_F)_._t)) consider r being FinSequence such that A4: t9 = t ^ r by A2, TREES_1:1; reconsider r = 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, XBOOLE_1:2; then A6: t1 is_a_proper_prefix_of r by XBOOLE_0:def_8; len t1 = 0 ; then 0 < len r by A6, TREES_1:6; then 0 + 1 <= len r by NAT_1:13; hence 1 <= len r ; ::_thesis: verum end; defpred S1[ set , set ] means ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st ( m = $1 & r1 = r | (Seg m) & t1 = t ^ r1 & $2 = (tree_of_subformulae F) . t1 ); A7: for k being Nat st k in Seg (len r) holds ex x being set st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len r) implies ex x being set st S1[k,x] ) assume A8: k in Seg (len r) ; ::_thesis: ex x being set st S1[k,x] r | (Seg k) is FinSequence by FINSEQ_1:15; then consider r1 being FinSequence such that A9: r1 = r | (Seg k) ; r1 is_a_prefix_of r by A8, A9, 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 A10: t1 = t ^ r1 ; ex x being set st x = (tree_of_subformulae F) . t1 ; hence ex x being set st S1[k,x] by A9, A10; ::_thesis: verum end; ex L being FinSequence st ( dom L = Seg (len r) & ( for k being Nat st k in Seg (len r) holds S1[k,L . k] ) ) from FINSEQ_1:sch_1(A7); then consider L being FinSequence such that dom L = Seg (len r) and A11: for k being Nat st k in Seg (len r) holds ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st ( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ; for k being Element of NAT st 1 <= k & k <= len r holds ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st ( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len r implies ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st ( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ) assume ( 1 <= k & k <= len r ) ; ::_thesis: ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st ( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) then k in Seg (len r) by FINSEQ_1:1; then ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st ( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) by A11; hence ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st ( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ; ::_thesis: verum end; then consider t1 being Element of dom (tree_of_subformulae F), r1 being FinSequence such that A12: r1 = r | (Seg 1) and A13: t1 = t ^ r1 and L . 1 = (tree_of_subformulae F) . t1 by A5; set H1 = (tree_of_subformulae F) . t1; A14: (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t proof ex m being Element of NAT st r1 = <*m*> by A5, A12, TREES_9:34; hence (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t by A13, Th7; ::_thesis: verum end; r1 is_a_prefix_of r by A12, TREES_1:def_1; then t1 is_a_prefix_of t9 by A4, A13, FINSEQ_6:13; then A15: len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t1)) by Th1, Th13; assume len (@ ((tree_of_subformulae F) . t9)) = len (@ ((tree_of_subformulae F) . t)) ; ::_thesis: contradiction hence contradiction by A15, A14, QC_LANG2:51; ::_thesis: verum end; len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t)) by A2, Th1, Th13; hence len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) by A3, XXREAL_0:1; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_proper_prefix_of t9 implies (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t ) set G = (tree_of_subformulae F) . t; set H = (tree_of_subformulae F) . t9; assume t is_a_proper_prefix_of t9 ; ::_thesis: (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t then len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) by Th14; hence (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t ; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_proper_prefix_of t9 implies (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t ) set G = (tree_of_subformulae F) . t; set H = (tree_of_subformulae F) . t9; assume A1: t is_a_proper_prefix_of t9 ; ::_thesis: (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t then t is_a_prefix_of t9 by XBOOLE_0:def_8; then A2: (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t by Th13; (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t by A1, Th15; hence (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t by A2, QC_LANG2:def_21; ::_thesis: verum end; 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 = {} ) proof let A be QC-alphabet ; ::_thesis: 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 = {} ) let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) holds ( (tree_of_subformulae F) . t = F iff t = {} ) let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (tree_of_subformulae F) . t = F iff t = {} ) now__::_thesis:_(_(tree_of_subformulae_F)_._t_=_F_implies_not_t_<>_{}_) reconsider t1 = {} as Element of dom (tree_of_subformulae F) by TREES_1:22; assume A1: (tree_of_subformulae F) . t = F ; ::_thesis: not t <> {} A2: t1 is_a_prefix_of t by XBOOLE_1:2; assume t <> {} ; ::_thesis: contradiction then t1 is_a_proper_prefix_of t by A2, XBOOLE_0:def_8; then (tree_of_subformulae F) . t is_proper_subformula_of (tree_of_subformulae F) . t1 by Th16; hence contradiction by A1, Def2; ::_thesis: verum end; hence ( (tree_of_subformulae F) . t = F implies t = {} ) ; ::_thesis: ( t = {} implies (tree_of_subformulae F) . t = F ) assume t = {} ; ::_thesis: (tree_of_subformulae F) . t = F hence (tree_of_subformulae F) . t = F by Def2; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 implies not t,t9 are_c=-comparable ) assume that A1: t <> t9 and A2: (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 ; ::_thesis: not t,t9 are_c=-comparable assume A3: t,t9 are_c=-comparable ; ::_thesis: contradiction percases ( t is_a_prefix_of t9 or t9 is_a_prefix_of t ) by A3, XBOOLE_0:def_9; suppose t is_a_prefix_of t9 ; ::_thesis: contradiction then t is_a_proper_prefix_of t9 by A1, XBOOLE_0:def_8; hence contradiction by A2, Th16; ::_thesis: verum end; suppose t9 is_a_prefix_of t ; ::_thesis: contradiction then t9 is_a_proper_prefix_of t by A1, XBOOLE_0:def_8; hence contradiction by A2, Th16; ::_thesis: verum end; end; end; 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 ) 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; ::_thesis: ( p1 in X & p2 in X & p1 <> p2 implies not p1,p2 are_c=-comparable ) assume that A4: ( p1 in X & p2 in X ) and A5: p1 <> p2 ; ::_thesis: not p1,p2 are_c=-comparable ( 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 not p1,p2 are_c=-comparable by A5, Th18; ::_thesis: verum end; for x being set st x in X holds x is FinSequence proof let x be set ; ::_thesis: ( x in X implies x is FinSequence ) assume x in X ; ::_thesis: x is FinSequence then ex t being Element of dom (tree_of_subformulae F) st ( t = x & (tree_of_subformulae F) . t = G ) by A1; hence x is FinSequence ; ::_thesis: verum end; then reconsider X = X as AntiChain_of_Prefixes by A3, TREES_1:def_10; X c= dom (tree_of_subformulae F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom (tree_of_subformulae F) ) assume x in X ; ::_thesis: x in dom (tree_of_subformulae F) then ex t being Element of dom (tree_of_subformulae F) st ( t = x & (tree_of_subformulae F) . t = G ) by A1; hence x in dom (tree_of_subformulae F) ; ::_thesis: verum end; hence X is AntiChain_of_Prefixes of dom (tree_of_subformulae F) by TREES_1:def_11; ::_thesis: verum 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); ::_thesis: ( t in X iff (tree_of_subformulae F) . t = G ) thus ( t in X iff (tree_of_subformulae F) . t = G ) ::_thesis: verum proof now__::_thesis:_(_t_in_X_implies_(tree_of_subformulae_F)_._t_=_G_) assume t in X ; ::_thesis: (tree_of_subformulae F) . t = G 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 ; ::_thesis: verum end; hence ( t in X implies (tree_of_subformulae F) . t = G ) ; ::_thesis: ( (tree_of_subformulae F) . t = G implies t in X ) assume (tree_of_subformulae F) . t = G ; ::_thesis: t in X hence t in X by A1; ::_thesis: verum end; end; hence 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 ) by A2; ::_thesis: verum end; 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 proof let P1, P2 be AntiChain_of_Prefixes of dom (tree_of_subformulae F); ::_thesis: ( ( for t being Element of dom (tree_of_subformulae F) holds ( t in P1 iff (tree_of_subformulae F) . t = G ) ) & ( for t being Element of dom (tree_of_subformulae F) holds ( t in P2 iff (tree_of_subformulae F) . t = G ) ) implies P1 = P2 ) assume A6: for t being Element of dom (tree_of_subformulae F) holds ( t in P1 iff (tree_of_subformulae F) . t = G ) ; ::_thesis: ( ex t being Element of dom (tree_of_subformulae F) st ( ( t in P2 implies (tree_of_subformulae F) . t = G ) implies ( (tree_of_subformulae F) . t = G & not t in P2 ) ) or P1 = P2 ) assume A7: for t being Element of dom (tree_of_subformulae F) holds ( t in P2 iff (tree_of_subformulae F) . t = G ) ; ::_thesis: P1 = P2 thus P1 c= P2 :: according to XBOOLE_0:def_10 ::_thesis: P2 c= P1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 or x in P2 ) assume A8: x in P1 ; ::_thesis: x in P2 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 x in P2 by A7; ::_thesis: verum end; thus P2 c= P1 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P2 or x in P1 ) assume A9: x in P2 ; ::_thesis: x in P1 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 x in P1 by A6; ::_thesis: verum end; end; 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 } proof let A be QC-alphabet ; ::_thesis: 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 } let F, G be Element of QC-WFF A; ::_thesis: 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 } 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 } :: according to XBOOLE_0:def_10 ::_thesis: { 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F -entry_points_in_subformula_tree_of G or x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ) assume A1: x in F -entry_points_in_subformula_tree_of G ; ::_thesis: x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = 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 x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ; ::_thesis: verum 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 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } or x in F -entry_points_in_subformula_tree_of G ) assume x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ; ::_thesis: x in F -entry_points_in_subformula_tree_of G then ex t9 being Element of dom (tree_of_subformulae F) st ( t9 = x & (tree_of_subformulae F) . t9 = G ) ; hence x in F -entry_points_in_subformula_tree_of G by Def3; ::_thesis: verum end; end; 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 <> {} ) proof let A be QC-alphabet ; ::_thesis: for G, F being Element of QC-WFF A holds ( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} ) let G, F be Element of QC-WFF A; ::_thesis: ( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} ) now__::_thesis:_(_G_is_subformula_of_F_implies_F_-entry_points_in_subformula_tree_of_G_<>_{}_) assume G is_subformula_of F ; ::_thesis: F -entry_points_in_subformula_tree_of G <> {} then G in rng (tree_of_subformulae F) by Th10; then ex x being set 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; ::_thesis: verum end; hence ( G is_subformula_of F implies F -entry_points_in_subformula_tree_of G <> {} ) ; ::_thesis: ( F -entry_points_in_subformula_tree_of G <> {} implies G is_subformula_of F ) assume F -entry_points_in_subformula_tree_of G <> {} ; ::_thesis: G is_subformula_of F then consider x being set 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 being Element of dom (tree_of_subformulae F) st ( x = t & (tree_of_subformulae F) . t = G ) ; then G in rng (tree_of_subformulae F) by FUNCT_1:def_3; hence G is_subformula_of F by Th10; ::_thesis: verum end; 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 ) proof let A be QC-alphabet ; ::_thesis: 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 ) let m be Element of NAT ; ::_thesis: 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 ) let F be Element of QC-WFF A; ::_thesis: 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 ) let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( 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 ) ) set G = (tree_of_subformulae F) . t; set H = (tree_of_subformulae F) . t9; assume that A1: t9 = t ^ <*m*> and A2: (tree_of_subformulae F) . t is negative ; ::_thesis: ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 ) A3: dom <*(the_argument_of ((tree_of_subformulae F) . t))*> = Seg 1 by FINSEQ_1:def_8; A4: ( succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) & 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 ((tree_of_subformulae F) . t) = <*(the_argument_of ((tree_of_subformulae F) . t))*> by A2, Def1; then dom <*(the_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A4, TREES_9:37; then m + 1 in dom <*(the_argument_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39; then A5: m + 1 = 0 + 1 by A3, FINSEQ_1:2, TARSKI:def_1; (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by A1, Th7; hence ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 ) by A2, A5, QC_LANG2:48; ::_thesis: verum end; 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 ) proof let A be QC-alphabet ; ::_thesis: 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 ) let m be Element of NAT ; ::_thesis: 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 ) let F be Element of QC-WFF A; ::_thesis: 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 ) let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( 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 ) implies ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) ) set G = (tree_of_subformulae F) . t; set H = (tree_of_subformulae F) . t9; assume that A1: t9 = t ^ <*m*> and A2: (tree_of_subformulae F) . t is conjunctive ; ::_thesis: ( ( (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 ) ) A3: list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A2, Def1; len <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = 2 by FINSEQ_1:44; then A4: dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = Seg 2 by FINSEQ_1:def_3; A5: succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) 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 ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A5, A3, TREES_9:37; then m + 1 in dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39; then A6: ( m + 1 = 0 + 1 or m + 1 = 1 + 1 ) by A4, FINSEQ_1:2, TARSKI:def_2; percases ( m = 0 or m = 1 ) by A6; supposeA7: m = 0 ; ::_thesis: ( ( (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 ) ) (tree_of_subformulae F) . t9 = (succ ((tree_of_subformulae F),t)) . (m + 1) by A1, TREES_9:40 .= the_left_argument_of ((tree_of_subformulae F) . t) by A5, A3, A7, FINSEQ_1:44 ; hence ( ( (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 ) ) by A7; ::_thesis: verum end; supposeA8: m = 1 ; ::_thesis: ( ( (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 ) ) (tree_of_subformulae F) . t9 = (succ ((tree_of_subformulae F),t)) . (m + 1) by A1, TREES_9:40 .= the_right_argument_of ((tree_of_subformulae F) . t) by A5, A3, A8, FINSEQ_1:44 ; hence ( ( (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 ) ) by A8; ::_thesis: verum end; end; end; 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 ) proof let A be QC-alphabet ; ::_thesis: 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 ) let m be Element of NAT ; ::_thesis: 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 ) let F be Element of QC-WFF A; ::_thesis: 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 ) let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( 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 ) ) set G = (tree_of_subformulae F) . t; set H = (tree_of_subformulae F) . t9; assume that A1: t9 = t ^ <*m*> and A2: (tree_of_subformulae F) . t is universal ; ::_thesis: ( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) A3: dom <*(the_scope_of ((tree_of_subformulae F) . t))*> = Seg 1 by FINSEQ_1:def_8; A4: ( succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) & 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; not VERUM A is universal by QC_LANG1:20; then A5: (tree_of_subformulae F) . t <> VERUM A by A2; ( not (tree_of_subformulae F) . t is atomic & not (tree_of_subformulae F) . t is negative & not (tree_of_subformulae F) . t is conjunctive ) by A2, QC_LANG1:20; then list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_scope_of ((tree_of_subformulae F) . t))*> by Def1, A5; then dom <*(the_scope_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A4, TREES_9:37; then m + 1 in dom <*(the_scope_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39; then A6: m + 1 = 0 + 1 by A3, FINSEQ_1:2, TARSKI:def_1; (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by A1, Th7; hence ( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) by A2, A6, QC_LANG2:50; ::_thesis: verum end; 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) ) proof let A be QC-alphabet ; ::_thesis: 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) ) let F be Element of QC-WFF A; ::_thesis: 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) ) let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (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) ) ) set G = (tree_of_subformulae F) . t; consider H being Element of QC-WFF A such that A1: H = the_argument_of ((tree_of_subformulae F) . t) ; assume A2: (tree_of_subformulae F) . t is negative ; ::_thesis: ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) ) then H is_immediate_constituent_of (tree_of_subformulae F) . t by A1, QC_LANG2:48; then consider m being Element of NAT 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 ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) ) by A2, A3, Th21; ::_thesis: verum end; Lm1: for x, y being set holds dom <*x,y*> = Seg 2 proof let x, y be set ; ::_thesis: dom <*x,y*> = Seg 2 thus dom <*x,y*> = Seg (len <*x,y*>) by FINSEQ_1:def_3 .= Seg 2 by FINSEQ_1:44 ; ::_thesis: verum end; 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) ) proof let A be QC-alphabet ; ::_thesis: 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) ) let F be Element of QC-WFF A; ::_thesis: 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) ) let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (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) ) ) set G = (tree_of_subformulae F) . t; assume A1: (tree_of_subformulae F) . t is conjunctive ; ::_thesis: ( 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) ) (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 (tree_of_subformulae F) * (t succ) = succ ((tree_of_subformulae F),t) ; ::_thesis: verum end; then A2: dom (t succ) = dom (succ ((tree_of_subformulae F),t)) by TREES_9:37 .= dom (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Def2 .= dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> 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 ((tree_of_subformulae F) . t)) . 1 by Def2 .= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 1 by A1, Def1 .= the_left_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:44 ; 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; ::_thesis: ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) ) 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 ((tree_of_subformulae F) . t)) . 2 by Def2 .= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 2 by A1, Def1 .= the_right_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:44 ; hence ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) ) by A2, A4, TREES_9:39; ::_thesis: verum end; 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) ) proof let A be QC-alphabet ; ::_thesis: 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) ) let F be Element of QC-WFF A; ::_thesis: 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) ) let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (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) ) ) set G = (tree_of_subformulae F) . t; consider H being Element of QC-WFF A such that A1: H = the_scope_of ((tree_of_subformulae F) . t) ; assume A2: (tree_of_subformulae F) . t is universal ; ::_thesis: ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) ) then H is_immediate_constituent_of (tree_of_subformulae F) . t by A1, QC_LANG2:50; then consider m being Element of NAT 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 ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) ) by A2, A3, Th23; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F, G, H be Element of QC-WFF A; ::_thesis: 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 let t be Element of dom (tree_of_subformulae F); ::_thesis: 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 let s be Element of dom (tree_of_subformulae G); ::_thesis: ( 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 ) defpred S1[ Element of NAT ] means 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 G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = $1 holds t ^ s in F -entry_points_in_subformula_tree_of H; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof A3: 1 in {1} by TARSKI:def_1; let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 holds t ^ s in F -entry_points_in_subformula_tree_of H let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 holds t ^ s in F -entry_points_in_subformula_tree_of H let s be Element of dom (tree_of_subformulae G); ::_thesis: ( G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 implies t ^ s in F -entry_points_in_subformula_tree_of H ) assume that A4: G = (tree_of_subformulae F) . t and A5: H = (tree_of_subformulae G) . s and A6: len s = k + 1 ; ::_thesis: t ^ s in F -entry_points_in_subformula_tree_of H 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 = 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 being Element of QC-WFF A 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__::_thesis:_(_H_=_(tree_of_subformulae_F)_._(t9_^_<*m*>)_&_t9_^_<*m*>_in_dom_(tree_of_subformulae_F)_) percases ( H9 is negative or H9 is conjunctive or H9 is universal ) by A15, A17, QC_LANG1:9, QC_LANG2:47; supposeA18: H9 is negative ; ::_thesis: ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) then ( H = the_argument_of H9 & m = 0 ) by A5, A14, A10, Th21; hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) by A13, A18, Th24; ::_thesis: verum end; supposeA19: H9 is conjunctive ; ::_thesis: ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) then ( ( H = the_left_argument_of H9 & m = 0 ) or ( H = the_right_argument_of H9 & m = 1 ) ) by A5, A14, A10, Th22; hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) by A13, A19, Th25; ::_thesis: verum end; supposeA20: H9 is universal ; ::_thesis: ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) then ( H = the_scope_of H9 & m = 0 ) by A5, A14, A10, Th23; hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) by A13, A20, Th26; ::_thesis: verum end; end; end; hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) ; ::_thesis: verum end; t ^ s = t9 ^ <*m*> by A7, A12, FINSEQ_1:32; hence t ^ s in F -entry_points_in_subformula_tree_of H by A16, Def3; ::_thesis: verum end; end; A21: S1[ 0 ] proof let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = 0 holds t ^ s in F -entry_points_in_subformula_tree_of H let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = 0 holds t ^ s in F -entry_points_in_subformula_tree_of H let s be Element of dom (tree_of_subformulae G); ::_thesis: ( G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = 0 implies t ^ s in F -entry_points_in_subformula_tree_of H ) assume that A22: G = (tree_of_subformulae F) . t and A23: H = (tree_of_subformulae G) . s and A24: len s = 0 ; ::_thesis: t ^ s in F -entry_points_in_subformula_tree_of H A25: s = {} by A24; then A26: t ^ s = t by FINSEQ_1:34; H = G by A23, A25, Def2; hence t ^ s in F -entry_points_in_subformula_tree_of H by A22, A26, Def3; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(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 ) ; ::_thesis: t ^ s in F -entry_points_in_subformula_tree_of H hence t ^ s in F -entry_points_in_subformula_tree_of H by A27, Def3; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F, G, H be Element of QC-WFF A; ::_thesis: 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 let t be Element of dom (tree_of_subformulae F); ::_thesis: 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 let s be FinSequence; ::_thesis: ( 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 ) defpred S1[ Element of NAT ] means 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 G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = $1 holds s in G -entry_points_in_subformula_tree_of H; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 holds s in G -entry_points_in_subformula_tree_of H let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 holds s in G -entry_points_in_subformula_tree_of H let s be FinSequence; ::_thesis: ( G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 implies s in G -entry_points_in_subformula_tree_of H ) 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 ; ::_thesis: s in G -entry_points_in_subformula_tree_of H 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 being Element of dom (tree_of_subformulae F) 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 = 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 = t9 as Element of dom (tree_of_subformulae F) by TREES_1:20; consider H9 being Element of QC-WFF A 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 = 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__::_thesis:_(_H_=_(tree_of_subformulae_G)_._(v_^_<*m*>)_&_v_^_<*m*>_in_dom_(tree_of_subformulae_G)_) percases ( H9 is negative or H9 is conjunctive or H9 is universal ) by A18, A19, QC_LANG1:9, QC_LANG2:47; supposeA20: H9 is negative ; ::_thesis: ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) then ( H = the_argument_of H9 & m = 0 ) by A9, A14, A15, Th21; hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) by A17, A20, Th24; ::_thesis: verum end; supposeA21: H9 is conjunctive ; ::_thesis: ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) then ( ( H = the_left_argument_of H9 & m = 0 ) or ( H = the_right_argument_of H9 & m = 1 ) ) by A9, A14, A15, Th22; hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) by A17, A21, Th25; ::_thesis: verum end; supposeA22: H9 is universal ; ::_thesis: ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) then ( H = the_scope_of H9 & m = 0 ) by A9, A14, A15, Th23; hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) by A17, A22, Th26; ::_thesis: verum end; end; end; hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) ; ::_thesis: verum end; hence s in G -entry_points_in_subformula_tree_of H by A6, Def3; ::_thesis: verum end; end; A23: S1[ 0 ] proof let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = 0 holds s in G -entry_points_in_subformula_tree_of H let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = 0 holds s in G -entry_points_in_subformula_tree_of H let s be FinSequence; ::_thesis: ( G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = 0 implies s in G -entry_points_in_subformula_tree_of H ) 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 ; ::_thesis: s in G -entry_points_in_subformula_tree_of H 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 being Element of dom (tree_of_subformulae F) st ( t9 = t ^ s & (tree_of_subformulae F) . t9 = H ) by A25; then H = G by A24, A27, FINSEQ_1:34; hence s in G -entry_points_in_subformula_tree_of H by A28, Def3; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(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 ) ; ::_thesis: s in G -entry_points_in_subformula_tree_of H hence s in G -entry_points_in_subformula_tree_of H by A29, Def3; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F, G, H be Element of QC-WFF A; ::_thesis: { (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 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 ) } or x in F -entry_points_in_subformula_tree_of H ) 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 ) } ; ::_thesis: x in F -entry_points_in_subformula_tree_of H then ex t being Element of dom (tree_of_subformulae F) ex 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 x in F -entry_points_in_subformula_tree_of H by Th27; ::_thesis: verum end; 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) proof let A be QC-alphabet ; ::_thesis: 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) let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t) let t be Element of dom (tree_of_subformulae F); ::_thesis: (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t) set T1 = (tree_of_subformulae F) | t; set T2 = tree_of_subformulae ((tree_of_subformulae F) . t); thus A1: dom ((tree_of_subformulae F) | t) = dom (tree_of_subformulae ((tree_of_subformulae F) . t)) :: according to TREES_4:def_1 ::_thesis: for b1 being Element of proj1 ((tree_of_subformulae F) | t) holds ((tree_of_subformulae F) | t) . b1 = (tree_of_subformulae ((tree_of_subformulae F) . t)) . b1 proof let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in dom ((tree_of_subformulae F) | t) or p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ) & ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) ) ) now__::_thesis:_(_p_in_dom_((tree_of_subformulae_F)_|_t)_implies_p_in_dom_(tree_of_subformulae_((tree_of_subformulae_F)_._t))_) consider G being Element of QC-WFF A 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 ((tree_of_subformulae F) | t) ; ::_thesis: p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) then p in (dom (tree_of_subformulae F)) | t by TREES_2:def_10; then reconsider t9 = t9 as Element of dom (tree_of_subformulae F) by A4, TREES_1:def_6; consider H being Element of QC-WFF A such that A5: H = (tree_of_subformulae F) . t9 ; A6: G -entry_points_in_subformula_tree_of H c= dom (tree_of_subformulae ((tree_of_subformulae F) . t)) 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 (tree_of_subformulae ((tree_of_subformulae F) . t)) by A6; ::_thesis: verum end; hence ( p in dom ((tree_of_subformulae F) | t) implies p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ) ; ::_thesis: ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) ) now__::_thesis:_(_p_in_dom_(tree_of_subformulae_((tree_of_subformulae_F)_._t))_implies_p_in_dom_((tree_of_subformulae_F)_|_t)_) consider G being Element of QC-WFF A such that A7: G = (tree_of_subformulae F) . t ; assume p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ; ::_thesis: p in dom ((tree_of_subformulae F) | t) then reconsider s = p as Element of dom (tree_of_subformulae G) by A7; consider H being Element of QC-WFF A 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 ((tree_of_subformulae F) | t) by TREES_2:def_10; ::_thesis: verum end; hence ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) ) ; ::_thesis: verum end; now__::_thesis:_for_p_being_Node_of_((tree_of_subformulae_F)_|_t)_holds_((tree_of_subformulae_F)_|_t)_._p_=_(tree_of_subformulae_((tree_of_subformulae_F)_._t))_._p let p be Node of ((tree_of_subformulae F) | t); ::_thesis: ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p consider G being Element of QC-WFF A 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 ((tree_of_subformulae F) | t) = (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 being Element of QC-WFF A such that A13: H = ((tree_of_subformulae F) | t) . p ; A14: t in F -entry_points_in_subformula_tree_of G by A11, Def3; ((tree_of_subformulae F) | t) . 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 ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p by A11, A13, Def3; ::_thesis: verum end; hence for p being Node of ((tree_of_subformulae F) | t) holds ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p ; ::_thesis: verum end; 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 ) proof let A be QC-alphabet ; ::_thesis: 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 ) let F, G be Element of QC-WFF A; ::_thesis: 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 ) let t be Element of dom (tree_of_subformulae F); ::_thesis: ( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G ) now__::_thesis:_(_t_in_F_-entry_points_in_subformula_tree_of_G_implies_(tree_of_subformulae_F)_|_t_=_tree_of_subformulae_G_) assume t in F -entry_points_in_subformula_tree_of G ; ::_thesis: (tree_of_subformulae F) | t = tree_of_subformulae G then (tree_of_subformulae F) . t = G by Def3; hence (tree_of_subformulae F) | t = tree_of_subformulae G by Th30; ::_thesis: verum end; hence ( t in F -entry_points_in_subformula_tree_of G implies (tree_of_subformulae F) | t = tree_of_subformulae G ) ; ::_thesis: ( (tree_of_subformulae F) | t = tree_of_subformulae G implies t in F -entry_points_in_subformula_tree_of G ) now__::_thesis:_(_(tree_of_subformulae_F)_|_t_=_tree_of_subformulae_G_implies_t_in_F_-entry_points_in_subformula_tree_of_G_) assume (tree_of_subformulae F) | t = tree_of_subformulae G ; ::_thesis: t in F -entry_points_in_subformula_tree_of 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; ::_thesis: verum end; hence ( (tree_of_subformulae F) | t = tree_of_subformulae G implies t in F -entry_points_in_subformula_tree_of G ) ; ::_thesis: verum end; 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 } proof let A be QC-alphabet ; ::_thesis: 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 } let F, G be Element of QC-WFF A; ::_thesis: 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 } 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 } :: according to XBOOLE_0:def_10 ::_thesis: { 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F -entry_points_in_subformula_tree_of G or x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } ) assume A1: x in F -entry_points_in_subformula_tree_of G ; ::_thesis: x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae 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 x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } ; ::_thesis: verum 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 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } or x in F -entry_points_in_subformula_tree_of G ) assume x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } ; ::_thesis: x in F -entry_points_in_subformula_tree_of G then ex t9 being Element of dom (tree_of_subformulae F) st ( t9 = x & (tree_of_subformulae F) | t9 = tree_of_subformulae G ) ; hence x in F -entry_points_in_subformula_tree_of G by Th31; ::_thesis: verum end; end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F, G, H be Element of QC-WFF A; ::_thesis: 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 let C be Chain of dom (tree_of_subformulae F); ::_thesis: ( 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 implies H is_subformula_of G ) 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 } ; ::_thesis: ( G is_subformula_of H or H is_subformula_of G ) consider t9 being Element of dom (tree_of_subformulae F) such that A3: G = (tree_of_subformulae F) . t9 and A4: t9 in C by A1; consider t99 being Element of dom (tree_of_subformulae F) 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; percases ( t9 is_a_prefix_of t99 or t99 is_a_prefix_of t9 ) by A7, XBOOLE_0:def_9; suppose t9 is_a_prefix_of t99 ; ::_thesis: ( G is_subformula_of H or H is_subformula_of G ) hence ( G is_subformula_of H or H is_subformula_of G ) by A3, A5, Th13; ::_thesis: verum end; suppose t99 is_a_prefix_of t9 ; ::_thesis: ( G is_subformula_of H or H is_subformula_of G ) hence ( G is_subformula_of H or H is_subformula_of G ) by A3, A5, Th13; ::_thesis: verum end; end; end; 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 proof G is_subformula_of F by Def4; then G in rng (tree_of_subformulae F) by Th10; then ex x being set st ( x in dom (tree_of_subformulae F) & (tree_of_subformulae F) . x = G ) by FUNCT_1:def_3; hence ex b1 being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . b1 = G ; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let G be Subformula of F; ::_thesis: for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds not t,t9 are_c=-comparable let t, t9 be Entry_Point_in_Subformula_Tree of G; ::_thesis: ( t <> t9 implies not t,t9 are_c=-comparable ) assume A1: t <> t9 ; ::_thesis: not t,t9 are_c=-comparable ( (tree_of_subformulae F) . t = G & (tree_of_subformulae F) . t9 = G ) by Def5; hence not t,t9 are_c=-comparable by A1, Th18; ::_thesis: verum end; 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) proof G is_subformula_of F by Def4; hence F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F) by Th20; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let G be Subformula of F; ::_thesis: for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G let t be Entry_Point_in_Subformula_Tree of G; ::_thesis: t in entry_points_in_subformula_tree G (tree_of_subformulae F) . t = G by Def5; hence t in entry_points_in_subformula_tree G by Def3; ::_thesis: verum end; 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 } proof let A be QC-alphabet ; ::_thesis: 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 } let F be Element of QC-WFF A; ::_thesis: 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 } let G be Subformula of F; ::_thesis: entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t } thus entry_points_in_subformula_tree G c= { t where t is Entry_Point_in_Subformula_Tree of G : t = t } :: according to XBOOLE_0:def_10 ::_thesis: { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c= entry_points_in_subformula_tree G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in entry_points_in_subformula_tree G or x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } ) assume x in entry_points_in_subformula_tree G ; ::_thesis: x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } 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 = t9 as Entry_Point_in_Subformula_Tree of G by A2, Def5; t9 = t9 ; hence x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } by A1; ::_thesis: verum end; thus { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c= entry_points_in_subformula_tree G ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } or x in entry_points_in_subformula_tree G ) assume x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } ; ::_thesis: x in entry_points_in_subformula_tree G then ex t being Entry_Point_in_Subformula_Tree of G st ( t = x & t = t ) ; hence x in entry_points_in_subformula_tree G by Th35; ::_thesis: verum end; end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let G1, G2 be Subformula of F; ::_thesis: 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 let t1 be Entry_Point_in_Subformula_Tree of G1; ::_thesis: 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 let s be Element of dom (tree_of_subformulae G1); ::_thesis: ( s in G1 -entry_points_in_subformula_tree_of G2 implies t1 ^ s is Entry_Point_in_Subformula_Tree of G2 ) (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 ; ::_thesis: t1 ^ s is Entry_Point_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 t1 ^ s is Entry_Point_in_Subformula_Tree of G2 by Def5; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let G2, G1 be Subformula of F; ::_thesis: 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 let t1 be Entry_Point_in_Subformula_Tree of G1; ::_thesis: 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 let s be FinSequence; ::_thesis: ( t1 ^ s is Entry_Point_in_Subformula_Tree of G2 implies s in G1 -entry_points_in_subformula_tree_of G2 ) 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 ; ::_thesis: s in G1 -entry_points_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 s in G1 -entry_points_in_subformula_tree_of G2 by A2, A1, Th28; ::_thesis: verum end; 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 ) } proof let A be QC-alphabet ; ::_thesis: 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 ) } let F be Element of QC-WFF A; ::_thesis: 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 ) } let G1, G2 be Subformula of F; ::_thesis: { (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 ) } 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 ) } :: according to XBOOLE_0:def_10 ::_thesis: { (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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 ) } ) 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 } ; ::_thesis: 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 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 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 ) } by A1; ::_thesis: verum 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 } ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 ) } or 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 } ) 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 ) } ; ::_thesis: 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 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 = t1 as Entry_Point_in_Subformula_Tree of G1 by Def5; x = t1 ^ s1 by A2; hence 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 } by A4; ::_thesis: verum end; end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let G1, G2 be Subformula of F; ::_thesis: { (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 { (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 { (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 by Th29; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let G1, G2 be Subformula of F; ::_thesis: ( 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 implies G2 is_subformula_of G1 ) given t1 being Entry_Point_in_Subformula_Tree of G1, t2 being Entry_Point_in_Subformula_Tree of G2 such that A1: t1 is_a_prefix_of t2 ; ::_thesis: G2 is_subformula_of G1 ( (tree_of_subformulae F) . t1 = G1 & (tree_of_subformulae F) . t2 = G2 ) by Def5; hence G2 is_subformula_of G1 by A1, Th13; ::_thesis: verum end; 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 proof let A be QC-alphabet ; ::_thesis: 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 let F be Element of QC-WFF A; ::_thesis: 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 let G2, G1 be Subformula of F; ::_thesis: ( G2 is_subformula_of G1 implies 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 ) assume A1: G2 is_subformula_of G1 ; ::_thesis: 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 now__::_thesis:_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 let t1 be Entry_Point_in_Subformula_Tree of G1; ::_thesis: ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 consider H being Element of QC-WFF A such that A2: H = G2 ; reconsider H = H as Subformula of G1 by A1, A2, Def4; set s = the Entry_Point_in_Subformula_Tree of H; (tree_of_subformulae G1) . the Entry_Point_in_Subformula_Tree of H = H by Def5; then the Entry_Point_in_Subformula_Tree of H in G1 -entry_points_in_subformula_tree_of G2 by A2, Def3; then t1 ^ the Entry_Point_in_Subformula_Tree of H is Entry_Point_in_Subformula_Tree of G2 by Th37; then consider t2 being Entry_Point_in_Subformula_Tree of G2 such that A3: t2 = t1 ^ the Entry_Point_in_Subformula_Tree of H ; take t2 = t2; ::_thesis: t1 is_a_prefix_of t2 thus t1 is_a_prefix_of t2 by A3, TREES_1:1; ::_thesis: verum end; hence 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 ; ::_thesis: verum end;