#lang racket
;; Starter code for A4Q1
;; May contain Unicode characters - download, don't cut/paste from browser

;; Here is the grammar for formulas or expressions in propositional logic,
;; represented as fully-parenthesized S-expressions.

;; expr = X [not ⊥]
;;      | (T -> T)
;;      | (T ∧ T)
;;      | (T ∨ T)
;;      | (¬ T)

;; Example: the formula for LEM is '(A ∨ (¬ A)).

;; A Kripke model (km) is an S-expression that satisfies the following grammar:
;; km = (symbol [var ...] km ...)
;; The symbol is the root label,
;; the list of variables are the ones forced at this node,
;; and the rest of the list is the children of the root.

;; Example:
;; s  O  A
;;    |
;; r  O
;;
;; is:

; (define ex1 '(r [] (s [A])))

;; Your task is to implement the following two functions.

;; The valid? function checks the monotonicity condition (every variable in the root list of a Kripke model
;; must appear in the root lists of its descendants) and that ⊥ is not used as a variable.

;; valid? : km -> boolean


;; We want to know whether or not a given formula is forced at the root of a valid Kripke model.

;; forced-at? : expr km -> boolean