B: The expression cons( x, y ) denotes the list formed by inserting the element x at the head of the list y. We denote the empty list by NIL; the list (2) by cons(2, NIL); the list , 2) by cons(1, cons(2, NIL)); etc. The expression LAST( x, y) is intended to mean that y is the last element of the list x. We have the following axioms (Vu) LAST(cons(u, NIL), u) (Vx) (Vy) (Vz)[ LAST(y, z) - LAST(cons(x, y), 2)] (B1) Prove the following theorem from these axioms by the method of resolution (av) LAST (cons(2,cons(1, NIL)), v) (B2) Use answer extraction to find v, the last element of the list 2. 1 (B3) Describe briefly how this method might be used to compute the last element of longer lists B: The expression cons( x, y ) denotes the list formed by inserting the element x at the head of the list y. We denote the empty list by NIL; the list (2) by cons(2, NIL); the list , 2) by cons(1, cons(2, NIL)); etc. The expression LAST( x, y) is intended to mean that y is the last element of the list x. We have the following axioms (Vu) LAST(cons(u, NIL), u) (Vx) (Vy) (Vz)[ LAST(y, z) - LAST(cons(x, y), 2)] (B1) Prove the following theorem from these axioms by the method of resolution (av) LAST (cons(2,cons(1, NIL)), v) (B2) Use answer extraction to find v, the last element of the list 2. 1 (B3) Describe briefly how this method might be used to compute the last element of longer lists