4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder(pred y : bb)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder(pred y : bb*bb)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder(pred y : bb*bb)(a,b)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder(pred y : bb*bb) a b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera =e= < b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera #=e= b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederexists1 (predy :: bb)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederexists predy : bb . a

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederexists! a: v . x

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederexists!a:v.x

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederexists! a :v.x

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederforall a: v . x

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera if b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdef x

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdef#

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{}when[]else{}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera/\b/\c

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera\/b\/c

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera=>b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera<=>b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertrue

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederfalse

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederb in s

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera =e= b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder(a = b)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera=>b=>c=>d

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera if b if c if d

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera<=>b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera/\b if b\/c if not c if def d

f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maederm div n = r <=>(exists s: Nat . m = n*r + s /\ s < n)

88d75e7bf413b86d54dcb8307cb27b51c3fa494dChristian Maedera => (b if c)

88d75e7bf413b86d54dcb8307cb27b51c3fa494dChristian Maedera if (b => c)

88d75e7bf413b86d54dcb8307cb27b51c3fa494dChristian Maeder(a => b) if c

88d75e7bf413b86d54dcb8307cb27b51c3fa494dChristian Maeder(a if b) => c