1 00:00:02,700 --> 00:00:06,100 We want to simplify this formula. 2 00:00:06,110 --> 00:00:08,600 We can assume the formulas in the frame context. 3 00:00:08,600 --> 00:00:14,700 Let us apply the SimplifyAuto tactic. 4 00:00:14,700 --> 00:00:20,400 The SimplifyAuto tactic recursively simplifies the subformulas. 5 00:00:20,400 --> 00:00:25,100 Tactic application successful. We get a simpler formula. 6 00:00:25,100 --> 00:00:35,550 Let us see the proof information. 7 00:00:35,550 --> 00:00:40,450 Three theorem provers have been tried to discharge this proof obligation. 8 00:00:48,350 --> 00:00:53,300 This proof obligation has been discharged successfully by Alt-Ergo. 9 00:01:12,300 --> 00:01:17,700 In one step, we got a much simpler formula.