Fder = Fslems + consts fill_valid, fill_ed :: "structr rule set" (* should be fill-valid for forward proof except when applied to a sequent which already contains an exclusion *) inductive "fill_ed" intrs dps "r : rulefs {drp, rp, invert rp} ==> r : fill_ed" bsrbs "r : rulefs bsrbs ==> r : fill_ed" ibsrbs "r : rulefs (invert ` bsrbs) ==> r : fill_ed" bsrus "r : rulefs bsrus ==> r : fill_ed" commaL "ALL W. ([$W |- $H], $W |- $C) : fill_ed ==> ([$W |- $U,, $H], $W |- $U,, $C) : fill_ed" commaR "ALL W. ([$W |- $H], $W |- $C) : fill_ed ==> ([$W |- $H,, $U], $W |- $C,, $U) : fill_ed" inductive "fill_valid" intrs ffilldc "r : rulefs ffilldc ==> r : fill_valid" tauS "tau_ok True Y ==> ([$W |- $Y], $W |- tau True Y) : fill_valid" tauA "tau_ok False Y ==> ([$Y |- $W], tau False Y |- $W) : fill_valid" end