[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Fri, 12 Feb 2016 17:04:11 +0100*References*: <79fff255-1912-451f-8fa7-b671618a3cfe@googlegroups.com> <E7288292-7600-4BF5-8F90-468DDA4C670F@gmail.com> <94b7cfa3-026a-4db2-9f2e-39f63cb7de3d@googlegroups.com>

Hi Ron,
there is nothing to prove: the right-hand side corresponds to an inductive definition of a primitive-recursive function where the initial value of h is h0 and at every step, the new value of h is computed as a function of the visible variables v and the previous value of h. (To be completely precise, I'm assuming that h does not occur in Init, Next or h0 and that h' does not occur in f(h,v).)
I'll send you a rough draft off-list. Stephan |

**References**:**Correctness of refinement mapping***From:*Ron Pressler

**Re: [tlaplus] Correctness of refinement mapping***From:*Stephan Merz

**Re: [tlaplus] Correctness of refinement mapping***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] Correctness of refinement mapping** - Next by Date:
**alternative spec. langs compiling to TLA+** - Previous by thread:
**Re: [tlaplus] Correctness of refinement mapping** - Next by thread:
**alternative spec. langs compiling to TLA+** - Index(es):