let A be QC-alphabet ; :: thesis: 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) )
let F be Element of QC-WFF A; :: thesis: 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) )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( (tree_of_subformulae F) . t is conjunctive implies ( 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) ) )
set G = (tree_of_subformulae F) . t;
assume A1: (tree_of_subformulae F) . t is conjunctive ; :: thesis: ( 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) )
(tree_of_subformulae F) * (t succ) = succ ((tree_of_subformulae F),t)
proof
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;
hence (tree_of_subformulae F) * (t succ) = succ ((tree_of_subformulae F),t) ; :: thesis: verum
end;
then A2: dom (t succ) = dom (succ ((tree_of_subformulae F),t)) by TREES_9:37
.= dom (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Def2
.= dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A1, Def1
.= {1,2} by Lm1, FINSEQ_1:2 ;
A3: 0 + 1 in {1,2} by TARSKI:def 2;
then t ^ <*0*> in dom (tree_of_subformulae F) by A2, TREES_9:39;
then (tree_of_subformulae F) . (t ^ <*0*>) = (succ ((tree_of_subformulae F),t)) . (0 + 1) by TREES_9:40
.= (list_of_immediate_constituents ((tree_of_subformulae F) . t)) . 1 by Def2
.= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 1 by A1, Def1
.= the_left_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:44 ;
hence ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) ) by A2, A3, TREES_9:39; :: thesis: ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
A4: 1 + 1 in {1,2} by TARSKI:def 2;
then t ^ <*1*> in dom (tree_of_subformulae F) by A2, TREES_9:39;
then (tree_of_subformulae F) . (t ^ <*1*>) = (succ ((tree_of_subformulae F),t)) . (1 + 1) by TREES_9:40
.= (list_of_immediate_constituents ((tree_of_subformulae F) . t)) . 2 by Def2
.= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 2 by A1, Def1
.= the_right_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:44 ;
hence ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) ) by A2, A4, TREES_9:39; :: thesis: verum