The abstract of the Mizar article:

The Subformula Tree of a Formula of the First Order Language

by

Oleg Okhotnikov

Received October 2, 1995

MML identifier: QC_LANG4

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, RELAT_1, TREES_1, ZFMISC_1, FUNCT_1, TREES_2, FINSET_1,
      TREES_4, BOOLE, TREES_9, ORDINAL1, CARD_1, MCART_1, ORDERS_1, TARSKI,
      QC_LANG1, ZF_LANG, QC_LANG4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSEQ_1, FINSEQ_4, CARD_1, TREES_1,
      TREES_2, TREES_4, TREES_9, QC_LANG1, QC_LANG2, MCART_1;
 constructors NAT_1, FINSEQ_4, TREES_4, TREES_9, QC_LANG2, XREAL_0, MEMBERED;
 clusters SUBSET_1, TREES_1, TREES_2, TREES_9, RELSET_1, TREES_A, FINSET_1,
      FINSEQ_1, NAT_1, MEMBERED, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

canceled 3;

theorem :: QC_LANG4:4
  for n being Nat, r being FinSequence ex q being FinSequence st
    q = r|Seg n & q is_a_prefix_of r;

canceled;

theorem :: QC_LANG4:6
  for D being non empty set, r being FinSequence of D,
    r1,r2 being FinSequence, k being Nat
      st k+1 <= len r & r1 = r|Seg (k+1) & r2 = r|Seg k holds
        ex x being Element of D st r1 = r2^<*x*>;

theorem :: QC_LANG4:7
  for D being non empty set, r being FinSequence of D, r1 being FinSequence
    st 1 <= len r & r1 = r|Seg 1 holds ex x being Element of D st r1 = <*x*>;

definition let D be non empty set, T be DecoratedTree of D;
 cluster -> Function-like Relation-like Element of dom T;
end;

definition let D be non empty set, T be DecoratedTree of D;
 cluster -> FinSequence-like Element of dom T;
end;

definition let D be non empty set;
 cluster finite DecoratedTree of D;
end;

reserve T for DecoratedTree,
        p for FinSequence of NAT;

theorem :: QC_LANG4:8
  T.p = (T|p).{};

reserve T for finite-branching DecoratedTree,
        t for Element of dom T,
        x for FinSequence,
        n, k, m for Nat;

theorem :: QC_LANG4:9
  succ(T,t) = T*(t succ);

theorem :: QC_LANG4:10
  dom (T*(t succ)) = dom (t succ);

theorem :: QC_LANG4:11
  dom succ(T,t) = dom (t succ);

theorem :: QC_LANG4:12
  t^<*n*> in dom T iff n+1 in dom (t succ);

theorem :: QC_LANG4:13
  for T, x, n st x^<*n*> in dom T holds T.(x^<*n*>) = succ(T,x).(n+1);

reserve x, x' for Element of dom T,
        y' for set;

theorem :: QC_LANG4:14
  x' in succ x implies T.x' in rng succ(T,x);

theorem :: QC_LANG4:15
  y' in rng succ(T,x) implies ex x' st y' = T.x' & x' in succ x;

reserve n,k1,k2,l,k,m for Nat,
        x,y,y1,y2 for set;

scheme ExDecTrees { D() -> non empty set, d() -> Element of D(),
    G(set) -> FinSequence of D() }:
 ex T being finite-branching DecoratedTree of D() st
    T.{} = d() &
    for t being Element of dom T, w being Element of D() st w = T.t
      holds succ(T,t) = G(w);

theorem :: QC_LANG4:16
  for T being Tree, t being Element of T holds
    ProperPrefixes t is finite Chain of T;

theorem :: QC_LANG4:17
  for T being Tree holds T-level 0 = {{}};

theorem :: QC_LANG4:18
  for T being Tree holds
    T-level (n+1) = union { succ w where w is Element of T : len w = n };

theorem :: QC_LANG4:19
  for T being finite-branching Tree, n being Nat holds T-level n is finite;

theorem :: QC_LANG4:20
  for T being finite-branching Tree holds
    T is finite iff ex n being Nat st T-level n = {};

theorem :: QC_LANG4:21
  for T being finite-branching Tree st not T is finite
    ex C being Chain of T st not C is finite;

theorem :: QC_LANG4:22
  for T being finite-branching Tree st not T is finite
    ex B being Branch of T st not B is finite;

theorem :: QC_LANG4:23
  for T being Tree, C being Chain of T, t being Element of T
    st t in C & not C is finite
      ex t' being Element of T st t' in C & t is_a_proper_prefix_of t';

theorem :: QC_LANG4:24
  for T being Tree, B being Branch of T, t being Element of T
    st t in B & not B is finite
      ex t' being Element of T st t' in B & t' in succ t;

theorem :: QC_LANG4:25
  for f being Function of NAT,NAT st
   (for n holds f.(n+1) qua Nat <= f.n qua Nat)
     ex m st for n st m <= n holds f.n = f.m;

scheme FinDecTree { D() -> non empty set,
    T() -> finite-branching DecoratedTree of D(), F(Element of D()) -> Nat }:
  T() is finite
provided
for t,t' being Element of dom T(), d being Element of D()
    st t' in succ t & d = T().t' holds F(d) < F(T().t);

reserve D for non empty set,
        T for DecoratedTree of D;

theorem :: QC_LANG4:26
  for y being set st y in rng T holds y is Element of D;

theorem :: QC_LANG4:27
  for x being set st x in dom T holds T.x is Element of D;

begin

reserve F, G, G',H, H' for Element of QC-WFF;

theorem :: QC_LANG4:28
  F is_subformula_of G implies len @ F <= len @ G;

theorem :: QC_LANG4:29
    F is_subformula_of G & len @ F = len @ G implies F = G;

definition let p be Element of QC-WFF;
  func list_of_immediate_constituents(p) -> FinSequence of QC-WFF equals
:: QC_LANG4:def 1
     <*> QC-WFF if p = VERUM or p is atomic,
     <* the_argument_of p *> if p is negative,
     <* the_left_argument_of p, the_right_argument_of p *> if
      p is conjunctive
    otherwise <* the_scope_of p *>;
end;

theorem :: QC_LANG4:30
  k in dom list_of_immediate_constituents(F) &
    G = (list_of_immediate_constituents(F)).k implies
      G is_immediate_constituent_of F;

theorem :: QC_LANG4:31
  rng list_of_immediate_constituents(F) =
    { G where G is Element of QC-WFF : G is_immediate_constituent_of F };

definition let p be Element of QC-WFF;
  func tree_of_subformulae(p) -> finite DecoratedTree of QC-WFF means
:: QC_LANG4:def 2
    it.{} = p & for x being Element of dom it holds
      succ(it,x) = list_of_immediate_constituents(it.x);
end;

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

canceled 2;

theorem :: QC_LANG4:34
  F in rng tree_of_subformulae(F);

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

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

theorem :: QC_LANG4:37
  G in rng tree_of_subformulae(F) & H is_immediate_constituent_of G
    implies H in rng tree_of_subformulae(F);

theorem :: QC_LANG4:38
  G in rng tree_of_subformulae(F) & H is_subformula_of G implies
    H in rng tree_of_subformulae(F);

theorem :: QC_LANG4:39
  G in rng tree_of_subformulae(F) iff G is_subformula_of F;

theorem :: QC_LANG4:40
    rng tree_of_subformulae(F) = Subformulae(F);

theorem :: QC_LANG4:41
    t' in succ t implies (tree_of_subformulae(F)).t'
    is_immediate_constituent_of (tree_of_subformulae(F)).t;

reserve x,y1,y2 for set;

theorem :: QC_LANG4:42
  t is_a_prefix_of t' implies (tree_of_subformulae(F)).t'
    is_subformula_of (tree_of_subformulae(F)).t;

theorem :: QC_LANG4:43
  t is_a_proper_prefix_of t' implies
    len @((tree_of_subformulae(F)).t') < len @((tree_of_subformulae(F)).t);

theorem :: QC_LANG4:44
  t is_a_proper_prefix_of t' implies
    (tree_of_subformulae(F)).t' <> (tree_of_subformulae(F)).t;

theorem :: QC_LANG4:45
  t is_a_proper_prefix_of t' implies (tree_of_subformulae(F)).t'
    is_proper_subformula_of (tree_of_subformulae(F)).t;

theorem :: QC_LANG4:46
    (tree_of_subformulae(F)).t = F iff t = {};

theorem :: QC_LANG4:47
  t <> t' & (tree_of_subformulae(F)).t = (tree_of_subformulae(F)).t' implies
    not t,t' are_c=-comparable;

definition let F, G be Element of QC-WFF;
  func F-entry_points_in_subformula_tree_of G ->
    AntiChain_of_Prefixes of dom tree_of_subformulae(F) means
:: QC_LANG4:def 3
      for t being Element of dom tree_of_subformulae(F) holds
        t in it iff (tree_of_subformulae(F)).t = G;
end;

canceled;

theorem :: QC_LANG4:49
  F-entry_points_in_subformula_tree_of G =
    { t where t is Element of dom tree_of_subformulae(F) :
      (tree_of_subformulae(F)).t = G };

theorem :: QC_LANG4:50
  G is_subformula_of F iff F-entry_points_in_subformula_tree_of G <> {};

theorem :: QC_LANG4:51
  t' = t^<*m*> & (tree_of_subformulae(F)).t is negative implies
    (tree_of_subformulae(F)).t' = the_argument_of (tree_of_subformulae(F)).t &
      m = 0;

theorem :: QC_LANG4:52
  t' = t^<*m*> & (tree_of_subformulae(F)).t is conjunctive implies
    (tree_of_subformulae(F)).t'
      = the_left_argument_of (tree_of_subformulae(F)).t & m = 0 or
    (tree_of_subformulae(F)).t'
      = the_right_argument_of (tree_of_subformulae(F)).t & m = 1;

theorem :: QC_LANG4:53
  t' = t^<*m*> & (tree_of_subformulae(F)).t is universal implies
    (tree_of_subformulae(F)).t' = the_scope_of (tree_of_subformulae(F)).t &
      m = 0;

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

reserve x,y for set;

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

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

reserve t for Element of dom tree_of_subformulae(F),
        s for Element of dom tree_of_subformulae(G);

theorem :: QC_LANG4:57
  t in F-entry_points_in_subformula_tree_of G &
  s in G-entry_points_in_subformula_tree_of H implies
  t^s in F-entry_points_in_subformula_tree_of H;

reserve t for Element of dom tree_of_subformulae(F),
        s for FinSequence;

theorem :: QC_LANG4:58
  t in F-entry_points_in_subformula_tree_of G &
  t^s in F-entry_points_in_subformula_tree_of H implies
  s in G-entry_points_in_subformula_tree_of H;

theorem :: QC_LANG4:59
for F,G,H holds
  { t^s where t is Element of dom tree_of_subformulae(F),
    s is Element of dom tree_of_subformulae(G) :
      t in F-entry_points_in_subformula_tree_of G &
      s in G-entry_points_in_subformula_tree_of H } c=
  F-entry_points_in_subformula_tree_of H;

theorem :: QC_LANG4:60
  (tree_of_subformulae(F))|t
    = tree_of_subformulae((tree_of_subformulae(F)).t);

theorem :: QC_LANG4:61
  t in F-entry_points_in_subformula_tree_of G iff
    (tree_of_subformulae(F))|t = tree_of_subformulae(G);

theorem :: QC_LANG4:62
    F-entry_points_in_subformula_tree_of G =
    { t where t is Element of dom tree_of_subformulae(F) :
      (tree_of_subformulae(F))|t = tree_of_subformulae(G) };

reserve C for Chain of dom tree_of_subformulae(F);

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

definition let F be Element of QC-WFF;
  mode Subformula of F -> Element of QC-WFF means
:: QC_LANG4:def 4
    it is_subformula_of F;
end;

definition let F be Element of QC-WFF; let G be Subformula of F;
  mode Entry_Point_in_Subformula_Tree of G ->
    Element of dom tree_of_subformulae(F) means
:: QC_LANG4:def 5
      (tree_of_subformulae(F)).it = G;
end;

reserve G for Subformula of F;

reserve t, t' for Entry_Point_in_Subformula_Tree of G;

canceled;

theorem :: QC_LANG4:65
    t <> t' implies not t,t' are_c=-comparable;

definition let F be Element of QC-WFF; let G be Subformula of F;
  func entry_points_in_subformula_tree(G) ->
    non empty AntiChain_of_Prefixes of dom tree_of_subformulae(F) equals
:: QC_LANG4:def 6
      F-entry_points_in_subformula_tree_of G;
end;

canceled;

theorem :: QC_LANG4:67
  t in entry_points_in_subformula_tree(G);

theorem :: QC_LANG4:68
  entry_points_in_subformula_tree(G) =
    { t where t is Entry_Point_in_Subformula_Tree of G : t = t };

reserve G1, G2 for Subformula of F,
        t1 for Entry_Point_in_Subformula_Tree of G1,
        s for Element of dom tree_of_subformulae(G1);

theorem :: QC_LANG4:69
  s in G1-entry_points_in_subformula_tree_of G2 implies
    t1^s is Entry_Point_in_Subformula_Tree of G2;

reserve s for FinSequence;

theorem :: QC_LANG4:70
    t1^s is Entry_Point_in_Subformula_Tree of G2 implies
  s in G1-entry_points_in_subformula_tree_of G2;

theorem :: QC_LANG4:71
for F,G1,G2 holds
  { t^s where t is Entry_Point_in_Subformula_Tree of G1,
    s is Element of dom tree_of_subformulae(G1) :
      s in G1-entry_points_in_subformula_tree_of G2 } =
  { t^s where t is Element of dom tree_of_subformulae(F),
    s is Element of dom tree_of_subformulae(G1) :
      t in F-entry_points_in_subformula_tree_of G1 &
      s in G1-entry_points_in_subformula_tree_of G2 };

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

reserve G1, G2 for Subformula of F,
        t1 for Entry_Point_in_Subformula_Tree of G1,
        t2 for Entry_Point_in_Subformula_Tree of G2;

theorem :: QC_LANG4:73
    (ex t1,t2 st t1 is_a_prefix_of t2) implies G2 is_subformula_of G1;

theorem :: QC_LANG4:74
    G2 is_subformula_of G1 implies for t1 ex t2 st t1 is_a_prefix_of t2;