Data Conversion Method between a Natural Number and a Binary Tree for an Inductive Proof and Its Application

This paper presents modeling ofa binary tree that represents a natural numberand gives an inductive proof for its propertiesusing theorem provers.We define a function for converting data from a natural numberinto a binary treeand give an inductive proof for its well-definedness.We formalize this method, develop a computational model based on it,and apply it to an electronic cash protocol.We also define the payment function on the binary treeand go on to prove the divisibility of electronic cashusing the theorem provers Isabelle/HOL and Coq, respectively.Furthermore, we discuss the effectiveness of this method.