fact: Fixpoint simplify' t p := match t with | Ttrue => Ttrue | Tfalse => Tfalse | Ttree cnj l r => match simplify' l p, cnj, simplify' r p with | Ttrue, true, r => r | Ttrue, false, _ => Ttrue | Tfalse, true, _ => Tfalse | Tfalse, false, r => r | l, true, Ttrue => l | _, true, Tfalse => Tfalse | l, true, r => Ttree true l r | _, false, Ttrue => Ttrue | l, false, Tfalse => l | l, false, r => Ttree false l r end | Tatom pos a => match relate p a pos with | ARimply => Ttrue | ARcontradict => Tfalse | ARunknown => t end end.
imports: Reals List Bool Gappa_common