:: The Subformula Tree of a Formula of the First Order Language
:: by Oleg Okhotnikov
::
:: 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)
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 ;

definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
func list_of_immediate_constituents p -> FinSequence of QC-WFF A equals :Def1: :: QC_LANG4:def 1
<*> () if ( p = VERUM A or p is atomic )
if p is negative
if p is conjunctive
otherwise <*()*>;
coherence
( ( ( p = VERUM A or p is atomic ) implies <*> () is FinSequence of QC-WFF A ) & ( p is negative implies is FinSequence of QC-WFF A ) & ( p is conjunctive implies is FinSequence of QC-WFF A ) & ( p = VERUM A or p is atomic or p is negative or p is conjunctive or <*()*> is FinSequence of QC-WFF A ) )
;
consistency
for b1 being FinSequence of QC-WFF A holds
( ( ( p = VERUM A or p is atomic ) & p is negative implies ( b1 = <*> () iff b1 = ) ) & ( ( p = VERUM A or p is atomic ) & p is conjunctive implies ( b1 = <*> () iff b1 = ) ) & ( p is negative & p is conjunctive implies ( b1 = iff b1 = ) ) )
by QC_LANG1:20;
end;

:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def 1 :
for A being QC-alphabet
for p being Element of QC-WFF A holds
( ( ( p = VERUM A or p is atomic ) implies list_of_immediate_constituents p = <*> () ) & ( p is negative implies list_of_immediate_constituents p = ) & ( p is conjunctive implies list_of_immediate_constituents p = ) & ( p = VERUM A or p is atomic or p is negative or p is conjunctive or list_of_immediate_constituents 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 & G = . 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 = { 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;
func tree_of_subformulae p -> finite DecoratedTree of QC-WFF A means :Def2: :: QC_LANG4:def 2
( it . {} = p & ( for x being Element of dom it holds succ (it,x) = list_of_immediate_constituents (it . x) ) );
existence
ex b1 being finite DecoratedTree of QC-WFF A st
( b1 . {} = p & ( for x being Element of dom b1 holds succ (b1,x) = list_of_immediate_constituents (b1 . x) ) )
proof end;
uniqueness
for b1, b2 being finite DecoratedTree of QC-WFF A st b1 . {} = p & ( for x being Element of dom b1 holds succ (b1,x) = list_of_immediate_constituents (b1 . x) ) & b2 . {} = p & ( for x being Element of dom b2 holds succ (b2,x) = list_of_immediate_constituents (b2 . x) ) holds
b1 = b2
proof end;
end;

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

theorem Th5: :: QC_LANG4:5
for A being QC-alphabet
for F being Element of QC-WFF A holds F in rng
proof end;

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 st t ^ <*n*> in dom holds
ex G being Element of QC-WFF A st
( G = . (t ^ <*n*>) & G is_immediate_constituent_of . 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 holds
( H is_immediate_constituent_of . t iff ex n being Nat st
( t ^ <*n*> in dom & H = . (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 & H is_immediate_constituent_of G holds
H in rng
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 & H is_subformula_of G holds
H in rng
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 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 = 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 st t9 in succ t holds
. t9 is_immediate_constituent_of . 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 st t is_a_prefix_of t9 holds
. t9 is_subformula_of . 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 st t is_a_proper_prefix_of t9 holds
len (@ ( . t9)) < len (@ ( . 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 st t is_a_proper_prefix_of t9 holds
. t9 <> . 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 st t is_a_proper_prefix_of t9 holds
. t9 is_proper_subformula_of . 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 holds
( . 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 st t <> t9 & . t = . 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;
func F -entry_points_in_subformula_tree_of G -> AntiChain_of_Prefixes of dom means :Def3: :: QC_LANG4:def 3
for t being Element of dom holds
( t in it iff . t = G );
existence
ex b1 being AntiChain_of_Prefixes of dom st
for t being Element of dom holds
( t in b1 iff . t = G )
proof end;
uniqueness
for b1, b2 being AntiChain_of_Prefixes of dom st ( for t being Element of dom holds
( t in b1 iff . t = G ) ) & ( for t being Element of dom holds
( t in b2 iff . t = G ) ) holds
b1 = b2
proof end;
end;

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

theorem Th19: :: QC_LANG4:19
for A being QC-alphabet
for F, G being Element of QC-WFF A holds F -entry_points_in_subformula_tree_of G = { t where t is Element of dom : . 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 <> {} )
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 st t9 = t ^ <*m*> & . t is negative holds
( . t9 = the_argument_of ( . 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 st t9 = t ^ <*m*> & . t is conjunctive & not ( . t9 = the_left_argument_of ( . t) & m = 0 ) holds
( . t9 = the_right_argument_of ( . 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 st t9 = t ^ <*m*> & . t is universal holds
( . t9 = the_scope_of ( . 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 st . t is negative holds
( t ^ in dom & . () = the_argument_of ( . 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 st . t is conjunctive holds
( t ^ in dom & . () = the_left_argument_of ( . t) & t ^ <*1*> in dom & . (t ^ <*1*>) = the_right_argument_of ( . 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 st . t is universal holds
( t ^ in dom & . () = the_scope_of ( . 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
for s being Element of dom 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
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 , s is Element of dom : ( 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 holds | t = tree_of_subformulae ( . 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 holds
( t in F -entry_points_in_subformula_tree_of G iff | 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 : | 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 st G in { ( . t) where t is Element of dom : t in C } & H in { ( . t) where t is Element of dom : 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;
mode Subformula of F -> Element of QC-WFF A means :Def4: :: QC_LANG4:def 4
it is_subformula_of F;
existence
ex b1 being Element of QC-WFF A st b1 is_subformula_of F
;
end;

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

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
let G be Subformula of F;
mode Entry_Point_in_Subformula_Tree of G -> Element of dom means :Def5: :: QC_LANG4:def 5
. it = G;
existence
ex b1 being Element of dom st . b1 = G
proof end;
end;

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

theorem :: QC_LANG4:34
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F
for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
proof end;

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
let G be Subformula of F;
coherence by ;
end;

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

theorem Th35: :: QC_LANG4:35
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F
for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G
proof end;

theorem Th36: :: QC_LANG4:36
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F holds entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
proof 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 () 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
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 () : s in G1 -entry_points_in_subformula_tree_of G2 } = { (t ^ s) where t is Element of dom , s is Element of dom () : ( 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 () : 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
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
proof end;