let p be MP-variable; :: thesis:
let A, B be MP-wff; :: thesis:
set e0 = elementary_tree 0 ;
set e1 = elementary_tree 1;
set e2 = elementary_tree 2;
A1: dom (@ p) = elementary_tree 0 by FUNCOP_1:19;
A2: <*0 *> in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
A3: ( dom ((elementary_tree 1) --> [1,0 ]) = elementary_tree 1 & dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 ) by FUNCOP_1:19;
then dom ('not' A) = (elementary_tree 1) with-replacement <*0 *>,(dom A) by A2, TREES_2:def 12;
then <*0 *> in dom ('not' A) by A2, TREES_1:def 12;
hence @ p <> 'not' A by A1, TARSKI:def 1, TREES_1:56; :: thesis:
dom ((#) A) = (elementary_tree 1) with-replacement <*0 *>,(dom A) by A2, A3, TREES_2:def 12;
then <*0 *> in dom ((#) A) by A2, TREES_1:def 12;
hence @ p <> (#) A by A1, TARSKI:def 1, TREES_1:56; :: thesis:
set y = ((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A;
A4: ( <*0 *> in elementary_tree 2 & <*1*> in elementary_tree 2 ) by TREES_1:55;
A5: dom ((elementary_tree 2) --> [2,0 ]) = elementary_tree 2 by FUNCOP_1:19;
then A6: dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) = (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*0 *>,(dom A) by A4, TREES_2:def 12;
not <*0 *> is_a_proper_prefix_of <*1*> by TREES_1:89;
then A7: <*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A) by A4, A5, A6, TREES_1:def 12;
then dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,A)) with-replacement <*1*>,(dom B) by TREES_2:def 12;
then <*1*> in dom (A '&' B) by A7, TREES_1:def 12;
hence @ p <> A '&' B by A1, TARSKI:def 1, TREES_1:56; :: thesis: