DISP	partial_valuation_df	(<F:Formula:L> eval under <a:Assignment:L>) == (<F> eval under <a>)
ABS	partial_valuation	(F eval under a) == (letrec val f = case f: x case (a x): 3 (inl ff ); 3 (inr x ); 3 (inl tt );; p case val p of inl(b) => if b then inl ff else inl tt fi | inr(f) => inr f ; pq case val p of inl(b) => if b then val q else inl ff fi | inr(f) => case val q of inl(b) => if b then inr f else inl ff fi | inr(f') => inr ff' ; pq case val p of inl(b) => if b then inl tt else val q fi | inr(f) => case val q of inl(b) => if b then inl tt else inr f fi | inr(f') => inr ff' ; pq case val p of inl(b) => if b then val q else inl tt fi | inr(f) => case val q of inl(b) => if b then inl tt else inr f fi | inr(f') => inr ff' ; ) F
ML	partial_valuation_unroll	let get_formula_type_from_partial_valuation = fst o fst o dest_term o snd o hd o snd o dest_term ;; let partial_valuationC t = FwdMacroC (concat `partial_valuation_` (concat (get_formula_type_from_partial_valuation t) `_unrollC`)) (AllC [UnfoldC `partial_valuation`; letrec_unrollC; formula_case_unrollC; TryC (FoldC `partial_valuation`)]) t ;; let partial_valuation_unrollC = FirstC (map partial_valuationC [(x eval under a) ; (P eval under a) ; (PQ eval under a) ; (PQ eval under a) ; (PQ eval under a) ]) ;; add_AbReduce_conv `partial_valuation` partial_valuation_unrollC;;
THM	partial_valuation_wf	a:Assignment. f:Formula. (f eval under a) + Formula
DISP	lift_df	h(<x:pv:*>)== h(<x>)
ABS	lift	h(x) == case x of inl(b) => if b then 3 else 3 fi | inr(f) => 3
ML	lift_unroll	let lift_unroller t = FwdMacroC `lift_unrollC` (AllC [UnfoldC `lift`; ReduceC]) t ;; let lift_unrollC = SomeC[lift_unroller h(inl tt ); lift_unroller h(inl ff ); lift_unroller h(inr f )] ;; add_AbReduce_conv `lift` lift_unrollC;;
THM	lift_wf	x: + Formula. h(x)
THM	lift_true_lemma	a:Assignment. f:Formula. h((f eval under a) ) = 3 (f eval under a) = (inl tt )
THM	lift_false_lemma	a:Assignment. f:Formula. h((f eval under a) ) = 3 (f eval under a) = (inl ff )
THM	lift_undecided_lemma	a:Assignment. f:Formula. h((f eval under a) ) = 3 (f':Formula. (f eval under a) = (inr f' ))
THM	partial_valuation_correct	a:Assignment. f:Formula. h((f eval under a) ) = (f under a)

the other theories