:: The Subformula Tree of a Formula of the First Order Language
:: by Oleg Okhotnikov
::
:: Received October 2, 1995
:: Copyright (c) 1995-2011 Association of Mizar Users

begin

theorem :: QC_LANG4:1

canceled;

theorem :: QC_LANG4:2

canceled;

theorem :: QC_LANG4:3

canceled;

theorem :: QC_LANG4:4

canceled;

theorem :: QC_LANG4:5

canceled;

theorem :: QC_LANG4:6

canceled;

theorem :: QC_LANG4:7

canceled;

theorem :: QC_LANG4:8

canceled;

theorem :: QC_LANG4:9

canceled;

theorem :: QC_LANG4:10

canceled;

theorem :: QC_LANG4:11

canceled;

theorem :: QC_LANG4:12

canceled;

theorem :: QC_LANG4:13

canceled;

theorem :: QC_LANG4:14

canceled;

theorem :: QC_LANG4:15

canceled;

theorem :: QC_LANG4:16

canceled;

theorem :: QC_LANG4:17

canceled;

theorem :: QC_LANG4:18

canceled;

theorem :: QC_LANG4:19

canceled;

theorem :: QC_LANG4:20

canceled;

theorem :: QC_LANG4:21

canceled;

theorem :: QC_LANG4:22

canceled;

theorem :: QC_LANG4:23

canceled;

theorem :: QC_LANG4:24

canceled;

theorem :: QC_LANG4:25

canceled;

theorem :: QC_LANG4:26

canceled;

theorem :: QC_LANG4:27

canceled;

theorem Th28: :: QC_LANG4:28

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

proof end;

theorem :: QC_LANG4:29

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

proof end;

definition

let p be Element of QC-WFF ;
func list_of_immediate_constituents p -> FinSequence of QC-WFF equals :Def1: :: 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)*>;
coherence
( ( ( p = VERUM or p is atomic ) implies <*> QC-WFF is FinSequence of QC-WFF ) & ( p is negative implies <*(the_argument_of p)*> is FinSequence of QC-WFF ) & ( p is conjunctive implies <*(the_left_argument_of p),(the_right_argument_of p)*> is FinSequence of QC-WFF ) & ( p = VERUM or p is atomic or p is negative or p is conjunctive or <*(the_scope_of p)*> is FinSequence of QC-WFF ) ) ;
consistency
for b₁ being FinSequence of QC-WFF holds
( ( ( p = VERUM or p is atomic ) & p is negative implies ( b₁ = <*> QC-WFF iff b₁ = <*(the_argument_of p)*> ) ) & ( ( p = VERUM or p is atomic ) & p is conjunctive implies ( b₁ = <*> QC-WFF iff b₁ = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) & ( p is negative & p is conjunctive implies ( b₁ = <*(the_argument_of p)*> iff b₁ = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) ) by QC_LANG1:51;

end;

:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def 1 :
for p being Element of QC-WFF holds
( ( ( p = VERUM or p is atomic ) implies list_of_immediate_constituents p = <*> QC-WFF ) & ( 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 or p is atomic or p is negative or p is conjunctive or list_of_immediate_constituents p = <*(the_scope_of p)*> ) );

theorem Th30: :: QC_LANG4:30

for k being Element of NAT
for F, G being Element of QC-WFF 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 Th31: :: QC_LANG4:31

for F being Element of QC-WFF holds rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF : G is_immediate_constituent_of F }

proof end;

definition

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

proof end;

uniqueness
for b₁, b₂ being finite DecoratedTree of QC-WFF st b₁ . {} = p & ( for x being Element of dom b₁ holds succ (b₁,x) = list_of_immediate_constituents (b₁ . x) ) & b₂ . {} = p & ( for x being Element of dom b₂ holds succ (b₂,x) = list_of_immediate_constituents (b₂ . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def 2 :
for p being Element of QC-WFF
for b₂ being finite DecoratedTree of QC-WFF holds
( b₂ = tree_of_subformulae p iff ( b₂ . {} = p & ( for x being Element of dom b₂ holds succ (b₂,x) = list_of_immediate_constituents (b₂ . x) ) ) );

theorem :: QC_LANG4:32

canceled;

theorem :: QC_LANG4:33

canceled;

theorem Th34: :: QC_LANG4:34

for F being Element of QC-WFF holds F in rng (tree_of_subformulae F)

proof end;

theorem Th35: :: QC_LANG4:35

for n being Element of NAT
for F being Element of QC-WFF
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 st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )

proof end;

theorem Th36: :: QC_LANG4:36

for H, F being Element of QC-WFF
for t being Element of dom (tree_of_subformulae F) holds
( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )

proof end;

theorem Th37: :: QC_LANG4:37

for G, F, H being Element of QC-WFF 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 Th38: :: QC_LANG4:38

for G, F, H being Element of QC-WFF st G in rng (tree_of_subformulae F) & H is_subformula_of G holds
H in rng (tree_of_subformulae F)

proof end;

theorem Th39: :: QC_LANG4:39

for G, F being Element of QC-WFF holds
( G in rng (tree_of_subformulae F) iff G is_subformula_of F )

proof end;

theorem :: QC_LANG4:40

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

proof end;

theorem :: QC_LANG4:41

for F being Element of QC-WFF
for t9, t being Element of dom (tree_of_subformulae F) st t9 in succ t holds
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t

proof end;

theorem Th42: :: QC_LANG4:42

for F being Element of QC-WFF
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 Th43: :: QC_LANG4:43

for F being Element of QC-WFF
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 Th44: :: QC_LANG4:44

for F being Element of QC-WFF
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 Th45: :: QC_LANG4:45

for F being Element of QC-WFF
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:46

for F being Element of QC-WFF
for t being Element of dom (tree_of_subformulae F) holds
( (tree_of_subformulae F) . t = F iff t = {} )

proof end;

theorem Th47: :: QC_LANG4:47

for F being Element of QC-WFF
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 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 :Def3: :: QC_LANG4:def 3
for t being Element of dom (tree_of_subformulae F) holds
( t in it iff (tree_of_subformulae F) . t = G );
existence
ex b₁ 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₁ iff (tree_of_subformulae F) . t = G )

proof end;

uniqueness
for b₁, b₂ 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₁ iff (tree_of_subformulae F) . t = G ) ) & ( for t being Element of dom (tree_of_subformulae F) holds
( t in b₂ iff (tree_of_subformulae F) . t = G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def 3 :
for F, G being Element of QC-WFF
for b₃ being AntiChain_of_Prefixes of dom (tree_of_subformulae F) holds
( b₃ = F -entry_points_in_subformula_tree_of G iff for t being Element of dom (tree_of_subformulae F) holds
( t in b₃ iff (tree_of_subformulae F) . t = G ) );

theorem :: QC_LANG4:48

canceled;

theorem Th49: :: QC_LANG4:49

for F, G being Element of QC-WFF 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 Th50: :: QC_LANG4:50

for G, F being Element of QC-WFF holds
( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} )

proof end;

theorem Th51: :: QC_LANG4:51

for m being Element of NAT
for F being Element of QC-WFF
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )

proof end;

theorem Th52: :: QC_LANG4:52

for m being Element of NAT
for F being Element of QC-WFF
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )

proof end;

theorem Th53: :: QC_LANG4:53

for m being Element of NAT
for F being Element of QC-WFF
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )

proof end;

theorem Th54: :: QC_LANG4:54

for F being Element of QC-WFF
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 Th55: :: QC_LANG4:55

for F being Element of QC-WFF
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 Th56: :: QC_LANG4:56

for F being Element of QC-WFF
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 Th57: :: QC_LANG4:57

for F, G, H being Element of QC-WFF
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 Th58: :: QC_LANG4:58

for F, G, H being Element of QC-WFF
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 Th59: :: QC_LANG4:59

for F, G, H being Element of QC-WFF 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 Th60: :: QC_LANG4:60

for F being Element of QC-WFF
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 Th61: :: QC_LANG4:61

for F, G being Element of QC-WFF
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:62

for F, G being Element of QC-WFF 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:63

for F, G, H being Element of QC-WFF
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 F be Element of QC-WFF ;
mode Subformula of F -> Element of QC-WFF means :Def4: :: QC_LANG4:def 4
it is_subformula_of F;
existence
ex b₁ being Element of QC-WFF st b₁ is_subformula_of F ;

end;

:: deftheorem Def4 defines Subformula QC_LANG4:def 4 :
for F, b₂ being Element of QC-WFF holds
( b₂ is Subformula of F iff b₂ is_subformula_of F );

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 :Def5: :: QC_LANG4:def 5
(tree_of_subformulae F) . it = G;
existence
ex b₁ being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . b₁ = G

proof end;

end;

:: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def 5 :
for F being Element of QC-WFF
for G being Subformula of F
for b₃ being Element of dom (tree_of_subformulae F) holds
( b₃ is Entry_Point_in_Subformula_Tree of G iff (tree_of_subformulae F) . b₃ = G );

theorem :: QC_LANG4:64

canceled;

theorem :: QC_LANG4:65

for F being Element of QC-WFF
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 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;
coherence
F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F)

proof end;

end;

:: deftheorem defines entry_points_in_subformula_tree QC_LANG4:def 6 :
for F being Element of QC-WFF
for G being Subformula of F holds entry_points_in_subformula_tree G = F -entry_points_in_subformula_tree_of G;

theorem :: QC_LANG4:66

canceled;

theorem Th67: :: QC_LANG4:67

for F being Element of QC-WFF
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 Th68: :: QC_LANG4:68

for F being Element of QC-WFF
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 Th69: :: QC_LANG4:69

for F being Element of QC-WFF
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:70

for F being Element of QC-WFF
for G2, G1 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2

proof end;

theorem Th71: :: QC_LANG4:71

for F being Element of QC-WFF
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:72

for F being Element of QC-WFF
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:73

for F being Element of QC-WFF
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:74

for F being Element of QC-WFF
for G2, G1 being Subformula of F st G2 is_subformula_of G1 holds
for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2

proof end;