:: by Oleg Okhotnikov

::

:: Received October 2, 1995

:: Copyright (c) 1995-2021 Association of Mizar Users

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)

for F, G being Element of QC-WFF A st F is_subformula_of G holds

len (@ F) <= len (@ G)

proof 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 by QC_LANG2:54, QC_LANG2:def 21;

for F, G being Element of QC-WFF A st F is_subformula_of G & len (@ F) = len (@ G) holds

F = G by QC_LANG2:54, QC_LANG2:def 21;

definition

let A be QC-alphabet ;

let p be Element of QC-WFF A;

( ( ( 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 b_{1} being FinSequence of QC-WFF A holds

( ( ( p = VERUM A or p is atomic ) & p is negative implies ( b_{1} = <*> (QC-WFF A) iff b_{1} = <*(the_argument_of p)*> ) ) & ( ( p = VERUM A or p is atomic ) & p is conjunctive implies ( b_{1} = <*> (QC-WFF A) iff b_{1} = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) & ( p is negative & p is conjunctive implies ( b_{1} = <*(the_argument_of p)*> iff b_{1} = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) )
by QC_LANG1:20;

end;
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 <*> (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)*>;

( ( ( 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 b

( ( ( p = VERUM A or p is atomic ) & p is negative implies ( b

:: 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)*> ) );

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 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

for k being 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 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 }

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 end;

definition

let A be QC-alphabet ;

let p be Element of QC-WFF A;

ex b_{1} being finite DecoratedTree of QC-WFF A st

( b_{1} . {} = p & ( for x being Element of dom b_{1} holds succ (b_{1},x) = list_of_immediate_constituents (b_{1} . x) ) )

for b_{1}, b_{2} being finite DecoratedTree of QC-WFF A st b_{1} . {} = p & ( for x being Element of dom b_{1} holds succ (b_{1},x) = list_of_immediate_constituents (b_{1} . x) ) & b_{2} . {} = p & ( for x being Element of dom b_{2} holds succ (b_{2},x) = list_of_immediate_constituents (b_{2} . x) ) holds

b_{1} = b_{2}

end;
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 ( it . {} = p & ( for x being Element of dom it holds succ (it,x) = list_of_immediate_constituents (it . x) ) );

ex b

( b

proof end;

uniqueness for b

b

proof 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 b_{3} being finite DecoratedTree of QC-WFF A holds

( b_{3} = tree_of_subformulae p iff ( b_{3} . {} = p & ( for x being Element of dom b_{3} holds succ (b_{3},x) = list_of_immediate_constituents (b_{3} . x) ) ) );

for A being QC-alphabet

for p being Element of QC-WFF A

for b

( b

theorem Th6: :: QC_LANG4:6

for A being QC-alphabet

for n being 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 )

for n being 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 end;

theorem Th7: :: QC_LANG4:7

for A being QC-alphabet

for F, H 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 Nat st

( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )

for F, H 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 Nat st

( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )

proof end;

theorem Th8: :: QC_LANG4:8

for A being QC-alphabet

for F, G, 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)

for F, G, 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 end;

theorem Th9: :: QC_LANG4:9

for A being QC-alphabet

for F, G, 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)

for F, G, 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 end;

theorem Th10: :: QC_LANG4:10

for A being QC-alphabet

for F, G being Element of QC-WFF A holds

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

for F, G being Element of QC-WFF A holds

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

proof 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

for F being Element of QC-WFF A holds rng (tree_of_subformulae F) = Subformulae F

proof end;

theorem :: QC_LANG4:12

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 t9 in succ t holds

(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t

for F being Element of QC-WFF A

for t, t9 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 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

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 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))

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 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

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 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

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 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 = {} )

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 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

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 end;

definition

let A be QC-alphabet ;

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

ex b_{1} being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st

for t being Element of dom (tree_of_subformulae F) holds

( t in b_{1} iff (tree_of_subformulae F) . t = G )

for b_{1}, b_{2} being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st ( for t being Element of dom (tree_of_subformulae F) holds

( t in b_{1} iff (tree_of_subformulae F) . t = G ) ) & ( for t being Element of dom (tree_of_subformulae F) holds

( t in b_{2} iff (tree_of_subformulae F) . t = G ) ) holds

b_{1} = b_{2}

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

func F -entry_points_in_subformula_tree_of G -> AntiChain_of_Prefixes of dom (tree_of_subformulae F) means :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 for t being Element of dom (tree_of_subformulae F) holds

( t in it iff (tree_of_subformulae F) . t = G );

ex b

for t being Element of dom (tree_of_subformulae F) holds

( t in b

proof end;

uniqueness for b

( t in b

( t in b

b

proof 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 b_{4} being AntiChain_of_Prefixes of dom (tree_of_subformulae F) holds

( b_{4} = F -entry_points_in_subformula_tree_of G iff for t being Element of dom (tree_of_subformulae F) holds

( t in b_{4} iff (tree_of_subformulae F) . t = G ) );

for A being QC-alphabet

for F, G being Element of QC-WFF A

for b

( b

( t in b

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 }

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 end;

theorem Th20: :: QC_LANG4:20

for A being QC-alphabet

for F, G being Element of QC-WFF A holds

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

for F, G being Element of QC-WFF A holds

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

proof end;

theorem Th21: :: QC_LANG4:21

for A being QC-alphabet

for m being Nat

for F being Element of QC-WFF A

for t, t9 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 )

for m being Nat

for F being Element of QC-WFF A

for t, t9 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 end;

theorem Th22: :: QC_LANG4:22

for A being QC-alphabet

for m being Nat

for F being Element of QC-WFF A

for t, t9 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 )

for m being Nat

for F being Element of QC-WFF A

for t, t9 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 end;

theorem Th23: :: QC_LANG4:23

for A being QC-alphabet

for m being Nat

for F being Element of QC-WFF A

for t, t9 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 )

for m being Nat

for F being Element of QC-WFF A

for t, t9 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 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) )

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 end;

Lm1: for x, y being set holds dom <*x,y*> = Seg 2

proof 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) )

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 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) )

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 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

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 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

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 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

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 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)

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 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 )

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 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 }

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 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

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 end;

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

existence

ex b_{1} being Element of QC-WFF A st b_{1} is_subformula_of F
;

end;
let F be Element of QC-WFF A;

existence

ex b

:: deftheorem Def4 defines Subformula QC_LANG4:def 4 :

for A being QC-alphabet

for F, b_{3} being Element of QC-WFF A holds

( b_{3} is Subformula of F iff b_{3} is_subformula_of F );

for A being QC-alphabet

for F, b

( b

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

let G be Subformula of F;

ex b_{1} being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . b_{1} = G

end;
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 (tree_of_subformulae F) . it = G;

ex b

proof 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 b_{4} being Element of dom (tree_of_subformulae F) holds

( b_{4} is Entry_Point_in_Subformula_Tree of G iff (tree_of_subformulae F) . b_{4} = G );

for A being QC-alphabet

for F being Element of QC-WFF A

for G being Subformula of F

for b

( b

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

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 end;

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

let G be Subformula of F;

F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F) by Def4, Th20;

end;
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;

F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F) by Def4, Th20;

:: 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;

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

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 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 }

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 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

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 end;

theorem :: QC_LANG4:38

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 FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds

s in G1 -entry_points_in_subformula_tree_of G2

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 FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds

s in G1 -entry_points_in_subformula_tree_of G2

proof 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 ) }

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 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

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 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

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 end;

theorem :: QC_LANG4:42

for A being QC-alphabet

for F being Element of QC-WFF A

for G1, G2 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

for F being Element of QC-WFF A

for G1, G2 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 end;