search

Ayertienna / IS5

Intuitionistic S5 logic formalization
4 stars 0 forks source link

Proofs for substitution properties - label-free #4

Closed Ayertienna closed 12 years ago

Ayertienna commented 12 years ago

At least the sketches of these are required to close (for now) the language definition part. It is still ok to Admitt or skip some trivial properties of ok_Bg, emptyEquiv and permut, as long as there is an informal sketch in the comment.

Ayertienna commented 12 years ago

subst_order_irrelevant is finished - which means that the only skips in proof of subst_t_preserv_types are ok_Bg-related.

Ayertienna commented 12 years ago

This is actually finished, if you count only language (not implementation) lemmas as relevant