ITree Program Logic