qc_lang4.miz



    begin

    reserve A for QC-alphabet;

    reserve n,k,m for Nat;

    reserve F,G,G9,H,H9 for Element of ( QC-WFF A);

    theorem :: QC_LANG4:1

    

     Th1: F is_subformula_of G implies ( len ( @ F)) <= ( len ( @ G))

    proof

      assume

       A1: F is_subformula_of G;

      per cases ;

        suppose F = G;

        hence thesis;

      end;

        suppose F <> G;

        then F is_proper_subformula_of G by A1, QC_LANG2:def 21;

        hence thesis by QC_LANG2: 54;

      end;

    end;

    theorem :: QC_LANG4:2

    F is_subformula_of G & ( len ( @ F)) = ( len ( @ G)) implies F = G by QC_LANG2: 54, QC_LANG2:def 21;

    definition

      let A;

      let p be Element of ( QC-WFF A);

      :: QC_LANG4:def1

      func list_of_immediate_constituents (p) -> FinSequence of ( QC-WFF A) equals

      : Def1: ( <*> ( QC-WFF A)) if p = ( VERUM A) or p is atomic,

<*( the_argument_of p)*> if p is negative,

<*( the_left_argument_of p), ( the_right_argument_of p)*> if p is conjunctive

      otherwise <*( the_scope_of p)*>;

      coherence ;

      consistency by QC_LANG1: 20;

    end

    theorem :: QC_LANG4:3

    

     Th3: k in ( dom ( list_of_immediate_constituents F)) & G = (( list_of_immediate_constituents F) . k) implies G is_immediate_constituent_of F

    proof

      assume that

       A1: k in ( dom ( list_of_immediate_constituents F)) and

       A2: G = (( list_of_immediate_constituents F) . k);

      

       A3: ( list_of_immediate_constituents F) <> ( <*> ( QC-WFF A)) by A1;

      

       A4: F <> ( VERUM A) & not F is atomic by Def1, A3;

      per cases by A4, QC_LANG1: 9;

        suppose

         A5: F is negative;

        then

         A6: ( list_of_immediate_constituents F) = <*( the_argument_of F)*> by Def1;

        then k in ( Seg 1) by A1, FINSEQ_1:def 8;

        then k = 1 by FINSEQ_1: 2, TARSKI:def 1;

        then G = ( the_argument_of F) by A2, A6, FINSEQ_1:def 8;

        hence thesis by A5, QC_LANG2: 48;

      end;

        suppose

         A7: F is universal;

        then

         A8: not F is conjunctive by QC_LANG1: 20;

        ( not F is atomic) & not F is negative by A7, QC_LANG1: 20;

        then

         A9: ( list_of_immediate_constituents F) = <*( the_scope_of F)*> by A8, Def1, A4;

        then k in ( Seg 1) by A1, FINSEQ_1:def 8;

        then k = 1 by FINSEQ_1: 2, TARSKI:def 1;

        then G = ( the_scope_of F) by A2, A9, FINSEQ_1:def 8;

        hence thesis by A7, QC_LANG2: 50;

      end;

        suppose

         A10: F is conjunctive;

        

         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

          per cases by A14, TARSKI:def 2;

            suppose k = 1;

            hence thesis by A2, A10, A13, A12, QC_LANG2: 49;

          end;

            suppose k = 2;

            hence thesis by A2, A10, A13, A11, QC_LANG2: 49;

          end;

        end;

        hence thesis;

      end;

        suppose

         A15: F is universal;

        then

         A16: not F is conjunctive by QC_LANG1: 20;

        ( not F is atomic) & not F is negative by A15, QC_LANG1: 20;

        then

         A17: ( list_of_immediate_constituents F) = <*( the_scope_of F)*> by A16, Def1, A4;

        then k in ( Seg 1) by A1, FINSEQ_1:def 8;

        then k = 1 by FINSEQ_1: 2, TARSKI:def 1;

        then G = ( the_scope_of F) by A2, A17, FINSEQ_1:def 8;

        hence thesis by A15, QC_LANG2: 50;

      end;

    end;

    theorem :: QC_LANG4:4

    

     Th4: ( rng ( list_of_immediate_constituents F)) = { G where G be Element of ( QC-WFF A) : G is_immediate_constituent_of F }

    proof

      thus ( rng ( list_of_immediate_constituents F)) c= { G where G be Element of ( QC-WFF A) : G is_immediate_constituent_of F }

      proof

        let y be object;

        assume

         A1: y in ( rng ( list_of_immediate_constituents F));

        ( rng ( list_of_immediate_constituents F)) c= ( QC-WFF A) by FINSEQ_1:def 4;

        then

        reconsider G = y as Element of ( QC-WFF A) by A1;

        ex x be object st x in ( dom ( list_of_immediate_constituents F)) & y = (( list_of_immediate_constituents F) . x) by A1, FUNCT_1:def 3;

        then G is_immediate_constituent_of F by Th3;

        hence thesis;

      end;

      thus { G where G be Element of ( QC-WFF A) : G is_immediate_constituent_of F } c= ( rng ( list_of_immediate_constituents F))

      proof

        let x be object;

        assume x in { G where G be Element of ( QC-WFF A) : G is_immediate_constituent_of F };

        then

        consider G such that

         A2: x = G and

         A3: G is_immediate_constituent_of F;

        ex n st n in ( dom ( list_of_immediate_constituents F)) & G = (( list_of_immediate_constituents F) . n)

        proof

          

           A4: F <> ( VERUM A) by A3, QC_LANG2: 41;

          per cases by A3, A4, QC_LANG1: 9, QC_LANG2: 47;

            suppose F is negative;

            then

             A5: ( list_of_immediate_constituents F) = <*( the_argument_of F)*> & G = ( the_argument_of F) by A3, Def1, QC_LANG2: 48;

            consider n such that

             A6: n = 1;

            ( dom <*( the_argument_of F)*>) = ( Seg 1) & ( <*( the_argument_of F)*> . n) = ( the_argument_of F) by A6, FINSEQ_1:def 8;

            hence thesis by A6, A5, FINSEQ_1: 3;

          end;

            suppose

             A7: F is conjunctive;

            

             A8: ( <*( the_left_argument_of F), ( the_right_argument_of F)*> . 2) = ( the_right_argument_of F) 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

              per cases by A3, A7, QC_LANG2: 49;

                suppose

                 A12: G = ( the_left_argument_of F);

                1 in {1, 2} by TARSKI:def 2;

                hence thesis by A10, A11, A9, A12, FINSEQ_1: 2;

              end;

                suppose G = ( the_right_argument_of F);

                hence thesis by A10, A8, A9, FINSEQ_1: 3;

              end;

            end;

            hence thesis;

          end;

            suppose

             A13: F is universal;

            then

             A14: not F is conjunctive by QC_LANG1: 20;

            ( not F is atomic) & not F is negative by A13, QC_LANG1: 20;

            then

             A15: ( list_of_immediate_constituents F) = <*( the_scope_of F)*> by A14, Def1, A4;

            consider n such that

             A16: n = 1;

            

             A17: G = ( the_scope_of F) by A3, A13, QC_LANG2: 50;

            ( dom <*( the_scope_of F)*>) = ( Seg 1) & ( <*( the_scope_of F)*> . n) = ( the_scope_of F) by A16, FINSEQ_1:def 8;

            hence thesis by A15, A16, A17, FINSEQ_1: 3;

          end;

        end;

        hence thesis by A2, FUNCT_1:def 3;

      end;

    end;

    definition

      let A;

      let p be Element of ( QC-WFF A);

      :: QC_LANG4:def2

      func tree_of_subformulae (p) -> finite DecoratedTree of ( QC-WFF A) means

      : Def2: (it . {} ) = p & for x be Element of ( dom it ) holds ( succ (it ,x)) = ( list_of_immediate_constituents (it . x));

      existence

      proof

        deffunc F( Element of ( QC-WFF A)) = ( len ( @ $1));

        deffunc G( Element of ( QC-WFF A)) = ( list_of_immediate_constituents $1);

        consider W be finite-branching DecoratedTree of ( QC-WFF A) such that

         A1: (W . {} ) = p & for x be Element of ( dom W), w be Element of ( QC-WFF A) st w = (W . x) holds ( succ (W,x)) = G(w) from TREES_9:sch 2;

        

         A2: for t,t9 be Element of ( dom W), d be Element of ( QC-WFF A) st t9 in ( succ t) & d = (W . t9) holds F(d) < F(.)

        proof

          let t,t9 be Element of ( dom W), d be Element of ( QC-WFF A) such that

           A3: t9 in ( succ t) and

           A4: d = (W . t9);

          consider n such that

           A5: t9 = (t ^ <*n*>) and (t ^ <*n*>) in ( dom W) by A3;

          

           A6: (W . t9) = (( succ (W,t)) . (n + 1)) by A5, TREES_9: 40

          .= (( list_of_immediate_constituents (W . t)) . (n + 1)) by A1;

          ( dom ( list_of_immediate_constituents (W . t))) = ( dom ( succ (W,t))) by A1

          .= ( dom (t succ )) by TREES_9: 38;

          then (n + 1) in ( dom ( list_of_immediate_constituents (W . t))) by A5, TREES_9: 39;

          hence thesis by A4, A6, Th3, QC_LANG2: 51;

        end;

        W is finite from TREES_9:sch 3( A2);

        then

        reconsider W as finite DecoratedTree of ( QC-WFF A);

        take W;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let t1,t2 be finite DecoratedTree of ( QC-WFF A);

        

         A7: for t1,t2 be finite DecoratedTree of ( QC-WFF A) st ((t1 . {} ) = p & for x be Element of ( dom t1) holds ( succ (t1,x)) = ( list_of_immediate_constituents (t1 . x))) & ((t2 . {} ) = p & for x be Element of ( dom t2) holds ( succ (t2,x)) = ( list_of_immediate_constituents (t2 . x))) holds t1 c= t2

        proof

          let t1,t2 be finite DecoratedTree of ( QC-WFF A);

          assume that

           A8: (t1 . {} ) = p and

           A9: for x be Element of ( dom t1) holds ( succ (t1,x)) = ( list_of_immediate_constituents (t1 . x)) and

           A10: (t2 . {} ) = p and

           A11: for x be Element of ( dom t2) holds ( succ (t2,x)) = ( list_of_immediate_constituents (t2 . x));

          defpred P[ set] means $1 in ( dom t2) & (t1 . $1) = (t2 . $1);

          

           A12: for t be Element of ( dom t1), n st P[t] & (t ^ <*n*>) in ( dom t1) holds P[(t ^ <*n*>)]

          proof

            let t be Element of ( dom t1), n;

            assume that

             A13: P[t] and

             A14: (t ^ <*n*>) in ( dom t1);

            reconsider t9 = t as Element of ( dom t2) by A13;

            

             A15: ( succ (t1,t)) = ( list_of_immediate_constituents (t2 . t9)) by A9, A13

            .= ( succ (t2,t9)) by A11;

            (t ^ <*n*>) in ( succ t) by A14;

            then n < ( card ( succ t)) by TREES_9: 7;

            then n < ( len (t succ )) by TREES_9:def 5;

            then n < ( len ( succ (t1,t))) by TREES_9: 28;

            then n < ( len (t9 succ )) by A15, TREES_9: 28;

            then n < ( card ( succ t9)) by TREES_9:def 5;

            then

             A16: (t9 ^ <*n*>) in ( succ t9) by TREES_9: 7;

            hence (t ^ <*n*>) in ( dom t2);

            

            thus (t1 . (t ^ <*n*>)) = (( succ (t2,t9)) . (n + 1)) by A14, A15, TREES_9: 40

            .= (t2 . (t ^ <*n*>)) by A16, TREES_9: 40;

          end;

          

           A17: P[ {} ] by A8, A10, TREES_1: 22;

          

           A18: for t be Element of ( dom t1) holds P[t] from TREES_2:sch 1( A17, A12);

          then for t be object st t in ( dom t1) holds t in ( dom t2);

          then

           A19: ( dom t1) c= ( dom t2);

          for x be object st x in ( dom t1) holds (t1 . x) = (t2 . x) by A18;

          hence thesis by A19, GRFUNC_1: 2;

        end;

        assume ((t1 . {} ) = p & for x be Element of ( dom t1) holds ( succ (t1,x)) = ( list_of_immediate_constituents (t1 . x))) & ((t2 . {} ) = p & for x be Element of ( dom t2) holds ( succ (t2,x)) = ( list_of_immediate_constituents (t2 . x)));

        then t1 c= t2 & t2 c= t1 by A7;

        hence thesis;

      end;

    end

    reserve t,t9,t99 for Element of ( dom ( tree_of_subformulae F));

    theorem :: QC_LANG4:5

    

     Th5: F in ( rng ( tree_of_subformulae F))

    proof

      (( tree_of_subformulae F) . {} ) = F & {} in ( dom ( tree_of_subformulae F)) by Def2, TREES_1: 22;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: QC_LANG4:6

    

     Th6: (t ^ <*n*>) in ( dom ( tree_of_subformulae F)) implies ex G st G = (( tree_of_subformulae F) . (t ^ <*n*>)) & G is_immediate_constituent_of (( tree_of_subformulae F) . t)

    proof

      

       A1: ( succ t) = { (t ^ <*k*>) : (t ^ <*k*>) in ( dom ( tree_of_subformulae F)) };

      assume (t ^ <*n*>) in ( dom ( tree_of_subformulae F));

      then

      consider t9 such that

       A2: t9 = (t ^ <*n*>);

      

       A3: ( rng ( list_of_immediate_constituents (( tree_of_subformulae F) . t))) = { G1 where G1 be Element of ( QC-WFF A) : G1 is_immediate_constituent_of (( tree_of_subformulae F) . t) } by Th4;

      consider G such that

       A4: G = (( tree_of_subformulae F) . t9);

      t9 in { (t ^ <*k*>) : (t ^ <*k*>) in ( dom ( tree_of_subformulae F)) } by A2;

      then G in ( rng ( succ (( tree_of_subformulae F),t))) by A4, A1, TREES_9: 41;

      then G in ( rng ( list_of_immediate_constituents (( tree_of_subformulae F) . t))) by Def2;

      hence thesis by A2, A4, A3;

    end;

    theorem :: QC_LANG4:7

    

     Th7: H is_immediate_constituent_of (( tree_of_subformulae F) . t) iff ex n st (t ^ <*n*>) in ( dom ( tree_of_subformulae F)) & H = (( tree_of_subformulae F) . (t ^ <*n*>))

    proof

      now

        set G = (( tree_of_subformulae F) . t);

        assume H is_immediate_constituent_of (( tree_of_subformulae F) . t);

        then H in { H1 where H1 be Element of ( QC-WFF A) : H1 is_immediate_constituent_of G };

        then

         A1: H in ( rng ( list_of_immediate_constituents G)) by Th4;

        ( succ (( tree_of_subformulae F),t)) = ( list_of_immediate_constituents G) by Def2;

        then

        consider t9 such that

         A2: H = (( tree_of_subformulae F) . t9) and

         A3: t9 in ( succ t) by A1, TREES_9: 42;

        ex n st t9 = (t ^ <*n*>) & (t ^ <*n*>) in ( dom ( tree_of_subformulae F)) by A3;

        hence ex n st (t ^ <*n*>) in ( dom ( tree_of_subformulae F)) & H = (( tree_of_subformulae F) . (t ^ <*n*>)) by A2;

      end;

      hence H is_immediate_constituent_of (( tree_of_subformulae F) . t) implies ex n st (t ^ <*n*>) in ( dom ( tree_of_subformulae F)) & H = (( tree_of_subformulae F) . (t ^ <*n*>));

      given n such that

       A4: (t ^ <*n*>) in ( dom ( tree_of_subformulae F)) and

       A5: H = (( tree_of_subformulae F) . (t ^ <*n*>));

      ex G st G = (( tree_of_subformulae F) . (t ^ <*n*>)) & G is_immediate_constituent_of (( tree_of_subformulae F) . t) by A4, Th6;

      hence thesis by A5;

    end;

    theorem :: QC_LANG4:8

    

     Th8: G in ( rng ( tree_of_subformulae F)) & H is_immediate_constituent_of G implies H in ( rng ( tree_of_subformulae F))

    proof

      assume that

       A1: G in ( rng ( tree_of_subformulae F)) and

       A2: H is_immediate_constituent_of G;

      consider x be object such that

       A3: x in ( dom ( tree_of_subformulae F)) and

       A4: G = (( tree_of_subformulae F) . x) by A1, FUNCT_1:def 3;

      consider t such that

       A5: t = x by A3;

      ex n st (t ^ <*n*>) in ( dom ( tree_of_subformulae F)) & H = (( tree_of_subformulae F) . (t ^ <*n*>)) by A2, A4, A5, Th7;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: QC_LANG4:9

    

     Th9: G in ( rng ( tree_of_subformulae F)) & H is_subformula_of G implies H in ( rng ( tree_of_subformulae F))

    proof

      assume that

       A1: G in ( rng ( tree_of_subformulae F)) and

       A2: H is_subformula_of G;

      consider n be Nat, L be 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 be Nat st 1 <= k & k < n holds ex H1,G1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = G1 & H1 is_immediate_constituent_of G1 by A2, QC_LANG2:def 20;

      defpred P[ Nat] means ex H9 st H9 = (L . ($1 + 1)) & ($1 + 1) in ( dom L) & H9 in ( rng ( tree_of_subformulae F));

      

       A8: for k be Nat st k <> 0 & P[k] holds ex m be Nat st m < k & P[m]

      proof

        

         A9: ( Seg n) = ( dom L) by A4, FINSEQ_1:def 3;

        let k be Nat;

        assume that

         A10: k <> 0 and

         A11: P[k];

        consider m be Nat such that

         A12: (m + 1) = k by A10, NAT_1: 6;

         0 < k by A10;

        then

         A13: ( 0 + 1) <= k by NAT_1: 13;

        ( Seg ( len L)) = ( dom L) by FINSEQ_1:def 3;

        then

         A14: (k + 1) <= n by A4, A11, FINSEQ_1: 1;

        then k in NAT & k < n by NAT_1: 13, ORDINAL1:def 12;

        then

         A15: ex H1,G1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = G1 & H1 is_immediate_constituent_of G1 by A7, A13;

        k <= n by A14, NAT_1: 13;

        then

         A16: k in ( dom L) by A13, A9, FINSEQ_1: 1;

        m < k by A12, NAT_1: 13;

        hence thesis by A11, A12, A15, A16, Th8;

      end;

      

       A17: ex k be Nat st P[k]

      proof

         0 <> n by A3;

        then

         A18: ex k be Nat st (k + 1) = n by NAT_1: 6;

        ( Seg n) = ( dom L) by A4, FINSEQ_1:def 3;

        hence thesis by A1, A6, A18, FINSEQ_1: 3;

      end;

       P[ 0 ] from NAT_1:sch 7( A17, A8);

      hence thesis by A5;

    end;

    theorem :: QC_LANG4:10

    

     Th10: G in ( rng ( tree_of_subformulae F)) iff G is_subformula_of F

    proof

      now

        set T = ( dom ( tree_of_subformulae F));

        defpred P[ set] means ex H st (( tree_of_subformulae F) . $1) = H & H is_subformula_of F;

        assume G in ( rng ( tree_of_subformulae F));

        then

        consider t be object such that

         A1: t in ( dom ( tree_of_subformulae F)) and

         A2: (( tree_of_subformulae F) . t) = G by FUNCT_1:def 3;

        reconsider t as Element of T by A1;

        

         A3: for t be Element of T, n st P[t] & (t ^ <*n*>) in T holds P[(t ^ <*n*>)]

        proof

          let t be Element of T, n;

          assume that

           A4: P[t] and

           A5: (t ^ <*n*>) in T;

          (( tree_of_subformulae F) . (t ^ <*n*>)) is Element of ( QC-WFF A) by A5, FUNCT_1: 102;

          then

          consider H9 such that

           A6: (( tree_of_subformulae F) . (t ^ <*n*>)) = H9;

          consider H such that

           A7: (( tree_of_subformulae F) . t) = H and

           A8: H is_subformula_of F by A4;

          ex G9 st G9 = (( tree_of_subformulae F) . (t ^ <*n*>)) & G9 is_immediate_constituent_of (( tree_of_subformulae F) . t) by A5, Th6;

          then H9 is_subformula_of H by A7, A6, QC_LANG2: 52;

          hence thesis by A8, A6, QC_LANG2: 57;

        end;

        

         A9: P[ {} ] by Def2;

        for t be Element of T holds P[t] from TREES_2:sch 1( A9, A3);

        then ex H st (( tree_of_subformulae F) . t) = H & H is_subformula_of F;

        hence G is_subformula_of F by A2;

      end;

      hence G in ( rng ( tree_of_subformulae F)) implies G is_subformula_of F;

      assume G is_subformula_of F;

      hence thesis by Th5, Th9;

    end;

    theorem :: QC_LANG4:11

    ( rng ( tree_of_subformulae F)) = ( Subformulae F)

    proof

      thus ( rng ( tree_of_subformulae F)) c= ( Subformulae F)

      proof

        let y be object;

        assume

         A1: y in ( rng ( tree_of_subformulae F));

        then y is Element of ( QC-WFF A) by RELAT_1: 167;

        then

        consider G such that

         A2: G = y;

        G is_subformula_of F by A1, A2, Th10;

        hence thesis by A2, QC_LANG2:def 22;

      end;

      thus ( Subformulae F) c= ( rng ( tree_of_subformulae F))

      proof

        let y be object;

        assume y in ( Subformulae F);

        then ex G st G = y & G is_subformula_of F by QC_LANG2:def 22;

        hence thesis by Th10;

      end;

    end;

    theorem :: QC_LANG4:12

    t9 in ( succ t) implies (( tree_of_subformulae F) . t9) is_immediate_constituent_of (( tree_of_subformulae F) . t)

    proof

      assume t9 in ( succ t);

      then ex n st t9 = (t ^ <*n*>) & (t ^ <*n*>) in ( dom ( tree_of_subformulae F));

      hence thesis by Th7;

    end;

    reserve x for set;

    theorem :: QC_LANG4:13

    

     Th13: t is_a_prefix_of t9 implies (( tree_of_subformulae F) . t9) is_subformula_of (( tree_of_subformulae F) . t)

    proof

      assume t is_a_prefix_of t9;

      then

      consider r be FinSequence such that

       A1: t9 = (t ^ r) by TREES_1: 1;

      reconsider r as FinSequence of NAT by A1, FINSEQ_1: 36;

      consider n such that

       A2: n = ( len r);

      defpred P[ set, object] means ex G be QC-formula of A, m,k1 be Nat, r1 be FinSequence st G = $2 & m = $1 & (m + k1) = (n + 1) & r1 = (r | ( Seg k1)) & G = (( tree_of_subformulae F) . (t ^ r1));

      

       A3: for k be Nat st k in ( Seg (n + 1)) holds ex x be object st P[k, x]

      proof

        let k be Nat;

        assume k in ( Seg (n + 1));

        then k <= (n + 1) by FINSEQ_1: 1;

        then

        consider k1 be Nat such that

         A4: (k + k1) = (n + 1) by NAT_1: 10;

        reconsider k1 as Element of NAT by ORDINAL1:def 12;

        (r | ( Seg k1)) is FinSequence by FINSEQ_1: 15;

        then

        consider r1 be FinSequence such that

         A5: r1 = (r | ( Seg k1));

        (t ^ r1) in ( dom ( tree_of_subformulae F))

        proof

          ex q be FinSequence st q = (r | ( Seg k1)) & q is_a_prefix_of r by TREES_9: 32;

          hence thesis by A1, A5, FINSEQ_6: 13, TREES_1: 20;

        end;

        then

        reconsider t1 = (t ^ r1) as Element of ( dom ( tree_of_subformulae F));

        consider G be QC-formula of A such that

         A6: G = (( tree_of_subformulae F) . t1);

        take G, G, k, k1, r1;

        thus thesis by A4, A5, A6;

      end;

      ex L be FinSequence st ( dom L) = ( Seg (n + 1)) & for k be Nat st k in ( Seg (n + 1)) holds P[k, (L . k)] from FINSEQ_1:sch 1( A3);

      then

      consider L be FinSequence such that

       A7: ( dom L) = ( Seg (n + 1)) and

       A8: for k be Nat st k in ( Seg (n + 1)) holds ex G be QC-formula of A, m,k1 be Nat, r1 be FinSequence st G = (L . k) & m = k & (m + k1) = (n + 1) & r1 = (r | ( Seg k1)) & G = (( tree_of_subformulae F) . (t ^ r1));

      

       A9: ( len L) = (n + 1) by A7, FINSEQ_1:def 3;

      

       A10: for k st 1 <= k & k <= (n + 1) holds ex G be QC-formula of A, k1 be Nat, r1 be FinSequence st G = (L . k) & (k + k1) = (n + 1) & r1 = (r | ( Seg k1)) & G = (( tree_of_subformulae F) . (t ^ r1))

      proof

        let k;

        assume 1 <= k & k <= (n + 1);

        then k in ( Seg (n + 1)) by FINSEQ_1: 1;

        then ex G be QC-formula of A, m,k1 be Nat, r1 be FinSequence st G = (L . k) & m = k & (m + k1) = (n + 1) & r1 = (r | ( Seg k1)) & G = (( tree_of_subformulae F) . (t ^ r1)) by A8;

        hence thesis;

      end;

      

       A11: for k st 1 <= k & k < (n + 1) holds ex H1,G1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = G1 & H1 is_immediate_constituent_of G1

      proof

        let k;

        assume that

         A12: 1 <= k and

         A13: k < (n + 1);

        consider H1 be QC-formula of A, k1 be Nat, r1 be 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 be QC-formula of A, k2 be Nat, r2 be FinSequence such that

         A18: G1 = (L . (k + 1)) and

         A19: ((k + 1) + k2) = (n + 1) and

         A20: r2 = (r | ( Seg k2)) and

         A21: G1 = (( tree_of_subformulae F) . (t ^ r2)) by A10;

        reconsider k1, k2 as Element of NAT by ORDINAL1:def 12;

        (k1 + 1) <= (n + 1) by A12, A15, XREAL_1: 6;

        then (k2 + 1) <= ( len r) by A2, A15, A19, XREAL_1: 6;

        then

        consider m be 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 be FinSequence st q = (r | ( Seg k2)) & q is_a_prefix_of r by TREES_9: 32;

          hence thesis by A1, A20, FINSEQ_6: 13, TREES_1: 20;

        end;

        then

        reconsider t2 = (t ^ r2) as Element of ( dom ( tree_of_subformulae F));

        

         A23: (t2 ^ <*m*>) = (t ^ r1) by A22, FINSEQ_1: 32;

        (t2 ^ <*m*>) in ( dom ( tree_of_subformulae F))

        proof

          ex q be FinSequence st q = (r | ( Seg k1)) & q is_a_prefix_of r by TREES_9: 32;

          hence thesis by A1, A16, A23, FINSEQ_6: 13, TREES_1: 20;

        end;

        then H1 is_immediate_constituent_of G1 by A17, A21, A23, Th7;

        hence thesis by A14, A18;

      end;

      

       A24: ( 0 + 1) <= (n + 1) by NAT_1: 13;

      then

      consider G be QC-formula of A, k1 be Nat, r1 be 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 be QC-formula of A, k1 be Nat, r1 be FinSequence such that

         A30: G = (L . (n + 1)) and

         A31: ((n + 1) + k1) = (n + 1) & r1 = (r | ( Seg k1)) and

         A32: G = (( tree_of_subformulae F) . (t ^ r1)) by A24, A10;

        r1 = {} by A31;

        hence thesis by A30, A32, FINSEQ_1: 34;

      end;

      ( dom r) = ( Seg k1) by A2, A26, FINSEQ_1:def 3;

      then t9 = (t ^ r1) by A1, A27;

      hence thesis by A24, A9, A25, A28, A29, A11, QC_LANG2:def 20;

    end;

    theorem :: QC_LANG4:14

    

     Th14: t is_a_proper_prefix_of t9 implies ( len ( @ (( tree_of_subformulae F) . t9))) < ( len ( @ (( tree_of_subformulae F) . t)))

    proof

      set G = (( tree_of_subformulae F) . t);

      set H = (( tree_of_subformulae F) . t9);

      assume

       A1: t is_a_proper_prefix_of t9;

      then

       A2: t is_a_prefix_of t9;

       A3:

      now

        consider r be FinSequence such that

         A4: t9 = (t ^ r) by A2, TREES_1: 1;

        reconsider r as FinSequence of NAT by A4, FINSEQ_1: 36;

        

         A5: 1 <= ( len r)

        proof

          reconsider t1 = {} as Element of ( dom ( tree_of_subformulae F)) by TREES_1: 22;

          r <> {} & t1 is_a_prefix_of r by A1, A4, FINSEQ_1: 34;

          then

           A6: t1 is_a_proper_prefix_of r;

          ( len t1) = 0 ;

          then 0 < ( len r) by A6, TREES_1: 6;

          then ( 0 + 1) <= ( len r) by NAT_1: 13;

          hence thesis;

        end;

        defpred P[ set, object] means ex t1 be Element of ( dom ( tree_of_subformulae F)), r1 be FinSequence, m be Nat st m = $1 & r1 = (r | ( Seg m)) & t1 = (t ^ r1) & $2 = (( tree_of_subformulae F) . t1);

        

         A7: for k be Nat st k in ( Seg ( len r)) holds ex x be object st P[k, x]

        proof

          let k be Nat such that k in ( Seg ( len r));

          (r | ( Seg k)) is FinSequence by FINSEQ_1: 15;

          then

          consider r1 be FinSequence such that

           A8: r1 = (r | ( Seg k));

          r1 is_a_prefix_of r by A8, TREES_1:def 1;

          then (t ^ r1) in ( dom ( tree_of_subformulae F)) by A4, FINSEQ_6: 13, TREES_1: 20;

          then

          consider t1 be Element of ( dom ( tree_of_subformulae F)) such that

           A9: t1 = (t ^ r1);

          ex x st x = (( tree_of_subformulae F) . t1);

          hence thesis by A8, A9;

        end;

        ex L be FinSequence st ( dom L) = ( Seg ( len r)) & for k be Nat st k in ( Seg ( len r)) holds P[k, (L . k)] from FINSEQ_1:sch 1( A7);

        then

        consider L be FinSequence such that ( dom L) = ( Seg ( len r)) and

         A10: for k be Nat st k in ( Seg ( len r)) holds ex t1 be Element of ( dom ( tree_of_subformulae F)), r1 be FinSequence, m be Nat st m = k & r1 = (r | ( Seg m)) & t1 = (t ^ r1) & (L . k) = (( tree_of_subformulae F) . t1);

        for k st 1 <= k & k <= ( len r) holds ex t1 be Element of ( dom ( tree_of_subformulae F)), r1 be FinSequence st r1 = (r | ( Seg k)) & t1 = (t ^ r1) & (L . k) = (( tree_of_subformulae F) . t1)

        proof

          let k;

          assume 1 <= k & k <= ( len r);

          then k in ( Seg ( len r)) by FINSEQ_1: 1;

          then ex t1 be Element of ( dom ( tree_of_subformulae F)), r1 be FinSequence, m be Nat st m = k & r1 = (r | ( Seg m)) & t1 = (t ^ r1) & (L . k) = (( tree_of_subformulae F) . t1) by A10;

          hence thesis;

        end;

        then

        consider t1 be Element of ( dom ( tree_of_subformulae F)), r1 be FinSequence such that

         A11: r1 = (r | ( Seg 1)) and

         A12: t1 = (t ^ r1) and (L . 1) = (( tree_of_subformulae F) . t1) by A5;

        set H1 = (( tree_of_subformulae F) . t1);

        

         A13: H1 is_immediate_constituent_of G

        proof

          ex m be Element of NAT st r1 = <*m*> by A5, A11, TREES_9: 34;

          hence thesis by A12, Th7;

        end;

        r1 is_a_prefix_of r by A11, TREES_1:def 1;

        then t1 is_a_prefix_of t9 by A4, A12, FINSEQ_6: 13;

        then

         A14: ( len ( @ H)) <= ( len ( @ H1)) by Th1, Th13;

        assume ( len ( @ H)) = ( len ( @ G));

        hence contradiction by A14, A13, QC_LANG2: 51;

      end;

      ( len ( @ H)) <= ( len ( @ G)) by A2, Th1, Th13;

      hence thesis by A3, XXREAL_0: 1;

    end;

    theorem :: QC_LANG4:15

    

     Th15: t is_a_proper_prefix_of t9 implies (( tree_of_subformulae F) . t9) <> (( tree_of_subformulae F) . t)

    proof

      set G = (( tree_of_subformulae F) . t);

      set H = (( tree_of_subformulae F) . t9);

      assume t is_a_proper_prefix_of t9;

      then ( len ( @ H)) < ( len ( @ G)) by Th14;

      hence thesis;

    end;

    theorem :: QC_LANG4:16

    

     Th16: t is_a_proper_prefix_of t9 implies (( tree_of_subformulae F) . t9) is_proper_subformula_of (( tree_of_subformulae F) . t)

    proof

      set G = (( tree_of_subformulae F) . t);

      set H = (( tree_of_subformulae F) . t9);

      assume

       A1: t is_a_proper_prefix_of t9;

      then t is_a_prefix_of t9;

      then

       A2: H is_subformula_of G by Th13;

      H <> G by A1, Th15;

      hence thesis by A2, QC_LANG2:def 21;

    end;

    theorem :: QC_LANG4:17

    (( tree_of_subformulae F) . t) = F iff t = {}

    proof

      now

        reconsider t1 = {} as Element of ( dom ( tree_of_subformulae F)) by TREES_1: 22;

        assume

         A1: (( tree_of_subformulae F) . t) = F;

        

         A2: t1 is_a_prefix_of t;

        assume t <> {} ;

        then t1 is_a_proper_prefix_of t by A2;

        then (( tree_of_subformulae F) . t) is_proper_subformula_of (( tree_of_subformulae F) . t1) by Th16;

        hence contradiction by A1, Def2;

      end;

      hence (( tree_of_subformulae F) . t) = F implies t = {} ;

      assume t = {} ;

      hence thesis by Def2;

    end;

    theorem :: QC_LANG4:18

    

     Th18: t <> t9 & (( tree_of_subformulae F) . t) = (( tree_of_subformulae F) . t9) implies not (t,t9) are_c=-comparable

    proof

      assume that

       A1: t <> t9 and

       A2: (( tree_of_subformulae F) . t) = (( tree_of_subformulae F) . t9);

      assume

       A3: (t,t9) are_c=-comparable ;

      per cases by A3;

        suppose t is_a_prefix_of t9;

        then t is_a_proper_prefix_of t9 by A1;

        hence contradiction by A2, Th16;

      end;

        suppose t9 is_a_prefix_of t;

        then t9 is_a_proper_prefix_of t by A1;

        hence contradiction by A2, Th16;

      end;

    end;

    definition

      let A;

      let F,G be Element of ( QC-WFF A);

      :: QC_LANG4:def3

      func F -entry_points_in_subformula_tree_of G -> AntiChain_of_Prefixes of ( dom ( tree_of_subformulae F)) means

      : Def3: for t be Element of ( dom ( tree_of_subformulae F)) holds t in it iff (( tree_of_subformulae F) . t) = G;

      existence

      proof

        consider X be set such that

         A1: X = { t where t be 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 be FinSequence st p1 in X & p2 in X & p1 <> p2 holds not (p1,p2) are_c=-comparable

          proof

            let p1,p2 be FinSequence;

            assume that

             A4: p1 in X & p2 in X and

             A5: p1 <> p2;

            (ex t1 be Element of ( dom ( tree_of_subformulae F)) st t1 = p1 & (( tree_of_subformulae F) . t1) = G) & ex t2 be Element of ( dom ( tree_of_subformulae F)) st t2 = p2 & (( tree_of_subformulae F) . t2) = G by A1, A4;

            hence thesis by A5, Th18;

          end;

          for x be set st x in X holds x is FinSequence

          proof

            let x be set;

            assume x in X;

            then ex t be Element of ( dom ( tree_of_subformulae F)) st t = x & (( tree_of_subformulae F) . t) = G by A1;

            hence thesis;

          end;

          then

          reconsider X as AntiChain_of_Prefixes by A3, TREES_1:def 10;

          X c= ( dom ( tree_of_subformulae F))

          proof

            let x be object;

            assume x in X;

            then ex t be Element of ( dom ( tree_of_subformulae F)) st t = x & (( tree_of_subformulae F) . t) = G by A1;

            hence thesis;

          end;

          hence thesis by TREES_1:def 11;

        end;

        for t be Element of ( dom ( tree_of_subformulae F)) holds t in X iff (( tree_of_subformulae F) . t) = G

        proof

          let t be Element of ( dom ( tree_of_subformulae F));

          thus t in X iff (( tree_of_subformulae F) . t) = G

          proof

            now

              assume t in X;

              then ex t9 be Element of ( dom ( tree_of_subformulae F)) st t9 = t & (( tree_of_subformulae F) . t9) = G by A1;

              hence (( tree_of_subformulae F) . t) = G;

            end;

            hence t in X implies (( tree_of_subformulae F) . t) = G;

            assume (( tree_of_subformulae F) . t) = G;

            hence thesis by A1;

          end;

        end;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let P1,P2 be AntiChain_of_Prefixes of ( dom ( tree_of_subformulae F));

        assume

         A6: for t be Element of ( dom ( tree_of_subformulae F)) holds t in P1 iff (( tree_of_subformulae F) . t) = G;

        assume

         A7: for t be Element of ( dom ( tree_of_subformulae F)) holds t in P2 iff (( tree_of_subformulae F) . t) = G;

        thus P1 c= P2

        proof

          let x be object such that

           A8: x in P1;

          P1 c= ( dom ( tree_of_subformulae F)) by TREES_1:def 11;

          then

          reconsider t = x as Element of ( dom ( tree_of_subformulae F)) by A8;

          (( tree_of_subformulae F) . t) = G by A6, A8;

          hence thesis by A7;

        end;

        thus P2 c= P1

        proof

          let x be object such that

           A9: x in P2;

          P2 c= ( dom ( tree_of_subformulae F)) by TREES_1:def 11;

          then

          reconsider t = x as Element of ( dom ( tree_of_subformulae F)) by A9;

          (( tree_of_subformulae F) . t) = G by A7, A9;

          hence thesis by A6;

        end;

      end;

    end

    theorem :: QC_LANG4:19

    

     Th19: (F -entry_points_in_subformula_tree_of G) = { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t) = G }

    proof

      thus (F -entry_points_in_subformula_tree_of G) c= { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t) = G }

      proof

        let x be object;

        assume

         A1: x in (F -entry_points_in_subformula_tree_of G);

        (F -entry_points_in_subformula_tree_of G) c= ( dom ( tree_of_subformulae F)) by TREES_1:def 11;

        then

        reconsider t9 = x as Element of ( dom ( tree_of_subformulae F)) by A1;

        (( tree_of_subformulae F) . t9) = G by A1, Def3;

        hence thesis;

      end;

      thus { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t) = G } c= (F -entry_points_in_subformula_tree_of G)

      proof

        let x be object;

        assume x in { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t) = G };

        then ex t9 st t9 = x & (( tree_of_subformulae F) . t9) = G;

        hence thesis by Def3;

      end;

    end;

    theorem :: QC_LANG4:20

    

     Th20: G is_subformula_of F iff (F -entry_points_in_subformula_tree_of G) <> {}

    proof

      now

        assume G is_subformula_of F;

        then G in ( rng ( tree_of_subformulae F)) by Th10;

        then ex x be object st x in ( dom ( tree_of_subformulae F)) & G = (( tree_of_subformulae F) . x) by FUNCT_1:def 3;

        hence (F -entry_points_in_subformula_tree_of G) <> {} by Def3;

      end;

      hence G is_subformula_of F implies (F -entry_points_in_subformula_tree_of G) <> {} ;

      assume (F -entry_points_in_subformula_tree_of G) <> {} ;

      then

      consider x be object such that

       A1: x in (F -entry_points_in_subformula_tree_of G) by XBOOLE_0:def 1;

      x in { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t) = G } by A1, Th19;

      then ex t st x = t & (( tree_of_subformulae F) . t) = G;

      then G in ( rng ( tree_of_subformulae F)) by FUNCT_1:def 3;

      hence thesis by Th10;

    end;

    theorem :: QC_LANG4:21

    

     Th21: t9 = (t ^ <*m*>) & (( tree_of_subformulae F) . t) is negative implies (( tree_of_subformulae F) . t9) = ( the_argument_of (( tree_of_subformulae F) . t)) & m = 0

    proof

      set G = (( tree_of_subformulae F) . t);

      set H = (( tree_of_subformulae F) . t9);

      assume that

       A1: t9 = (t ^ <*m*>) and

       A2: G is negative;

      

       A3: ( dom <*( the_argument_of G)*>) = ( Seg 1) by FINSEQ_1:def 8;

      

       A4: ( succ (( tree_of_subformulae F),t)) = ( list_of_immediate_constituents G) & ex q be Element of ( dom ( tree_of_subformulae F)) st q = t & ( succ (( tree_of_subformulae F),t)) = (( tree_of_subformulae F) * (q succ )) by Def2, TREES_9:def 6;

      ( list_of_immediate_constituents G) = <*( the_argument_of G)*> by A2, Def1;

      then ( dom <*( the_argument_of G)*>) = ( dom (t succ )) by A4, TREES_9: 37;

      then (m + 1) in ( dom <*( the_argument_of G)*>) by A1, TREES_9: 39;

      then

       A5: (m + 1) = ( 0 + 1) by A3, FINSEQ_1: 2, TARSKI:def 1;

      H is_immediate_constituent_of G by A1, Th7;

      hence thesis by A2, A5, QC_LANG2: 48;

    end;

    theorem :: QC_LANG4:22

    

     Th22: t9 = (t ^ <*m*>) & (( tree_of_subformulae F) . t) is conjunctive implies (( tree_of_subformulae F) . t9) = ( the_left_argument_of (( tree_of_subformulae F) . t)) & m = 0 or (( tree_of_subformulae F) . t9) = ( the_right_argument_of (( tree_of_subformulae F) . t)) & m = 1

    proof

      set G = (( tree_of_subformulae F) . t);

      set H = (( tree_of_subformulae F) . t9);

      assume that

       A1: t9 = (t ^ <*m*>) and

       A2: G is conjunctive;

      

       A3: ( list_of_immediate_constituents G) = <*( the_left_argument_of G), ( the_right_argument_of G)*> by A2, Def1;

      ( len <*( the_left_argument_of G), ( the_right_argument_of G)*>) = 2 by FINSEQ_1: 44;

      then

       A4: ( dom <*( the_left_argument_of G), ( the_right_argument_of G)*>) = ( Seg 2) by FINSEQ_1:def 3;

      

       A5: ( succ (( tree_of_subformulae F),t)) = ( list_of_immediate_constituents G) by Def2;

      ex q be Element of ( dom ( tree_of_subformulae F)) st q = t & ( succ (( tree_of_subformulae F),t)) = (( tree_of_subformulae F) * (q succ )) by TREES_9:def 6;

      then ( dom <*( the_left_argument_of G), ( the_right_argument_of G)*>) = ( dom (t succ )) by A5, A3, TREES_9: 37;

      then (m + 1) in ( dom <*( the_left_argument_of G), ( the_right_argument_of G)*>) by A1, TREES_9: 39;

      then

       A6: (m + 1) = ( 0 + 1) or (m + 1) = (1 + 1) by A4, FINSEQ_1: 2, TARSKI:def 2;

      per cases by A6;

        suppose

         A7: m = 0 ;

        H = (( succ (( tree_of_subformulae F),t)) . (m + 1)) by A1, TREES_9: 40

        .= ( the_left_argument_of G) by A5, A3, A7, FINSEQ_1: 44;

        hence thesis by A7;

      end;

        suppose

         A8: m = 1;

        H = (( succ (( tree_of_subformulae F),t)) . (m + 1)) by A1, TREES_9: 40

        .= ( the_right_argument_of G) by A5, A3, A8, FINSEQ_1: 44;

        hence thesis by A8;

      end;

    end;

    theorem :: QC_LANG4:23

    

     Th23: t9 = (t ^ <*m*>) & (( tree_of_subformulae F) . t) is universal implies (( tree_of_subformulae F) . t9) = ( the_scope_of (( tree_of_subformulae F) . t)) & m = 0

    proof

      set G = (( tree_of_subformulae F) . t);

      set H = (( tree_of_subformulae F) . t9);

      assume that

       A1: t9 = (t ^ <*m*>) and

       A2: G is universal;

      

       A3: ( dom <*( the_scope_of G)*>) = ( Seg 1) by FINSEQ_1:def 8;

      

       A4: ( succ (( tree_of_subformulae F),t)) = ( list_of_immediate_constituents G) & ex q be 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: G <> ( VERUM A) by A2;

      G is non atomic non negative non conjunctive by A2, QC_LANG1: 20;

      then ( list_of_immediate_constituents G) = <*( the_scope_of G)*> by Def1, A5;

      then ( dom <*( the_scope_of G)*>) = ( dom (t succ )) by A4, TREES_9: 37;

      then (m + 1) in ( dom <*( the_scope_of G)*>) by A1, TREES_9: 39;

      then

       A6: (m + 1) = ( 0 + 1) by A3, FINSEQ_1: 2, TARSKI:def 1;

      H is_immediate_constituent_of G by A1, Th7;

      hence thesis by A2, A6, QC_LANG2: 50;

    end;

    theorem :: QC_LANG4:24

    

     Th24: (( tree_of_subformulae F) . t) is negative implies (t ^ <* 0 *>) in ( dom ( tree_of_subformulae F)) & (( tree_of_subformulae F) . (t ^ <* 0 *>)) = ( the_argument_of (( tree_of_subformulae F) . t))

    proof

      set G = (( tree_of_subformulae F) . t);

      consider H such that

       A1: H = ( the_argument_of G);

      assume

       A2: G is negative;

      then H is_immediate_constituent_of G by A1, QC_LANG2: 48;

      then

      consider m such that

       A3: (t ^ <*m*>) in ( dom ( tree_of_subformulae F)) and H = (( tree_of_subformulae F) . (t ^ <*m*>)) by Th7;

      m = 0 by A2, A3, Th21;

      hence thesis by A2, A3, Th21;

    end;

    reserve x,y for set;

    

     Lm1: ( dom <*x, y*>) = ( Seg 2)

    proof

      

      thus ( dom <*x, y*>) = ( Seg ( len <*x, y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

    end;

    theorem :: QC_LANG4:25

    

     Th25: (( tree_of_subformulae F) . t) is conjunctive implies (t ^ <* 0 *>) in ( dom ( tree_of_subformulae F)) & (( tree_of_subformulae F) . (t ^ <* 0 *>)) = ( the_left_argument_of (( tree_of_subformulae F) . t)) & (t ^ <*1*>) in ( dom ( tree_of_subformulae F)) & (( tree_of_subformulae F) . (t ^ <*1*>)) = ( the_right_argument_of (( tree_of_subformulae F) . t))

    proof

      set G = (( tree_of_subformulae F) . t);

      assume

       A1: G is conjunctive;

      (( tree_of_subformulae F) * (t succ )) = ( succ (( tree_of_subformulae F),t))

      proof

        ex q be Element of ( dom ( tree_of_subformulae F)) st q = t & ( succ (( tree_of_subformulae F),t)) = (( tree_of_subformulae F) * (q succ )) by TREES_9:def 6;

        hence thesis;

      end;

      

      then

       A2: ( dom (t succ )) = ( dom ( succ (( tree_of_subformulae F),t))) by TREES_9: 37

      .= ( dom ( list_of_immediate_constituents G)) by Def2

      .= ( dom <*( the_left_argument_of G), ( the_right_argument_of G)*>) by A1, Def1

      .= {1, 2} by Lm1, FINSEQ_1: 2;

      

       A3: ( 0 + 1) in {1, 2} by TARSKI:def 2;

      then (t ^ <* 0 *>) in ( dom ( tree_of_subformulae F)) by A2, TREES_9: 39;

      

      then (( tree_of_subformulae F) . (t ^ <* 0 *>)) = (( succ (( tree_of_subformulae F),t)) . ( 0 + 1)) by TREES_9: 40

      .= (( list_of_immediate_constituents G) . 1) by Def2

      .= ( <*( the_left_argument_of G), ( the_right_argument_of G)*> . 1) by A1, Def1

      .= ( the_left_argument_of G) 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;

      

       A4: (1 + 1) in {1, 2} by TARSKI:def 2;

      then (t ^ <*1*>) in ( dom ( tree_of_subformulae F)) by A2, TREES_9: 39;

      

      then (( tree_of_subformulae F) . (t ^ <*1*>)) = (( succ (( tree_of_subformulae F),t)) . (1 + 1)) by TREES_9: 40

      .= (( list_of_immediate_constituents G) . 2) by Def2

      .= ( <*( the_left_argument_of G), ( the_right_argument_of G)*> . 2) by A1, Def1

      .= ( the_right_argument_of G) by FINSEQ_1: 44;

      hence thesis by A2, A4, TREES_9: 39;

    end;

    theorem :: QC_LANG4:26

    

     Th26: (( tree_of_subformulae F) . t) is universal implies (t ^ <* 0 *>) in ( dom ( tree_of_subformulae F)) & (( tree_of_subformulae F) . (t ^ <* 0 *>)) = ( the_scope_of (( tree_of_subformulae F) . t))

    proof

      set G = (( tree_of_subformulae F) . t);

      consider H such that

       A1: H = ( the_scope_of G);

      assume

       A2: G is universal;

      then H is_immediate_constituent_of G by A1, QC_LANG2: 50;

      then

      consider m such that

       A3: (t ^ <*m*>) in ( dom ( tree_of_subformulae F)) and H = (( tree_of_subformulae F) . (t ^ <*m*>)) by Th7;

      m = 0 by A2, A3, Th23;

      hence thesis by A2, A3, Th23;

    end;

    reserve t for Element of ( dom ( tree_of_subformulae F)),

s for Element of ( dom ( tree_of_subformulae G));

    theorem :: QC_LANG4:27

    

     Th27: t in (F -entry_points_in_subformula_tree_of G) & s in (G -entry_points_in_subformula_tree_of H) implies (t ^ s) in (F -entry_points_in_subformula_tree_of H)

    proof

      defpred P[ Nat] means for F, G, H, t, s holds G = (( tree_of_subformulae F) . t) & H = (( tree_of_subformulae G) . s) & ( len s) = $1 implies (t ^ s) in (F -entry_points_in_subformula_tree_of H);

      

       A1: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A2: P[k];

        thus P[(k + 1)]

        proof

          

           A3: 1 in {1} by TARSKI:def 1;

          let F, G, H, t, s;

          assume that

           A4: G = (( tree_of_subformulae F) . t) and

           A5: H = (( tree_of_subformulae G) . s) and

           A6: ( len s) = (k + 1);

          consider v be FinSequence, x be set such that

           A7: s = (v ^ <*x*>) and

           A8: ( len v) = k by A6, TREES_2: 3;

          reconsider u = <*x*> as FinSequence of NAT by A7, FINSEQ_1: 36;

          

           A9: ( rng u) c= NAT by FINSEQ_1:def 4;

          ( dom u) = ( Seg 1) & (u . 1) = x by FINSEQ_1:def 8;

          then x in ( rng u) by A3, FINSEQ_1: 2, FUNCT_1:def 3;

          then

          reconsider m = x as Element of NAT by A9;

          reconsider v as FinSequence of NAT by A7, FINSEQ_1: 36;

          reconsider s9 = v as Element of ( dom ( tree_of_subformulae G)) by A7, TREES_1: 21;

          consider H9 such that

           A10: H9 = (( tree_of_subformulae G) . s9);

          

           A11: (t ^ s9) in (F -entry_points_in_subformula_tree_of H9) by A2, A4, A8, A10;

          (F -entry_points_in_subformula_tree_of H9) c= ( dom ( tree_of_subformulae F)) by TREES_1:def 11;

          then

          consider t9 be Element of ( dom ( tree_of_subformulae F)) such that

           A12: t9 = (t ^ s9) by A11;

          

           A13: H9 = (( tree_of_subformulae F) . t9) by A11, A12, Def3;

          

           A14: s = (s9 ^ <*m*>) by A7;

          then

           A15: H is_immediate_constituent_of H9 by A5, A10, Th7;

          

           A16: H = (( tree_of_subformulae F) . (t9 ^ <*m*>)) & (t9 ^ <*m*>) in ( dom ( tree_of_subformulae F))

          proof

            

             A17: H9 <> ( VERUM A) by A15, QC_LANG2: 41;

            now

              per cases by A15, A17, QC_LANG1: 9, QC_LANG2: 47;

                suppose

                 A18: H9 is negative;

                then H = ( the_argument_of H9) & m = 0 by A5, A14, A10, Th21;

                hence thesis by A13, A18, Th24;

              end;

                suppose

                 A19: H9 is conjunctive;

                then H = ( the_left_argument_of H9) & m = 0 or H = ( the_right_argument_of H9) & m = 1 by A5, A14, A10, Th22;

                hence thesis by A13, A19, Th25;

              end;

                suppose

                 A20: H9 is universal;

                then H = ( the_scope_of H9) & m = 0 by A5, A14, A10, Th23;

                hence thesis by A13, A20, Th26;

              end;

            end;

            hence thesis;

          end;

          (t ^ s) = (t9 ^ <*m*>) by A7, A12, FINSEQ_1: 32;

          hence thesis by A16, Def3;

        end;

      end;

      

       A21: P[ 0 ]

      proof

        let F, G, H, t, s;

        assume that

         A22: G = (( tree_of_subformulae F) . t) and

         A23: H = (( tree_of_subformulae G) . s) and

         A24: ( len s) = 0 ;

        

         A25: s = {} by A24;

        then

         A26: (t ^ s) = t by FINSEQ_1: 34;

        H = G by A23, A25, Def2;

        hence thesis by A22, A26, Def3;

      end;

      for k holds P[k] from NAT_1:sch 2( A21, A1);

      then

       A27: G = (( tree_of_subformulae F) . t) & H = (( tree_of_subformulae G) . s) & ( len s) = ( len s) implies (t ^ s) in (F -entry_points_in_subformula_tree_of H);

      assume t in (F -entry_points_in_subformula_tree_of G) & s in (G -entry_points_in_subformula_tree_of H);

      hence thesis by A27, Def3;

    end;

    reserve t for Element of ( dom ( tree_of_subformulae F)),

s for FinSequence;

    theorem :: QC_LANG4:28

    

     Th28: t in (F -entry_points_in_subformula_tree_of G) & (t ^ s) in (F -entry_points_in_subformula_tree_of H) implies s in (G -entry_points_in_subformula_tree_of H)

    proof

      defpred P[ Nat] means for F, G, H, t, s holds G = (( tree_of_subformulae F) . t) & (t ^ s) in (F -entry_points_in_subformula_tree_of H) & ( len s) = $1 implies s in (G -entry_points_in_subformula_tree_of H);

      

       A1: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A2: P[k];

        thus P[(k + 1)]

        proof

          let F, G, H, t, s;

          assume that

           A3: G = (( tree_of_subformulae F) . t) and

           A4: (t ^ s) in (F -entry_points_in_subformula_tree_of H) and

           A5: ( len s) = (k + 1);

          consider v be FinSequence, x be 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 be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t1) = H } by Th19;

          then

          consider t99 such that

           A8: t99 = (t ^ s) and

           A9: (( tree_of_subformulae F) . t99) = H by A4;

          reconsider s1 = s as FinSequence of NAT by A8, FINSEQ_1: 36;

          

           A10: s1 = (v ^ <*x*>) by A6;

          then

          reconsider u = <*x*> as FinSequence of NAT by FINSEQ_1: 36;

          reconsider v as FinSequence of NAT by A10, FINSEQ_1: 36;

          

           A11: ( rng u) c= NAT by FINSEQ_1:def 4;

          

           A12: 1 in {1} by TARSKI:def 1;

          ( dom u) = ( Seg 1) & (u . 1) = x by FINSEQ_1:def 8;

          then x in ( rng u) by A12, FINSEQ_1: 2, FUNCT_1:def 3;

          then

          reconsider m = x as Element of NAT by A11;

          consider t9 be FinSequence of NAT such that

           A13: t9 = (t ^ v);

          

           A14: t99 = (t9 ^ <*m*>) by A6, A8, A13, FINSEQ_1: 32;

          then t9 is_a_prefix_of t99 by TREES_1: 1;

          then

          reconsider t9 as Element of ( dom ( tree_of_subformulae F)) by TREES_1: 20;

          consider H9 such that

           A15: H9 = (( tree_of_subformulae F) . t9);

          (t ^ v) in (F -entry_points_in_subformula_tree_of H9) by A13, A15, Def3;

          then

           A16: v in (G -entry_points_in_subformula_tree_of H9) by A2, A3, A7;

          (G -entry_points_in_subformula_tree_of H9) = { v1 where v1 be Element of ( dom ( tree_of_subformulae G)) : (( tree_of_subformulae G) . v1) = H9 } by Th19;

          then

           A17: ex v1 be Element of ( dom ( tree_of_subformulae G)) st v = v1 & (( tree_of_subformulae G) . v1) = H9 by A16;

          then

          reconsider v as Element of ( dom ( tree_of_subformulae G));

          

           A18: H is_immediate_constituent_of H9 by A9, A14, A15, Th7;

          H = (( tree_of_subformulae G) . (v ^ <*m*>)) & (v ^ <*m*>) in ( dom ( tree_of_subformulae G))

          proof

            

             A19: H9 <> ( VERUM A) by A18, QC_LANG2: 41;

            now

              per cases by A18, A19, QC_LANG1: 9, QC_LANG2: 47;

                suppose

                 A20: H9 is negative;

                then H = ( the_argument_of H9) & m = 0 by A9, A14, A15, Th21;

                hence thesis by A17, A20, Th24;

              end;

                suppose

                 A21: H9 is conjunctive;

                then H = ( the_left_argument_of H9) & m = 0 or H = ( the_right_argument_of H9) & m = 1 by A9, A14, A15, Th22;

                hence thesis by A17, A21, Th25;

              end;

                suppose

                 A22: H9 is universal;

                then H = ( the_scope_of H9) & m = 0 by A9, A14, A15, Th23;

                hence thesis by A17, A22, Th26;

              end;

            end;

            hence thesis;

          end;

          hence thesis by A6, Def3;

        end;

      end;

      

       A23: P[ 0 ]

      proof

        let F, G, H, t, s;

        assume that

         A24: G = (( tree_of_subformulae F) . t) and

         A25: (t ^ s) in (F -entry_points_in_subformula_tree_of H) and

         A26: ( len s) = 0 ;

        

         A27: s = {} by A26;

        then

        reconsider s9 = s as Element of ( dom ( tree_of_subformulae G)) by TREES_1: 22;

        

         A28: G = (( tree_of_subformulae G) . s9) by A27, Def2;

        (F -entry_points_in_subformula_tree_of H) = { t1 where t1 be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t1) = H } by Th19;

        then ex t9 st t9 = (t ^ s) & (( tree_of_subformulae F) . t9) = H by A25;

        then H = G by A24, A27, FINSEQ_1: 34;

        hence thesis by A28, Def3;

      end;

      for k holds P[k] from NAT_1:sch 2( A23, A1);

      then

       A29: G = (( tree_of_subformulae F) . t) & (t ^ s) in (F -entry_points_in_subformula_tree_of H) & ( len s) = ( len s) implies s in (G -entry_points_in_subformula_tree_of H);

      assume t in (F -entry_points_in_subformula_tree_of G) & (t ^ s) in (F -entry_points_in_subformula_tree_of H);

      hence thesis by A29, Def3;

    end;

    theorem :: QC_LANG4:29

    

     Th29: for F, G, H holds { (t ^ s) where t be Element of ( dom ( tree_of_subformulae F)), s be Element of ( dom ( tree_of_subformulae G)) : t in (F -entry_points_in_subformula_tree_of G) & s in (G -entry_points_in_subformula_tree_of H) } c= (F -entry_points_in_subformula_tree_of H)

    proof

      let F, G, H;

      let x be object;

      assume x in { (t ^ s) where t be Element of ( dom ( tree_of_subformulae F)), s be Element of ( dom ( tree_of_subformulae G)) : t in (F -entry_points_in_subformula_tree_of G) & s in (G -entry_points_in_subformula_tree_of H) };

      then ex t be Element of ( dom ( tree_of_subformulae F)), s be Element of ( dom ( tree_of_subformulae G)) st x = (t ^ s) & t in (F -entry_points_in_subformula_tree_of G) & s in (G -entry_points_in_subformula_tree_of H);

      hence thesis by Th27;

    end;

    theorem :: QC_LANG4:30

    

     Th30: (( tree_of_subformulae F) | t) = ( tree_of_subformulae (( tree_of_subformulae F) . t))

    proof

      set T1 = (( tree_of_subformulae F) | t);

      set T2 = ( tree_of_subformulae (( tree_of_subformulae F) . t));

      thus

       A1: ( dom T1) = ( dom T2)

      proof

        let p be FinSequence of NAT ;

        now

          consider G such that

           A2: G = (( tree_of_subformulae F) . t);

          

           A3: t in (F -entry_points_in_subformula_tree_of G) by A2, Def3;

          consider t9 be FinSequence of NAT such that

           A4: t9 = (t ^ p);

          assume p in ( dom T1);

          then p in (( dom ( tree_of_subformulae F)) | t) by TREES_2:def 10;

          then

          reconsider t9 as Element of ( dom ( tree_of_subformulae F)) by A4, TREES_1:def 6;

          consider H such that

           A5: H = (( tree_of_subformulae F) . t9);

          

           A6: (G -entry_points_in_subformula_tree_of H) c= ( dom T2) by A2, TREES_1:def 11;

          t9 in (F -entry_points_in_subformula_tree_of H) by A5, Def3;

          then p in (G -entry_points_in_subformula_tree_of H) by A3, A4, Th28;

          hence p in ( dom T2) by A6;

        end;

        hence p in ( dom T1) implies p in ( dom T2);

        now

          consider G such that

           A7: G = (( tree_of_subformulae F) . t);

          assume p in ( dom T2);

          then

          reconsider s = p as Element of ( dom ( tree_of_subformulae G)) by A7;

          consider H such that

           A8: H = (( tree_of_subformulae G) . s);

          

           A9: s in (G -entry_points_in_subformula_tree_of H) by A8, Def3;

          

           A10: (F -entry_points_in_subformula_tree_of H) c= ( dom ( tree_of_subformulae F)) by TREES_1:def 11;

          t in (F -entry_points_in_subformula_tree_of G) by A7, Def3;

          then (t ^ s) in (F -entry_points_in_subformula_tree_of H) by A9, Th27;

          then s in (( dom ( tree_of_subformulae F)) | t) by A10, TREES_1:def 6;

          hence p in ( dom T1) by TREES_2:def 10;

        end;

        hence thesis;

      end;

      now

        let p be Node of T1;

        consider G such that

         A11: G = (( tree_of_subformulae F) . t);

        reconsider s = p as Element of ( dom ( tree_of_subformulae G)) by A1, A11;

        

         A12: ( dom T1) = (( dom ( tree_of_subformulae F)) | t) by TREES_2:def 10;

        then

        reconsider t9 = (t ^ s) as Element of ( dom ( tree_of_subformulae F)) by TREES_1:def 6;

        consider H such that

         A13: H = (T1 . p);

        

         A14: t in (F -entry_points_in_subformula_tree_of G) by A11, Def3;

        (T1 . p) = (( tree_of_subformulae F) . (t ^ p)) by A12, TREES_2:def 10;

        then t9 in (F -entry_points_in_subformula_tree_of H) by A13, Def3;

        then s in (G -entry_points_in_subformula_tree_of H) by A14, Th28;

        hence (T1 . p) = (T2 . p) by A11, A13, Def3;

      end;

      hence for p be Node of T1 holds (T1 . p) = (T2 . p);

    end;

    theorem :: QC_LANG4:31

    

     Th31: t in (F -entry_points_in_subformula_tree_of G) iff (( tree_of_subformulae F) | t) = ( tree_of_subformulae G)

    proof

      now

        assume t in (F -entry_points_in_subformula_tree_of G);

        then (( tree_of_subformulae F) . t) = G by Def3;

        hence (( tree_of_subformulae F) | t) = ( tree_of_subformulae G) by Th30;

      end;

      hence t in (F -entry_points_in_subformula_tree_of G) implies (( tree_of_subformulae F) | t) = ( tree_of_subformulae G);

      now

        assume (( tree_of_subformulae F) | t) = ( tree_of_subformulae G);

        then

         A1: (( tree_of_subformulae F) . t) = (( tree_of_subformulae G) . {} ) by TREES_9: 35;

        (( tree_of_subformulae G) . {} ) = G by Def2;

        hence t in (F -entry_points_in_subformula_tree_of G) by A1, Def3;

      end;

      hence thesis;

    end;

    theorem :: QC_LANG4:32

    (F -entry_points_in_subformula_tree_of G) = { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) | t) = ( tree_of_subformulae G) }

    proof

      thus (F -entry_points_in_subformula_tree_of G) c= { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) | t) = ( tree_of_subformulae G) }

      proof

        let x be object;

        assume

         A1: x in (F -entry_points_in_subformula_tree_of G);

        (F -entry_points_in_subformula_tree_of G) c= ( dom ( tree_of_subformulae F)) by TREES_1:def 11;

        then

        reconsider t9 = x as Element of ( dom ( tree_of_subformulae F)) by A1;

        (( tree_of_subformulae F) | t9) = ( tree_of_subformulae G) by A1, Th31;

        hence thesis;

      end;

      thus { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) | t) = ( tree_of_subformulae G) } c= (F -entry_points_in_subformula_tree_of G)

      proof

        let x be object;

        assume x in { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) | t) = ( tree_of_subformulae G) };

        then ex t9 st t9 = x & (( tree_of_subformulae F) | t9) = ( tree_of_subformulae G);

        hence thesis by Th31;

      end;

    end;

    reserve C for Chain of ( dom ( tree_of_subformulae F));

    theorem :: QC_LANG4:33

    for F, G, H, C st G in { (( tree_of_subformulae F) . t) where t be Element of ( dom ( tree_of_subformulae F)) : t in C } & H in { (( tree_of_subformulae F) . t) where t be Element of ( dom ( tree_of_subformulae F)) : t in C } holds G is_subformula_of H or H is_subformula_of G

    proof

      let F, G, H, C;

      assume that

       A1: G in { (( tree_of_subformulae F) . t) where t be Element of ( dom ( tree_of_subformulae F)) : t in C } and

       A2: H in { (( tree_of_subformulae F) . t) where t be Element of ( dom ( tree_of_subformulae F)) : t in C };

      consider t9 such that

       A3: G = (( tree_of_subformulae F) . t9) and

       A4: t9 in C by A1;

      consider t99 such that

       A5: H = (( tree_of_subformulae F) . t99) and

       A6: t99 in C by A2;

      

       A7: (t9,t99) are_c=-comparable by A4, A6, TREES_2:def 3;

      per cases by A7;

        suppose t9 is_a_prefix_of t99;

        hence thesis by A3, A5, Th13;

      end;

        suppose t99 is_a_prefix_of t9;

        hence thesis by A3, A5, Th13;

      end;

    end;

    definition

      let A;

      let F be Element of ( QC-WFF A);

      :: QC_LANG4:def4

      mode Subformula of F -> Element of ( QC-WFF A) means

      : Def4: it is_subformula_of F;

      existence ;

    end

    definition

      let A;

      let F be Element of ( QC-WFF A);

      let G be Subformula of F;

      :: QC_LANG4:def5

      mode Entry_Point_in_Subformula_Tree of G -> Element of ( dom ( tree_of_subformulae F)) means

      : Def5: (( tree_of_subformulae F) . it ) = G;

      existence

      proof

        G is_subformula_of F by Def4;

        then G in ( rng ( tree_of_subformulae F)) by Th10;

        then ex x be object st x in ( dom ( tree_of_subformulae F)) & (( tree_of_subformulae F) . x) = G by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    reserve G for Subformula of F;

    reserve t,t9 for Entry_Point_in_Subformula_Tree of G;

    theorem :: QC_LANG4:34

    t <> t9 implies not (t,t9) are_c=-comparable

    proof

      assume

       A1: t <> t9;

      (( tree_of_subformulae F) . t) = G & (( tree_of_subformulae F) . t9) = G by Def5;

      hence thesis by A1, Th18;

    end;

    definition

      let A;

      let F be Element of ( QC-WFF A);

      let G be Subformula of F;

      :: QC_LANG4:def6

      func entry_points_in_subformula_tree (G) -> non empty AntiChain_of_Prefixes of ( dom ( tree_of_subformulae F)) equals (F -entry_points_in_subformula_tree_of G);

      coherence by Def4, Th20;

    end

    theorem :: QC_LANG4:35

    

     Th35: t in ( entry_points_in_subformula_tree G)

    proof

      (( tree_of_subformulae F) . t) = G by Def5;

      hence thesis by Def3;

    end;

    theorem :: QC_LANG4:36

    

     Th36: ( entry_points_in_subformula_tree G) = { t where t be Entry_Point_in_Subformula_Tree of G : t = t }

    proof

      thus ( entry_points_in_subformula_tree G) c= { t where t be Entry_Point_in_Subformula_Tree of G : t = t }

      proof

        let x be object;

        assume x in ( entry_points_in_subformula_tree G);

        then x in { t where t be Element of ( dom ( tree_of_subformulae F)) : (( tree_of_subformulae F) . t) = G } by Th19;

        then

        consider t9 be Element of ( dom ( tree_of_subformulae F)) such that

         A1: t9 = x and

         A2: (( tree_of_subformulae F) . t9) = G;

        reconsider t9 as Entry_Point_in_Subformula_Tree of G by A2, Def5;

        t9 = t9;

        hence thesis by A1;

      end;

      thus { t where t be Entry_Point_in_Subformula_Tree of G : t = t } c= ( entry_points_in_subformula_tree G)

      proof

        let x be object;

        assume x in { t where t be Entry_Point_in_Subformula_Tree of G : t = t };

        then ex t st t = x & t = t;

        hence thesis by Th35;

      end;

    end;

    reserve G1,G2 for Subformula of F,

t1 for Entry_Point_in_Subformula_Tree of G1,

s for Element of ( dom ( tree_of_subformulae G1));

    theorem :: QC_LANG4:37

    

     Th37: s in (G1 -entry_points_in_subformula_tree_of G2) implies (t1 ^ s) is Entry_Point_in_Subformula_Tree of G2

    proof

      (( tree_of_subformulae F) . t1) = G1 by Def5;

      then

       A1: t1 in (F -entry_points_in_subformula_tree_of G1) by Def3;

      assume s in (G1 -entry_points_in_subformula_tree_of G2);

      then

       A2: (t1 ^ s) in (F -entry_points_in_subformula_tree_of G2) by A1, Th27;

      (F -entry_points_in_subformula_tree_of G2) c= ( dom ( tree_of_subformulae F)) by TREES_1:def 11;

      then

      reconsider t9 = (t1 ^ s) as Element of ( dom ( tree_of_subformulae F)) by A2;

      (( tree_of_subformulae F) . t9) = G2 by A2, Def3;

      hence thesis by Def5;

    end;

    reserve s for FinSequence;

    theorem :: QC_LANG4:38

    (t1 ^ s) is Entry_Point_in_Subformula_Tree of G2 implies s in (G1 -entry_points_in_subformula_tree_of G2)

    proof

      consider t9 be FinSequence such that

       A1: t9 = (t1 ^ s);

      (( tree_of_subformulae F) . t1) = G1 by Def5;

      then

       A2: t1 in (F -entry_points_in_subformula_tree_of G1) by Def3;

      assume (t1 ^ s) is Entry_Point_in_Subformula_Tree of G2;

      then t9 in { t2 where t2 be Entry_Point_in_Subformula_Tree of G2 : t2 = t2 } by A1;

      then t9 in ( entry_points_in_subformula_tree G2) by Th36;

      hence thesis by A2, A1, Th28;

    end;

    theorem :: QC_LANG4:39

    

     Th39: for F, G1, G2 holds { (t ^ s) where t be Entry_Point_in_Subformula_Tree of G1, s be Element of ( dom ( tree_of_subformulae G1)) : s in (G1 -entry_points_in_subformula_tree_of G2) } = { (t ^ s) where t be Element of ( dom ( tree_of_subformulae F)), s be Element of ( dom ( tree_of_subformulae G1)) : t in (F -entry_points_in_subformula_tree_of G1) & s in (G1 -entry_points_in_subformula_tree_of G2) }

    proof

      let F, G1, G2;

      thus { (t ^ s) where t be Entry_Point_in_Subformula_Tree of G1, s be Element of ( dom ( tree_of_subformulae G1)) : s in (G1 -entry_points_in_subformula_tree_of G2) } c= { (t ^ s) where t be Element of ( dom ( tree_of_subformulae F)), s be Element of ( dom ( tree_of_subformulae G1)) : t in (F -entry_points_in_subformula_tree_of G1) & s in (G1 -entry_points_in_subformula_tree_of G2) }

      proof

        let x be object;

        assume x in { (t ^ s) where t be Entry_Point_in_Subformula_Tree of G1, s be Element of ( dom ( tree_of_subformulae G1)) : s in (G1 -entry_points_in_subformula_tree_of G2) };

        then

        consider t1 be Entry_Point_in_Subformula_Tree of G1, s1 be Element of ( dom ( tree_of_subformulae G1)) such that

         A1: x = (t1 ^ s1) & s1 in (G1 -entry_points_in_subformula_tree_of G2);

        (( tree_of_subformulae F) . t1) = G1 by Def5;

        then t1 in (F -entry_points_in_subformula_tree_of G1) by Def3;

        hence thesis by A1;

      end;

      thus { (t ^ s) where t be Element of ( dom ( tree_of_subformulae F)), s be 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 be Entry_Point_in_Subformula_Tree of G1, s be Element of ( dom ( tree_of_subformulae G1)) : s in (G1 -entry_points_in_subformula_tree_of G2) }

      proof

        let x be object;

        assume x in { (t ^ s) where t be Element of ( dom ( tree_of_subformulae F)), s be 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 be Element of ( dom ( tree_of_subformulae F)), s1 be Element of ( dom ( tree_of_subformulae G1)) such that

         A2: x = (t1 ^ s1) and

         A3: t1 in (F -entry_points_in_subformula_tree_of G1) and

         A4: s1 in (G1 -entry_points_in_subformula_tree_of G2);

        (( tree_of_subformulae F) . t1) = G1 by A3, Def3;

        then

        reconsider t1 as Entry_Point_in_Subformula_Tree of G1 by Def5;

        x = (t1 ^ s1) by A2;

        hence thesis by A4;

      end;

    end;

    theorem :: QC_LANG4:40

    for F, G1, G2 holds { (t ^ s) where t be Entry_Point_in_Subformula_Tree of G1, s be Element of ( dom ( tree_of_subformulae G1)) : s in (G1 -entry_points_in_subformula_tree_of G2) } c= ( entry_points_in_subformula_tree G2)

    proof

      let F, G1, G2;

      { (t ^ s) where t be Entry_Point_in_Subformula_Tree of G1, s be Element of ( dom ( tree_of_subformulae G1)) : s in (G1 -entry_points_in_subformula_tree_of G2) } = { (t ^ s) where t be Element of ( dom ( tree_of_subformulae F)), s be Element of ( dom ( tree_of_subformulae G1)) : t in (F -entry_points_in_subformula_tree_of G1) & s in (G1 -entry_points_in_subformula_tree_of G2) } by Th39;

      hence thesis by Th29;

    end;

    reserve G1,G2 for Subformula of F,

t1 for Entry_Point_in_Subformula_Tree of G1,

t2 for Entry_Point_in_Subformula_Tree of G2;

    theorem :: QC_LANG4:41

    (ex t1, t2 st t1 is_a_prefix_of t2) implies G2 is_subformula_of G1

    proof

      given t1, t2 such that

       A1: t1 is_a_prefix_of t2;

      (( tree_of_subformulae F) . t1) = G1 & (( tree_of_subformulae F) . t2) = G2 by Def5;

      hence thesis by A1, Th13;

    end;

    theorem :: QC_LANG4:42

    G2 is_subformula_of G1 implies for t1 holds ex t2 st t1 is_a_prefix_of t2

    proof

      assume

       A1: G2 is_subformula_of G1;

      now

        let t1;

        consider H be Element of ( QC-WFF A) such that

         A2: H = G2;

        reconsider H as Subformula of G1 by A1, A2, Def4;

        set s = the Entry_Point_in_Subformula_Tree of H;

        (( tree_of_subformulae G1) . s) = H by Def5;

        then s in (G1 -entry_points_in_subformula_tree_of G2) by A2, Def3;

        then (t1 ^ s) is Entry_Point_in_Subformula_Tree of G2 by Th37;

        then

        consider t2 such that

         A3: t2 = (t1 ^ s);

        take t2;

        thus t1 is_a_prefix_of t2 by A3, TREES_1: 1;

      end;

      hence thesis;

    end;