fact: Fixpoint di (st : nat) : BV -> BV -> BV -> Memo -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) => match st return BV with | O => di0 | S t => match IsNull (cx t di0 cx0 al0 mem0) return BV with | true => di t di0 cx0 al0 mem0 | false => BV_increment (di t di0 cx0 al0 mem0) end end with cx (st : nat) : BV -> BV -> BV -> Memo -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) => match st return BV with | O => cx0 | S t => match IsNull (cx t di0 cx0 al0 mem0) return BV with | true => cx t di0 cx0 al0 mem0 | false => BV_decrement (cx t di0 cx0 al0 mem0) end end with al (st : nat) : BV -> BV -> BV -> Memo -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) => match st return BV with | O => al0 | S t => match IsNull (cx t di0 cx0 al0 mem0) return BV with | true => al t di0 cx0 al0 mem0 | false => al t di0 cx0 al0 mem0 end end with mem (st : nat) : BV -> BV -> BV -> Memo -> Memo := fun (di0 cx0 al0 : BV) (mem0 : Memo) => match st return Memo with | O => mem0 | S t => match IsNull (cx t di0 cx0 al0 mem0) return Memo with | true => mem t di0 cx0 al0 mem0 | false => MemoWrite (mem t di0 cx0 al0 mem0) (BV_to_nat (di t di0 cx0 al0 mem0)) (al t di0 cx0 al0 mem0) end end.
imports: Fill_defs