let m be Element of NAT ; :: thesis: for F being Element of QC-WFF
for t', t being Element of dom (tree_of_subformulae F) st t' = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t' = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t' = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
let F be Element of QC-WFF ; :: thesis: for t', t being Element of dom (tree_of_subformulae F) st t' = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t' = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t' = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
let t', t be Element of dom (tree_of_subformulae F); :: thesis: ( t' = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t' = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) implies ( (tree_of_subformulae F) . t' = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t';
assume that
A1:
t' = t ^ <*m*>
and
A2:
(tree_of_subformulae F) . t is conjunctive
; :: thesis: ( ( (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 ) )
A3:
list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*>
by A2, Def1;
len <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = 2
by FINSEQ_1:61;
then A4:
dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = Seg 2
by FINSEQ_1:def 3;
A5:
succ (tree_of_subformulae F),t = list_of_immediate_constituents ((tree_of_subformulae F) . t)
by Def2;
ex q being 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 ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ )
by A5, A3, Th10;
then
m + 1 in dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*>
by A1, Th12;
then A6:
( m + 1 = 0 + 1 or m + 1 = 1 + 1 )
by A4, FINSEQ_1:4, TARSKI:def 2;