fact: Fixpoint di2 (st : nat) : BV -> BV -> BV -> Memo -> BV -> BV -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) (ad0 da0 : BV) => match st return BV with | O => di0 | S t => match IsNull (cx2 t di0 cx0 al0 mem0 ad0 da0) return BV with | true => di2 t di0 cx0 al0 mem0 ad0 da0 | false => di2 t di0 cx0 al0 mem0 ad0 da0 end end with cx2 (st : nat) : BV -> BV -> BV -> Memo -> BV -> BV -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) (ad0 da0 : BV) => match st return BV with | O => cx0 | S t => match IsNull (cx2 t di0 cx0 al0 mem0 ad0 da0) return BV with | true => cx2 t di0 cx0 al0 mem0 ad0 da0 | false => BV_decrement (cx2 t di0 cx0 al0 mem0 ad0 da0) end end with al2 (st : nat) : BV -> BV -> BV -> Memo -> BV -> BV -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) (ad0 da0 : BV) => match st return BV with | O => al0 | S t => match IsNull (cx2 t di0 cx0 al0 mem0 ad0 da0) return BV with | true => al2 t di0 cx0 al0 mem0 ad0 da0 | false => al2 t di0 cx0 al0 mem0 ad0 da0 end end with mem2 (st : nat) : BV -> BV -> BV -> Memo -> BV -> BV -> Memo := fun (di0 cx0 al0 : BV) (mem0 : Memo) (ad0 da0 : BV) => match st return Memo with | O => mem0 | S t => match IsNull (cx2 t di0 cx0 al0 mem0 ad0 da0) return Memo with | true => mem2 t di0 cx0 al0 mem0 ad0 da0 | false => MemoWrite (mem2 t di0 cx0 al0 mem0 ad0 da0) (BV_to_nat (ad2 t di0 cx0 al0 mem0 ad0 da0)) (da2 t di0 cx0 al0 mem0 ad0 da0) end end with ad2 (st : nat) : BV -> BV -> BV -> Memo -> BV -> BV -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) (ad0 da0 : BV) => match st return BV with | O => ad0 | S t => match IsNull (cx2 t di0 cx0 al0 mem0 ad0 da0) return BV with | true => ad2 t di0 cx0 al0 mem0 ad0 da0 | false => BV_increment (ad2 t di0 cx0 al0 mem0 ad0 da0) end end with da2 (st : nat) : BV -> BV -> BV -> Memo -> BV -> BV -> BV := fun (di0 cx0 al0 : BV) (mem0 : Memo) (ad0 da0 : BV) => match st return BV with | O => da0 | S t => match IsNull (cx2 t di0 cx0 al0 mem0 ad0 da0) return BV with | true => da2 t di0 cx0 al0 mem0 ad0 da0 | false => da2 t di0 cx0 al0 mem0 ad0 da0 end end.
imports: Fill_defs