This project is read-only.
1
Vote

12-10-05_1 : named instantiations with parameters

description

Another bug reported by Tom Rodeheffer: the PM doesn't handle named instantiations.

Modules Prop and InstanceBug are accepted by SANY, but the PM throws an
exception when trying to prove theorem DoubleOne.

-------------------------------- MODULE Prop --------------------------------
EXTENDS Naturals, TLAPS

CONSTANT n
ASSUME InNat == n \in Nat

THEOREM TwoN == 2*n \in Nat
BY InNat

=============================================

---------------------------- MODULE InstanceBug ----------------------------
EXTENDS Naturals, TLAPS

P(n) == INSTANCE Prop

THEOREM DoubleOne == P(1)!TwoN
BY SMT

==============================================

file attachments

comments

MartinRie wrote Jan 19, 2015 at 3:21 PM

Confirmed at 2015-01-19