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.