Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof resit / 7 / a

Reading the abstract syntax tree recursively gives the eight distinct subformulasA subformula includes the complete propositional formula itself as well as the operands of its connectives. There are nine occurrences in the abstract syntax tree, because the atomic formula $A$ occurs twice, but only eight different propositional formulas in the set.