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 A1:
( t' = t ^ <*m*> & (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 ) )
A2:
succ (tree_of_subformulae F),t = list_of_immediate_constituents ((tree_of_subformulae F) . t)
by Def2;
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 A1, Def1;
consider q being Element of dom (tree_of_subformulae F) such that
A4:
( q = t & succ (tree_of_subformulae F),t = (tree_of_subformulae F) * (q succ ) )
by TREES_9:def 6;
dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ )
by A2, A3, A4, Th10;
then A5:
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;
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
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;
then A6:
( m + 1 = 0 + 1 or m + 1 = 1 + 1 )
by A5, FINSEQ_1:4, TARSKI:def 2;