search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Stuck #152

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

This seems provable, but I can't figure out how. Any ideas?

6 subgoal
a : nat
b : nat
c : nat
st : state
H1 : st Z - st Y = c + a
H2 : st Y = b
______________________________________(1/6)
st Z = c + a + b
jaewooklee93 commented 9 years ago 
st Z = 0
st Y = 1
a = 0
b = 1
c = 0

satisfy the assumption but don't satisfy the goal, so it is a counterexample