DISP	Formula_df	Formula== Formula
ABS	Formula	Formula == rec(formula.Var + formula + formula formula + formula formula + formula formula)
THM	Formula_wf	Formula
ML	RecMemberFormulaCD	let RecMemberFormulaCD = Unfolds ``Formula member`` 0 THEN RecTypeEqTypeCD THEN Try (Fold `Formula` 0) ;;
DISP	formula_case_df	{[SOFT}case{->0} <F:Formula:L>:{\\}<y:Var> <c1:Var case:L>{\\} <p1:P> <c2:case:L>{\\}<p2:Conjunct 1><p3:Conjunct 2> <c3: case:L>{\\}<p4:disjunct 1><p5: disjunct 2> <c4: case:L> ;{\\}<p6:Antecedent><p7:Consequent> <c5:case:L>{<-}{]} == case <F>: <y> <c1> <p1> <c2> <p2><p3> <c3> <p4><p5> <c4> <p6><p7> <c5>
ABS	formula_case	case F: x varC[x]; p1 notC[p1]; p2p3 andC[p2; p3]; p4p5 orC[p4; p5]; p6p7 impC[p6; p7]; == case F of inl(x) => varC[x] | inr(F) => case F of inl(p1) => notC[p1] | inr(F) => case F of inl(x) => let <p2,p3> = x in andC[p2; p3] | inr(F) => case F of inl(x) => let <p4,p5> = x in orC[p4; p5] | inr(x) => let <p6,p7> = x in impC[p6; p7]
DISP	fvar_df	<x:Var:L>== <x>
ABS	fvar	F == inl F
THM	fvar_wf	x:Var. x Formula
THM	comb_for_fvar_wf	(x,z.x) x:Var True Formula
DISP	fnot_df	<p:Formula:L>== <p>
ABS	fnot	p == inr (inl p )
THM	fnot_wf	x:Formula. x Formula
THM	comb_for_fnot_wf	(x,z.x) x:Formula True Formula
DISP	fand_df	<p:Formula:L><q:Formula:*>== <p><q>
ABS	fand	pq == inr inr (inl <p, q> )
THM	fand_wf	p,q:Formula. pq Formula
THM	comb_for_fand_wf	(p,q,z.pq) p:Formula q:Formula True Formula
DISP	for_df	<p:Formula:L><q:Formula:L>== <p><q>
ABS	for	pq == inr inr inr (inl <p, q> )
THM	for_wf	p,q:Formula. pq Formula
THM	comb_for_for_wf	(p,q,z.pq) p:Formula q:Formula True Formula
DISP	fimp_df	<p:Formula:L><q:Formula:L>== <p><q>
ABS	fimp	pq == inr inr inr inr <p, q>
THM	fimp_wf	p,q:Formula. pq Formula
THM	comb_for_fimp_wf	(p,q,z.pq) p:Formula q:Formula True Formula
ML	formula_case_unroll	let get_formula_case_arg = fst o fst o dest_term o snd o hd o snd o dest_term;; let formula_caseC t = let arg = (get_formula_case_arg t) in (FwdMacroC (concat `formula_case_` (concat arg `_unrollC`)) (AllC [UnfoldC `formula_case`; UnfoldC arg; ReduceC]) t) ;; let formula_case_unrollC = FirstC[formula_caseC case F: x X[x]; a A[a]; bc B[b; c]; de C[d; e]; fg D[f; g];; formula_caseC case F: x X[x]; a A[a]; bc B[b; c]; de C[d; e]; fg D[f; g];; formula_caseC case FFF: x X[x]; a A[a]; bc B[b; c]; de C[d; e]; fg D[f; g];; formula_caseC case FFF: x X[x]; a A[a]; bc B[b; c]; de C[d; e]; fg D[f; g];; formula_caseC case FFF: x X[x]; a A[a]; bc B[b; c]; de C[d; e]; fg D[f; g];] ;; add_AbReduce_conv `formula_case` formula_case_unrollC;;
ML	mk_formula_case_term	let mk_formula_case_term v (x,vcase) (p,not_case) (p1,q1,and_case) (p2,q2,or_case) (p3,q3,imp_case) = mk_ab_term (`formula_case`, []) [[],v;[x],vcase;[p],not_case; [p1;q1],and_case; [p2;q2],or_case;  [p3;q3],imp_case] ;;
DISP	subformula_df	subformula(<F:Formula:*>)== subformula(<F>)
ABS	subformula	subformula(F) == case F: x []; p (p::[]); pq (p::q::[]); pq (p::q::[]); pq (p::q::[]);
THM	subformula_wf	F:Formula. subformula(F) Formula List

the other theories