reverse of multi_R in context

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring

11 stars 6 forks source link

reverse of multi_R in context #138

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

1 subgoals
t1 : tm
t2 : tm
t2' : tm
H : value t1
H0 : t2 ==>* t2'
______________________________________(1/1)
t2 ==> t2'

I want to apply the reverse of multi_R to H0 in the context, does something like that exist?

jaewooklee93 commented 9 years ago

No, I think it's impossible. There is a case t2 = t2' (#step = 0) under the condition of t2 ==>* t2' (#step ∈ Nat) , but then t2 ==> t2' (#step = 1) cannot be true.

AdamBJ commented 9 years ago

Ok, I'll stick with induction for that question then, thanks.