a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březina(pred y : bb)

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březina(pred y : bb * bb)

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březina(pred y : bb * bb)(a, b)

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 4, column 1) expected further mixfix token: [":","!","*","+","-"]

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 5, column 7) unexpected mixfix token: <

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 6, column 3) unexpected mixfix token: #=

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 7, column 10) unexpected mixfix token: predy

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 7, column 1) unexpected mixfix token: exists1

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaexists predy:bb . a

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaexists! a:v . x

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaexists! a:v . x

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaexists! a:v . x

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaforall a:v . x

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinab => a

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinadef x

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 15, column 4) unexpected mixfix token: #

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 16, column 2) unexpected mixfix token: }

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel BřezinaError (line 16, column 3) not a formula: {} when [] else {}

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa /\ b /\ c

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa \/ b \/ c

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa => b

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa <=> b

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinatrue

7f0b01bf0a8f5c5b3ef145e81511b6db2cb4f98fPavel Březinafalse

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinab in s

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa =e= b

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa = b

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa => b => c => d

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinad => c => b => a

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinaa <=> b

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinadef d => not c => b \/ c => a /\ b

a1e4113a5388e34c08459c5b69679c82ac2bddc9Pavel Březinam div n = r <=> exists s:Nat . m = n * r + s /\ s < n

132e477d69e07e02fe6e4d668c0bb6226206474aPavel Březina