Re: [tlaplus] Missing theorem

[fl <freder...@xxxxxxxxxxx>]

 

If you need the definition of S further down in the proof, you may prefer the variant

<4>1. J \in Nat

<4>. DEFINE S == ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) )

<4>2. seq \in [ 1 .. J ->  S]

<4>3. seq \in Seq(S)

  <5>. HIDE DEF S

  <5>. QED  BY <4>1, <4>2

 

 

 

I've used this variant and thank you it works.

 

--

FL