[tlaplus] How to prove RealInv' in the example "BubbleSort" ?

["cf Shi." <shichunfeng1314@xxxxxxxxx>]

Hello, 
I'm new in tlaps and trying to finish the example BubbleSort.tla[1]. But the attempt was invalid.  
I have no idea on it, and whether I handled it in a disorderly way? How to prove RealInv' in the example "BubbleSort" ?

My approach to this is as follows: (of course, this is predictably not working)


<2>2. RealInv'
    <3>1. CASE pc = "Lbl_1"
       BY DEF TypeOK, RealInv, Lbl_1,
              Lbl_2, IsSortedTo,IsSorted,IsSortedFromTo, IsPermOf, Perms, ** 
    <3>2. CASE pc = "Lbl_2"
    <3>3. CASE pc = "Done"
        BY IsPermOfExchange DEF TypeOK, RealInv, Lbl_1, Lbl_2,IsSortedTo,
                 IsSorted,IsSortedFromTo, IsPermOf, Perms, ** 
    <3>4. QED 
        BY <3>1,<3>2,<3>3 DEF TypeOK, RealInv, Lbl_1, Lbl_2  

-------------------------------------------------------------------------

[1] https://github.com/tlaplus/tlapm/blob/master/examples/BubbleSort.tla

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ee395ae0-b749-4f4e-9da0-611f91564424n%40googlegroups.com.