Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >
-->

Examplessmall logo



Examples -> ExternalSimplification -> agm.prf


2 [] x<=y|y<=x.
3 [] -(x<=y)| -(u<=v)|x+u<=y+v.
4 [] 0<=a.
5 [] 0<=b.
6 [] -(0<=x)| -(x<=y)|x^2<=y^2.
8 [] a!=b.
9 [] -(sqrt(a*b)< (a+b)/2).
10 [simplify,9] a+b<=2* (a*b)^ (1/2).
12 [hyper,10,6,2,simplify,unit_del,8] a<= -b.
20 [hyper,12,3,5,simplify] a<=0.
21 [hyper,12,3,4,simplify] b<=0.
23 [hyper,20,6,4,simplify] a=0.
29 [hyper,21,6,5,simplify] b=0.
41 [para_into,29,23] b=a.
49 [para_into,41,29] 0=a.
50 [para_into,49,41] 0=b.
51 [para_into,50,49] a=b.
52 [binary,51,8] $F.