發送短信 : Theorem Proving in Higher Order Logics

 _    _     ______    ____     __   __  __    __  
| || | ||  /_   _//  |  _ \\   \ \\/ // \ \\ / // 
| || | ||   -| ||-   | |_| ||   \ ` //   \ \/ //  
| \\_/ ||   _| ||_   | .  //     | ||     \  //   
 \____//   /_____//  |_|\_\\     |_||      \//    
  `---`    `-----`   `-` --`     `-`'       `