fact: Definition intro_state (st:state) (f: LForm) (hf: HFormula) := let (hs,c) := intro_impl nil f hf in match cnf_hyps (is_classic c) hs st with | Fail f => Fail f | Success p => Success p | Progress st => match c with | None => Progress(st,None) | Some g => match augment_cnf false (NEG g) st with | Fail f => Fail f | Success p => Success p | Progress st' => Progress(st',Some g) end end end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause