Hi,
I'm trying to prove all elements in a sub sequence is nonnull if all elements in the original sequence is nonnull. Here is the program.
http://rise4fun.com/Dafny/T8M
I realize that the same property can be proved on sets since the relations of subsets form a lattice in Dafny.
My question is what is the right way to prove the same property on sub sequences?
Thanks!
