Lily

This case study concerns the metatheory of the linear Lily language.

It is incomplete; ask User:varming for updates.

In this example I will show examples of the following:

• Encoding of a linear type system.
• Definition of an abstract machine using evaluation frames.
• Correspondence between the big step semantics and the machine.
• Complete induction on the height of a derivation.

Lily - the language

Grammar

I define the grammar for the types

% Lily meta theory
% By Carsten Varming 2006
%sort tp %.
%name tp %.
%term func %pi tp %-> tp %-> tp %.
%term all %pi (%pi tp %-> tp) %-> tp %.
%term bang %pi tp %-> tp %.
%term i tp %.
%term tensor %pi tp %-> tp %-> tp %.
%freeze tp %.

and the grammar for the terms and values

%sort term %.
%name term %.
%term lam %pi tp %-> (%pi term %-> term) %-> term %.
%term app %pi term %-> term %-> term %.
%term tlam %pi (%pi tp %-> term) %-> term %.
%term tapp %pi term %-> tp %-> term %.
%term thunk %pi tp %-> (%pi term %-> term) %-> term %.
%term letb %pi term %-> (%pi term %-> term) %-> term %.
%term unit term %.
%term letu %pi term %-> term %-> term %.
%term tens %pi term %-> term %-> term %.
%term lett %pi term %-> (%pi term %-> term %-> term) %-> term %.
%freeze term %.
%sort value {_ term} %.
%mode value %in %.
%term val_lam value (lam _ _) %.
%term val_tlam value (tlam _) %.
%term val_thunk value (thunk _ _) %.
%term val_unit value unit %.
%term val_tens value (tens _ _) %.
%worlds () (value _) %.
%terminates {} (value _) %.
%freeze value %.

Next I define the call-by-name big step evaluation relation

%sort \n/ {_ term} {_ term} %.
%mode \n/ %in %out %.
%name \n/ %.
%prec %none 500 \n/ %.
%term ev_lam lam T M \n/ lam T M %.
%term ev_tlam tlam M \n/ tlam M %.
%term ev_thunk thunk T M \n/ thunk T M %.
%term ev_unit unit \n/ unit %.
%term ev_tens tens M N \n/ tens M N %.
%term ev_app %pi (app M N \n/ V) %<- (M \n/ lam _ M') %<- (M' N \n/ V) %.
%term ev_tapp %pi (tapp M T \n/ V) %<- (M \n/ tlam M') %<- (M' T \n/ V) %.
%term ev_letb %pi (letb M N \n/ V) %<- (M \n/ thunk T M') %<- (N (letb (thunk T M') M') \n/ V) %.
%term ev_letu %pi (letu M N \n/ V) %<- (M \n/ unit) %<- (N \n/ V) %.
%term ev_lett %pi (lett M N \n/ V) %<- (M \n/ tens M' M'') %<- (N M' M'' \n/ V) %.
%worlds () (\n/ _ _) %.
%covers \n/ %in %out %.
%freeze \n/ %.
%sort \/ {_ term} %.
%prec %postfix 500 \/ %.
%mode \/ %in %.
%term terminate %pi (M \/) %<- (M \n/ V) %.
%freeze \/ %.

I also have an strict (call-by-value) evaluation relation for Lily.

%sort \s/ {_ term} {_ term} %.
%mode \s/ %in %out %.
%name \s/ %.
%prec %none 500 \s/ %.
%term evs_lam lam T M \s/ lam T M %.
%term evs_tlam tlam M \s/ tlam M %.
%term evs_thunk thunk T M \s/ thunk T M %.
%term evs_unit unit \s/ unit %.
%term evs_tens tens M N \s/ tens M N %.
%term evs_app %pi (app M N \s/ V) %<- (M \s/ lam _ M') %<- (N \s/ V') %<- (M' V' \s/ V) %.
%term evs_tapp %pi (tapp M T \s/ V) %<- (M \s/ tlam M') %<- (M' T \s/ V) %.
%term evs_letb %pi (letb M N \s/ V) %<- (M \s/ thunk T M') %<- (N (letb (thunk T M') M') \s/ V) %.
%term evs_letu %pi (letu M N \s/ V) %<- (M \s/ unit) %<- (N \s/ V) %.
%term evs_lett %pi (lett M N \s/ V) %<- (M \s/ tens M' M'') %<- (N M' M'' \s/ V) %.
%worlds () (\s/ _ _) %.
%covers \s/ %in %out %.
%freeze \s/ %.

Value soundness

By now I can prove value soundness for the two evaluation relations.

%sort value_soundness {_ M \n/ V} {_ value V} %.
%mode value_soundness %in %out %.
%term vs_lam value_soundness ev_lam val_lam %.
%term vs_tlam value_soundness ev_tlam val_tlam %.
%term vs_thunk value_soundness ev_thunk val_thunk %.
%term vs_unit value_soundness ev_unit val_unit %.
%term vs_tens value_soundness ev_tens val_tens %.
%term vs_app %pi (value_soundness (ev_app D' _) V) %<- (value_soundness D' V) %.
%term vs_tapp %pi (value_soundness (ev_tapp D' _) V) %<- (value_soundness D' V) %.
%term vs_letb %pi (value_soundness (ev_letb D' _) V) %<- (value_soundness D' V) %.
%term vs_letu %pi (value_soundness (ev_letu D' _) V) %<- (value_soundness D' V) %.
%term vs_lett %pi (value_soundness (ev_lett D' _) V) %<- (value_soundness D' V) %.
%worlds () (value_soundness _ _) %.
%freeze value_soundness %.
%total D (value_soundness D _) %.
%sort value_soundness_s {_ M \s/ V} {_ value V} %.
%mode value_soundness_s %in %out %.
%term vs_lam value_soundness_s evs_lam val_lam %.
%term vs_tlam value_soundness_s evs_tlam val_tlam %.
%term vs_thunk value_soundness_s evs_thunk val_thunk %.
%term vs_unit value_soundness_s evs_unit val_unit %.
%term vs_tens value_soundness_s evs_tens val_tens %.
%term vs_app %pi (value_soundness_s (evs_app D' _ _) V) %<- (value_soundness_s D' V) %.
%term vs_tapp %pi (value_soundness_s (evs_tapp D' _) V) %<- (value_soundness_s D' V) %.
%term vs_letb %pi (value_soundness_s (evs_letb D' _) V) %<- (value_soundness_s D' V) %.
%term vs_letu %pi (value_soundness_s (evs_letu D' _) V) %<- (value_soundness_s D' V) %.
%term vs_lett %pi (value_soundness_s (evs_lett D' _) V) %<- (value_soundness_s D' V) %.
%worlds () (value_soundness_s _ _) %.
%freeze value_soundness_s %.
%total D (value_soundness_s D _) %.

It is also neat to know that values evaluate to themselves.

%sort selfeval {_ value V} {_ V \n/ V} %.
%mode selfeval %in %out %.
%term selfeval_lam selfeval val_lam ev_lam %.
%term selfeval_tlam selfeval val_tlam ev_tlam %.
%term selfeval_thunk selfeval val_thunk ev_thunk %.
%term selfeval_tens selfeval val_tens ev_tens %.
%term selfeval_unit selfeval val_unit ev_unit %.
%worlds () (selfeval _ _) %.
%freeze selfeval %.
%total V (selfeval V _) %.
%sort selfevals {_ value V} {_ V \s/ V} %.
%mode selfevals %in %out %.
%term selfevals_lam selfevals val_lam evs_lam %.
%term selfevals_tlam selfevals val_tlam evs_tlam %.
%term selfevals_thunk selfevals val_thunk evs_thunk %.
%term selfevals_tens selfevals val_tens evs_tens %.
%term selfevals_unit selfevals val_unit evs_unit %.
%worlds () (selfevals _ _) %.
%freeze selfevals %.
%total V (selfevals V _) %.

Equalities

I need some equalities on types and terms:

%sort eqt {_ tp} {_ tp} %.
%mode eqt %in %out %.
%term eqt_ref eqt T T %.
%worlds () (eqt _ _) %.
%freeze eqt %.
%total D (eqt D _) %.
%sort eqt_symm {_ eqt T T'} {_ eqt T' T} %.
%mode eqt_symm %in %out %.
%term eqt_symm_rule eqt_symm eqt_ref eqt_ref %.
%worlds () (eqt_symm _ _) %.
%freeze eqt_symm %.
%total {} (eqt_symm _ _) %.
%sort eqt_ctx {_ eqt T T'} {C %pi tp %-> tp} {_ eqt (C T) (C T')} %.
%mode eqt_ctx %in %in %out %.
%term eqt_ctx_ref eqt_ctx eqt_ref _ eqt_ref %.
%worlds () (eqt_ctx _ _ _) %.
%freeze eqt_ctx %.
%total D (eqt_ctx D _ _) %.
%sort eqt_ctx2 {_ eqt T T'} {_ eqt T2 T2'} {C %pi tp %-> tp %-> tp} {_ eqt (C T T2) (C T' T2')} %.
%mode eqt_ctx2 %in %in %in %out %.
%term eqt_ctx2_ref eqt_ctx2 eqt_ref eqt_ref _ eqt_ref %.
%worlds () (eqt_ctx2 _ _ _ _) %.
%freeze eqt_ctx2 %.
%total {} (eqt_ctx2 _ _ _ _) %.
%sort eq {_ term} {_ term} %.
%mode eq %in %out %.
%term eq_ref eq M M %.
%worlds () (eq _ _) %.
%freeze eq %.
%total D (eq D _) %.
%sort eq_ctx {_ eq M M'} {C %pi term %-> term} {_ eq (C M) (C M')} %.
%mode eq_ctx %in %in %out %.
%term eq_ctx_ref eq_ctx eq_ref _ eq_ref %.
%worlds () (eq_ctx _ _ _) %.
%freeze eq_ctx %.
%total D (eq_ctx D _ _) %.
%sort eq_ctx2 {_ eq M M'} {_ eq M2 M2'} {C %pi term %-> term %-> term} {_ eq (C M M2) (C M' M2')} %.
%mode eq_ctx2 %in %in %in %out %.
%term eq_ctx2_ref eq_ctx2 eq_ref eq_ref _ eq_ref %.
%worlds () (eq_ctx2 _ _ _ _) %.
%freeze eq_ctx2 %.
%total D (eq_ctx2 D _ _ _) %.
%sort eq_eval {_ eq M M'} {_ M \n/ V} {_ M' \n/ V} %.
%mode eq_eval %in %in %out %.
%term eq_eval_rule eq_eval eq_ref E E %.
%worlds () (eq_eval _ _ _) %.
%freeze eq_eval %.
%total D (eq_eval D _ _) %.
%sort eq_eval2 {_ eq V V'} {_ M \n/ V} {_ M \n/ V'} %.
%mode eq_eval2 %in %in %out %.
%term eq_eval2_rule eq_eval2 eq_ref E E %.
%worlds () (eq_eval2 _ _ _) %.
%freeze eq_eval2 %.
%total D (eq_eval2 D _ _) %.
%sort eq_res_s {_ eq V V'} {_ M \s/ V} {_ M \s/ V'} %.
%mode eq_res_s %in %in %out %.
%term eq_res_s_rile eq_res_s eq_ref E E %.
%worlds () (eq_res_s _ _ _) %.
%freeze eq_res_s %.
%total {} (eq_res_s _ _ _) %.
%sort eq_evaluations {_ M \n/ V} {_ M' \n/ V'} %.
%mode eq_evaluations %in %out %.
%term eq_evaluations_ref eq_evaluations E E %.
%worlds () (eq_evaluations _ _) %.
%freeze eq_evaluations %.
%total D (eq_evaluations D _) %.
%sort eq_tens {_ eq (tens M1 M2) (tens M1' M2')} {_ eq M1 M1'} {_ eq M2 M2'} %.
%mode eq_tens %in %out %out %.
%term eq_tens_rule eq_tens eq_ref eq_ref eq_ref %.
%worlds () (eq_tens _ _ _) %.
%freeze eq_tens %.
%total D (eq_tens D _ _) %.
%sort eq_thunk {_ eq (thunk T E) (thunk T' E')} {_ eq (letb (thunk T E) E) (letb (thunk T' E') E')} %.
%mode eq_thunk %in %out %.
%term eq_thunk_rule eq_thunk eq_ref eq_ref %.
%worlds () (eq_thunk _ _) %.
%freeze eq_thunk %.
%total D (eq_thunk D _) %.
%sort eq_lam {_ eq (lam T E) (lam T' E')} {_ eq X X'} {_ eq (E X) (E' X')} %.
%mode eq_lam %in %in %out %.
%term eq_lam_rule eq_lam eq_ref eq_ref eq_ref %.
%worlds () (eq_lam _ _ _) %.
%freeze eq_lam %.
%total D (eq_lam D _ _) %.
%sort eq_tlam {_ eq (tlam E) (tlam E')} {_ eqt X X'} {_ eq (E X) (E' X')} %.
%mode eq_tlam %in %in %out %.
%term eq_tlam_rule eq_tlam eq_ref eqt_ref eq_ref %.
%worlds () (eq_tlam _ _ _) %.
%freeze eq_tlam %.
%total D (eq_tlam D _ _) %.
%sort eq_sym {_ eq A B} {_ eq B A} %.
%mode eq_sym %in %out %.
%term eq_sym_rule eq_sym eq_ref eq_ref %.
%worlds () (eq_sym _ _) %.
%freeze eq_sym %.
%total D (eq_sym D _) %.

Determinism

Evaluation is deterministic.

%sort eval_determ {_ M \n/ V} {_ M \n/ V'} {_ eq V V'} %.
%mode eval_determ %in %in %out %.
%term eval_determ_unit eval_determ ev_unit ev_unit eq_ref %.
%term eval_determ_tens eval_determ ev_tens ev_tens eq_ref %.
%term eval_determ_tlam eval_determ ev_tlam ev_tlam eq_ref %.
%term eval_determ_lam eval_determ ev_lam ev_lam eq_ref %.
%term eval_determ_thunk eval_determ ev_thunk ev_thunk eq_ref %.
%term eval_determ_app
  %pi (eval_determ (%the (app M1 M2 \n/ V) (ev_app EV2 EV1)) (%the (app M1 M2 \n/ V') (ev_app EV2' EV1')) Q)
  %<- (eval_determ EV1 EV1' Q1)
  %<- (eq_lam Q1 (%the (eq M2 M2) eq_ref) Q3)
  %<- (eq_sym Q3 Q4)
  %<- (eq_eval Q4 EV2' EV2s)
  %<- (eval_determ EV2 EV2s Q) %.
%term eval_determ_tapp
  %pi (eval_determ (%the (tapp M1 T2 \n/ V) (ev_tapp EV2 EV1)) (%the (tapp M1 T2 \n/ V') (ev_tapp EV2' EV1')) Q)
  %<- (eval_determ EV1 EV1' Q1)
  %<- (eq_tlam Q1 (%the (eqt T2 T2) eqt_ref) Q3)
  %<- (eq_sym Q3 Q4)
  %<- (eq_eval Q4 EV2' EV2s)
  %<- (eval_determ EV2 EV2s Q) %.
%term eval_determ_letb
  %pi (eval_determ (%the (letb M1 M2 \n/ V) (ev_letb EV2 EV1)) (%the (letb M1 M2 \n/ V') (ev_letb EV2' EV1')) Q)
  %<- (eval_determ EV1 EV1' Q1)
  %<- (eq_thunk Q1 Q2)
  %<- (eq_ctx Q2 M2 Q3)
  %<- (eq_sym Q3 Q4)
  %<- (eq_eval Q4 EV2' EV2s)
  %<- (eval_determ EV2 EV2s Q) %.
%term eval_determ_letu
  %pi (eval_determ (%the (letu M1 M2 \n/ V) (ev_letu EV2 EV1)) (%the (letu M1 M2 \n/ V') (ev_letu EV2' EV1')) Q)
  %<- (eval_determ EV2 EV2' Q) %.
%term eval_determ_lett
  %pi (eval_determ (%the (lett M1 M2 \n/ V) (ev_lett EV2 EV1)) (%the (lett M1 M2 \n/ V') (ev_lett EV2' EV1')) Q)
  %<- (eval_determ EV1 EV1' Q1)
  %<- (eq_tens Q1 Q2 Q3)
  %<- (eq_ctx2 Q2 Q3 M2 Q4)
  %<- (eq_sym Q4 Q4')
  %<- (eq_eval Q4' EV2' EV2s)
  %<- (eval_determ EV2 EV2s Q) %.
%worlds () (eval_determ _ _ _) %.
%freeze eval_determ %.
%total D (eval_determ D _ _) %.

And transitive:

%sort eval_trans {_ M \n/ V} {_ V \n/ V'} {_ M \n/ V'} %.
%mode eval_trans %in %in %out %.
%term eval_trans_rule
  %pi (eval_trans EV EV' EV'')
  %<- (value_soundness EV Vv)
  %<- (selfeval Vv EVv')
  %<- (eval_determ EVv' EV' Q)
  %<- (eq_eval2 Q EV EV'') %.
%worlds () (eval_trans _ _ _) %.
%total {} (eval_trans _ _ _) %.
%sort eq_val {_ eq M M'} {_ value M} {_ value M'} %.
%mode eq_val %in %in %out %.
%term eq_val_rule eq_val eq_ref V V %.
%worlds () (eq_val _ _ _) %.
%freeze eval_trans %.
%total {} (eq_val _ _ _) %.

Frame stack semantics

The abstract machine is defined as a relation on tuples consisting of a frame stack and a term to evaluate in that stack.

Evaluation frames

The frame stack is a stack of evaluation frames that provides a context on which we will continue evaluation after we have computed a value for the current term.

%sort frame {_ %pi term %-> term} %.
%name frame %.
%term fletb {M} frame ([a] letb a M) %.
%term fapp {M} frame ([a] app a M) %.
%term ftapp {T} frame ([a] tapp a T) %.
%term fletu {M} frame ([a] letu a M) %.
%term flett {M} frame ([a] lett a M) %.
%freeze frame %.

Evaluation frames are functions from terms to terms and sometimes I need to apply such a function to a term.

%sort frameapp {_ frame F} {_ term} {_ term} %.
%mode frameapp %in %in %out %.
%term frameapp_app frameapp (%the (frame F') F) M (F' M) %.
%worlds () (frameapp _ _ _) %.
%freeze frameapp %.
%total D (frameapp D _ _) %.
%sort frameapp_exists {F} {M} {_ frameapp F M M'} %.
%mode frameapp_exists %in %in %out %.
%term frameapp_exists_rule frameapp_exists F M frameapp_app %.
%worlds () (frameapp_exists _ _ _) %.
%freeze frameapp_exists %.
%total D (frameapp_exists D _ _) %.

The definition of the frame stack and application of frame stacks to terms.

%sort framestack %.
%name framestack %.
%term cons %pi (frame F) %-> framestack %-> framestack %.
%term nil framestack %.
%freeze framestack %.
%sort frameapply {_ framestack} {_ term} {_ term} %.
%mode frameapply %in %in %out %.
%term frameapply_nil frameapply nil M M %.
%term frameapply_cons
  %pi (frameapply (cons F Fs) M M')
  %<- (frameapp F M M'')
  %<- (frameapply Fs M'' M') %.
%worlds () (frameapply _ _ _) %.
%freeze frameapply %.
%total D (frameapply D _ _) %.

I should move you:

%block blam {y term}%.

Equalities on frame stacks

I also need some equational reasoning on frame stacks:

%sort eqf {_ framestack} {_ framestack} %.
%mode eqf %in %out %.
%term eqf_ref eqf Fs Fs %.
%freeze eqf %.
%sort eqf_symm {_ eqf Fs Fs'} {_ eqf Fs' Fs} %.
%mode eqf_symm %in %out %.
%term eqf_symm_rule eqf_symm eqf_ref eqf_ref %.
%worlds (blam) (eqf_symm _ _) %.
%freeze eqf_symm %.
%total {} (eqf_symm _ _) %.
%sort eqf_trans {_ eqf Fs Fs'} {_ eqf Fs' Fs''} {_ eqf Fs Fs''} %.
%mode eqf_trans %in %in %out %.
%term eqf_trans_rule eqf_trans eqf_ref eqf_ref eqf_ref %.
%worlds (blam) (eqf_trans _ _ _) %.
%freeze eqf_trans %.
%total {} (eqf_trans _ _ _) %.
%sort eqf_extend {F} {_ eqf Fs Fs'} {_ eqf (cons F Fs) (cons F Fs')} %.
%mode eqf_extend %in %in %out %.
%term eqf_extend_rule eqf_extend _ eqf_ref eqf_ref %.
%worlds (blam) (eqf_extend _ _ _) %.
%freeze eqf_extend %.
%total {} (eqf_extend _ _ _) %.
%sort frameapply_eq {_ eqf Fs Fs'} {_ frameapply Fs M FsM} {_ frameapply Fs' M FsM} %.
%mode frameapply_eq %in %in %out %.
%term frameapply_eq_rule frameapply_eq eqf_ref FA FA %.
%worlds (blam) (frameapply_eq _ _ _) %.
%freeze frameapply_eq %.
%total {} (frameapply_eq _ _ _) %.
%sort frameapply_nil_eq {_ frameapply nil M M'} {_ eq M M'} %.
%mode frameapply_nil_eq %in %out %.
%term frameapply_nil_eq_rule frameapply_nil_eq frameapply_nil eq_ref %.
%worlds (blam) (frameapply_nil_eq _ _) %.
%freeze frameapply_nil_eq %.
%total {} (frameapply_nil_eq _ _) %.

More metatheorems about frame application

%sort frameapply_exists {Fs} {M} {_ frameapply Fs M M'} %.
%mode frameapply_exists %in %in %out %.
%term frameapply_exists_nil frameapply_exists nil M frameapply_nil %.
%term frameapply_exists_cons_letu
  %pi (frameapply_exists (cons (fletu N) Fs) M (frameapply_cons FsA frameapp_app))
  %<- (frameapply_exists Fs (letu M N) FsA) %.
%term frameapply_exists_cons_letb
  %pi (frameapply_exists (cons (fletb N) Fs) M (frameapply_cons FsA frameapp_app))
  %<- (frameapply_exists Fs (letb M N) FsA) %.
%term frameapply_exists_cons_lett
  %pi (frameapply_exists (cons (flett N) Fs) M (frameapply_cons FsA frameapp_app))
  %<- (frameapply_exists Fs (lett M N) FsA) %.
%term frameapply_exists_cons_app
  %pi (frameapply_exists (cons (fapp N) Fs) M (frameapply_cons FsA frameapp_app))
  %<- (frameapply_exists Fs (app M N) FsA) %.
%term frameapply_exists_cons_tapp
  %pi (frameapply_exists (cons (ftapp N) Fs) M (frameapply_cons FsA frameapp_app))
  %<- (frameapply_exists Fs (tapp M N) FsA) %.
%worlds () (frameapply_exists _ _ _) %.
%freeze frameapply_exists %.
%total D (frameapply_exists D _ _) %.

Frame stack evaluation

Here I define the evaluation relation for the abstract machine.

%scope frameapply_exists_cons_tapp %sort -> {_ framestack} {_ term} {_ framestack} {_ term} %.
%mode --> %in %in %out %out %.
%term evfs_letu --> Fs (letu M N) (cons (fletu N) Fs) M %.
%term evfs_letb --> Fs (letb M N) (cons (fletb N) Fs) M %.
%term evfs_lett --> Fs (lett M N) (cons (flett N) Fs) M %.
%term evfs_app --> Fs (app M N) (cons (fapp N) Fs) M %.
%term evfs_tapp --> Fs (tapp M T) (cons (ftapp T) Fs) M %.
%term evfs_lam --> (cons (fapp N) Fs) (lam _ M') Fs (M' N) %.
%term evfs_tlam --> (cons (ftapp T) Fs) (tlam M') Fs (M' T) %.
%term evfs_unit --> (cons (fletu N) Fs) unit Fs N %.
%term evfs_tens --> (cons (flett N) Fs) (tens M1 M2) Fs (N M1 M2) %.
%term evfs_thunk --> (cons (fletb N) Fs) (thunk T M) Fs (N (letb (thunk T M) M)) %.
%worlds () (--> _ _ _ _) %.
%covers --> %out %in %out %out %.
%freeze --> %.
%sort eq_step {_ eq M M'} {_ --> Fs M Fs1 M1} {_ --> Fs M' Fs1 M1} %.
%mode eq_step %in %in %out %.
%term eq_step_rule eq_step eq_ref S S %.
%worlds () (eq_step _ _ _) %.
%total {} (eq_step _ _ _) %.
%scope eq_step_rule %sort ->* {_ framestack} {_ term} {_ framestack} {_ term} %.
%term ->*_ref -->* Fs M Fs M %.
%scope eq_step_rule %term ->*_step %pi (-->* Fs M Fs' M') %<- (--> Fs'' M'' Fs' M') %<- (-->* Fs M Fs'' M'') %.
%freeze -->* %.

Meta theory of the abstract machine

Here are some basic properties of the abstract machine:

%sort concat-->* {_ -->* Fs M Fs'' M''} {_ -->* Fs'' M'' Fs' M'} {_ -->* Fs M Fs' M'} %.
%mode concat-->* %in %in %out %.
%term concatref concat-->* S -->*_ref S %.
%term concatstep %pi (concat-->* S' (-->*_step Ss S) (-->*_step Sc S)) %<- (concat-->* S' Ss Sc) %.
%worlds () (concat-->* _ _ _) %.
%freeze concat-->* %.
%total D (concat-->* _ D _) %.
%scope concatstep %sort ->*_impossible {_ --> nil V Fs M} {_ value V} {_ -->* Fs' M' Fs'' M''} %.
%mode {%in V term} {%in Fs framestack} {%in M term} {%in Fs' framestack} {%in M' term} {%in Fs'' framestack} {%in M'' term} {%in S --> nil V Fs M} {%in V1 value V} {%out R -->* Fs' M' Fs'' M''} -->*_impossible S V1 R %.
%worlds () (-->*_impossible _ _ _) %.
%freeze -->*_impossible %.
%total {} (-->*_impossible _ _ _) %.
%sort lemma44 {Fs framestack} {M} {_ frameapply Fs M FsM} {_ -->* nil FsM Fs M} %.
%mode lemma44 %in %in %in %out %.
%term lemma44_nil lemma44 nil M frameapply_nil -->*_ref %.
%term lemma44_cons_letu
  %pi (lemma44 (cons (fletu N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_letu))
  %<- (lemma44 Fs (letu M N) FA MS) %.
%term lemma44_cons_letb
  %pi (lemma44 (cons (fletb N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_letb))
  %<- (lemma44 Fs (letb M N) FA MS) %.
%term lemma44_cons_lett
  %pi (lemma44 (cons (flett N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_lett))
  %<- (lemma44 Fs (lett M N) FA MS) %.
%term lemma44_cons_app
  %pi (lemma44 (cons (fapp N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_app))
  %<- (lemma44 Fs (app M N) FA MS) %.
%term lemma44_cons_tapp
  %pi (lemma44 (cons (ftapp N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_tapp))
  %<- (lemma44 Fs (tapp M N) FA MS) %.
%worlds () (lemma44 _ _ _ _) %.
%freeze lemma44 %.
%total D (lemma44 D _ _ _) %.
%sort frameApplyUnique {_ frameapply Fs M FsM} {_ frameapply Fs M FsM'} {_ eq FsM FsM'} %.
%mode frameApplyUnique %in %in %out %.
%term frameApplyUnique_nil frameApplyUnique frameapply_nil frameapply_nil eq_ref %.
%term frameApplyUnique_cons
  %pi (frameApplyUnique (frameapply_cons FsA frameapp_app) (frameapply_cons FsA' frameapp_app) Q)
  %<- (frameApplyUnique FsA FsA' Q) %.
%worlds () (frameApplyUnique _ _ _) %.
%freeze frameApplyUnique %.
%total D (frameApplyUnique D _ _) %.

Correspondence between the big step semantics and the abstract machine

%sort lemma48 {Fs} {M} {_ M \n/ V} {_ -->* Fs M Fs V} %.
%mode lemma48 %in %in %in %out %.
%term lemma48_lam lemma48 _ _ ev_lam -->*_ref %.
%term lemma48_tens lemma48 _ _ ev_tens -->*_ref %.
%term lemma48_thunk lemma48 _ _ ev_thunk -->*_ref %.
%term lemma48_tlam lemma48 _ _ ev_tlam -->*_ref %.
%term lemma48_unit lemma48 _ _ ev_unit -->*_ref %.
%term lemma48_app
  %pi (lemma48 Fs (app M1 M2) (ev_app EM' EM1) Sr)
  %<- (lemma48 (cons (fapp M2) Fs) M1 (%the (M1 \n/ (lam _ M')) EM1) SM1)
  %<- (lemma48 Fs (M' M2) (%the (M' M2 \n/ V) EM') SM')
  %<- (concat-->* (-->*_step SM1 evfs_lam) SM' S)
  %<- (concat-->* (-->*_step -->*_ref evfs_app) S Sr) %.
%term lemma48_tapp
  %pi (lemma48 Fs (tapp M1 T) (ev_tapp EM' EM1) Sr)
  %<- (lemma48 (cons (ftapp T) Fs) M1 (%the (M1 \n/ (tlam M')) EM1) SM1)
  %<- (lemma48 Fs (M' T) (%the (M' T \n/ V) EM') SM')
  %<- (concat-->* (-->*_step SM1 evfs_tlam) SM' S)
  %<- (concat-->* (-->*_step -->*_ref evfs_tapp) S Sr) %.
%term lemma48_letu
  %pi (lemma48 Fs (letu M1 M2) (ev_letu EM' EM1) Sr)
  %<- (lemma48 (cons (fletu M2) Fs) M1 (%the (M1 \n/ unit) EM1) SM1)
  %<- (lemma48 Fs M2 (%the (M2 \n/ V) EM') SM')
  %<- (concat-->* (-->*_step SM1 evfs_unit) SM' S)
  %<- (concat-->* (-->*_step -->*_ref evfs_letu) S Sr) %.
%term lemma48_letb
  %pi (lemma48 Fs (letb M1 M2) (ev_letb EM' EM1) Sr)
  %<- (lemma48 (cons (fletb M2) Fs) M1 (%the (M1 \n/ (thunk T M')) EM1) SM1)
  %<- (lemma48 Fs (M2 (letb (thunk T M') M')) (%the (M2 (letb (thunk T M') M') \n/ V) EM') SM')
  %<- (concat-->* (-->*_step SM1 evfs_thunk) SM' S)
  %<- (concat-->* (-->*_step -->*_ref evfs_letb) S Sr) %.
%term lemma48_lett
  %pi (lemma48 Fs (lett M1 M2) (ev_lett EM' EM1) Sr)
  %<- (lemma48 (cons (flett M2) Fs) M1 (%the (M1 \n/ (tens M' M'')) EM1) SM1)
  %<- (lemma48 Fs (M2 M' M'') (%the (M2 M' M'' \n/ V) EM') SM')
  %<- (concat-->* (-->*_step SM1 evfs_tens) SM' S)
  %<- (concat-->* (-->*_step -->*_ref evfs_lett) S Sr) %.
%worlds () (lemma48 _ _ _ _) %.
%freeze lemma48 %.
%total D (lemma48 _ _ D _) %.
%sort lemma46a {Fs framestack} {_ M' \n/ V} {_ frameapply Fs M M'} {_ frameapply Fs V' N} {_ M \n/ V'} {_ N \n/ V} %.
%sort lemma46b {Fs framestack} {_ M \n/ V'} {_ N \n/ V} {_ frameapply Fs M M'} {_ frameapply Fs V' N} {_ M' \n/ V} %.
%mode lemma46a %in %in %in %out %out %out %.
%mode lemma46b %in %in %in %in %in %out %.
%term lemma46a_nil
  %pi (lemma46a nil E frameapply_nil frameapply_nil E EV)
  %<- (value_soundness E Vv)
  %<- (selfeval Vv EV) %.
%term lemma46a_letu
  %pi (lemma46a (cons (fletu N) Fs) (%the (M' \n/ V) E) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E')
  %<- (lemma46a Fs E FA FA' (ev_letu (%the (N \n/ V') RN) RM) (%the (_ \n/ V) R2))
  %<- (frameapply_exists Fs (letu unit N) FAu)
  %<- (lemma46b Fs (%the (letu unit N \n/ V') (ev_letu RN ev_unit)) R2 FAu FA' E') %.
%term lemma46a_app
  %pi (lemma46a (cons (fapp N) Fs) (%the (M' \n/ V) E) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E')
  %<- (lemma46a Fs E FA FA' (ev_app RN (%the (M \n/ (lam T M1)) RM)) R2)
  %<- (frameapply_exists Fs (app (lam T M1) N) FAu)
  %<- (lemma46b Fs (ev_app RN ev_lam) R2 FAu FA' E') %.
%term lemma46a_tapp
  %pi (lemma46a (cons (ftapp N) Fs) (%the (M' \n/ V) E) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E')
  %<- (lemma46a Fs E FA FA' (ev_tapp RN (%the (M \n/ (tlam T)) RM)) R2)
  %<- (frameapply_exists Fs (tapp (tlam T) N) FAu)
  %<- (lemma46b Fs (ev_tapp RN ev_tlam) R2 FAu FA' E') %.
%term lemma46a_letb
  %pi (lemma46a (cons (fletb N) Fs) (%the (M' \n/ V) E) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E')
  %<- (lemma46a Fs E FA FA' (ev_letb RN (%the (M \n/ (thunk T M1)) RM)) R2)
  %<- (frameapply_exists Fs (letb (thunk T M1) N) FAu)
  %<- (lemma46b Fs (ev_letb RN ev_thunk) R2 FAu FA' E') %.
%term lemma46a_lett
  %pi (lemma46a (cons (flett N) Fs) (%the (M' \n/ V) E) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E')
  %<- (lemma46a Fs E FA FA' (ev_lett RN (%the (M \n/ (tens M1 M2)) RM)) R2)
  %<- (frameapply_exists Fs (lett (tens M1 M2) N) FAu)
  %<- (lemma46b Fs (ev_lett RN ev_tens) R2 FAu FA' E') %.
%term lemma46b_nil
  %pi (lemma46b nil (%the (M1 \n/ M2) E) E' frameapply_nil frameapply_nil E'')
  %<- (value_soundness E V)
  %<- (selfeval V EV)
  %<- (eval_determ EV E' Q)
  %<- (eq_eval2 Q E E'') %.
%term lemma46b_letu
  %pi (lemma46b (cons (fletu M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3)
  %<- (lemma46a Fs1 E2 X2 X3 (ev_letu EM6 EM2) EN)
  %<- (eval_trans E1 EM2 EM1)
  %<- (lemma46b Fs1 (ev_letu EM6 EM1) EN X1 X3 E3) %.
%term lemma46b_lett
  %pi (lemma46b (cons (flett M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3)
  %<- (lemma46a Fs1 E2 X2 X3 (ev_lett EM6 EM2) EN)
  %<- (eval_trans E1 EM2 EM1)
  %<- (lemma46b Fs1 (ev_lett EM6 EM1) EN X1 X3 E3) %.
%term lemma46b_app
  %pi (lemma46b (cons (fapp M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3)
  %<- (lemma46a Fs1 E2 X2 X3 (ev_app EM6 EM2) EN)
  %<- (eval_trans E1 EM2 EM1)
  %<- (lemma46b Fs1 (ev_app EM6 EM1) EN X1 X3 E3) %.
%term lemma46b_tapp
  %pi (lemma46b (cons (ftapp M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3)
  %<- (lemma46a Fs1 E2 X2 X3 (ev_tapp EM6 EM2) EN)
  %<- (eval_trans E1 EM2 EM1)
  %<- (lemma46b Fs1 (ev_tapp EM6 EM1) EN X1 X3 E3) %.
%term lemma46b_letb
  %pi (lemma46b (cons (fletb M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3)
  %<- (lemma46a Fs1 E2 X2 X3 (ev_letb EM6 EM2) EN)
  %<- (eval_trans E1 EM2 EM1)
  %<- (lemma46b Fs1 (ev_letb EM6 EM1) EN X1 X3 E3) %.
%worlds () (lemma46a _ _ _ _ _ _) (lemma46b _ _ _ _ _ _) %.
%freeze lemma46b lemma46a %.
%total (D E) (lemma46a D _ _ _ _ _) (lemma46b E _ _ _ _ _) %.
%sort lemma47 {_ --> Fs M Fs' M'} {_ frameapply Fs' M' FsM'} {_ frameapply Fs M FsM} {_ FsM' \n/ V} {_ FsM \n/ V} %.
%mode lemma47 %in %in %out %in %out %.
%term lemma47_letu lemma47 evfs_letu (frameapply_cons X1 frameapp_app) X1 EV' EV' %.
%term lemma47_letb lemma47 evfs_letb (frameapply_cons X1 frameapp_app) X1 EV' EV' %.
%term lemma47_lett lemma47 evfs_lett (frameapply_cons X1 frameapp_app) X1 EV' EV' %.
%term lemma47_app lemma47 evfs_app (frameapply_cons X1 frameapp_app) X1 EV' EV' %.
%term lemma47_tapp lemma47 evfs_tapp (frameapply_cons X1 frameapp_app) X1 EV' EV' %.
%term lemma47_unit
  %pi (lemma47 evfs_unit X1 (frameapply_cons X3 frameapp_app) EV' EV)
  %<- (lemma46a Fs EV' X1 X2 (%the (M2 \n/ V') EM2) EN)
  %<- (frameapply_exists Fs (letu unit M2) X3)
  %<- (lemma46b Fs (ev_letu EM2 ev_unit) EN X3 X2 EV) %.
%term lemma47_tens
  %pi (lemma47 evfs_tens X1 (frameapply_cons X3 frameapp_app) EV' EV)
  %<- (lemma46a Fs EV' X1 X2 EM2 EN)
  %<- (frameapply_exists Fs (lett (tens M3 M4) M2) X3)
  %<- (lemma46b Fs (ev_lett EM2 ev_tens) EN X3 X2 EV) %.
%term lemma47_thunk
  %pi (lemma47 evfs_thunk X1 (frameapply_cons X3 frameapp_app) EV' EV)
  %<- (lemma46a Fs EV' X1 X2 EM2 EN)
  %<- (frameapply_exists Fs (letb (thunk T M4) M2) X3)
  %<- (lemma46b Fs (ev_letb EM2 ev_thunk) EN X3 X2 EV) %.
%term lemma47_lam
  %pi (lemma47 evfs_lam X1 (frameapply_cons X3 frameapp_app) EV' EV)
  %<- (lemma46a Fs EV' X1 X2 EM2 EN)
  %<- (frameapply_exists Fs (app (lam T M4) M2) X3)
  %<- (lemma46b Fs (ev_app EM2 ev_lam) EN X3 X2 EV) %.
%term lemma47_tlam
  %pi (lemma47 evfs_tlam X1 (frameapply_cons X3 frameapp_app) EV' EV)
  %<- (lemma46a Fs EV' X1 X2 EM2 EN)
  %<- (frameapply_exists Fs (tapp (tlam M4) M2) X3)
  %<- (lemma46b Fs (ev_tapp EM2 ev_tlam) EN X3 X2 EV) %.
%worlds () (lemma47 _ _ _ _ _) %.
%freeze lemma47 %.
%total S (lemma47 S _ _ _ _) %.
%scope lemma47_tlam %sort ->r* {_ framestack} {_ term} {_ framestack} {_ term} %.
%term ->r*_ref -->r* Fs M Fs M %.
%scope lemma47_tlam %term ->r*_step %pi (-->r* Fs M Fs' M') %<- (--> Fs M Fs'' M'') %<- (-->r* Fs'' M'' Fs' M') %.
%freeze -->r* %.
%sort concat-->r* {_ -->r* Fs M Fs' M'} {_ -->r* Fs' M' Fs'' M''} {_ -->r* Fs M Fs'' M''} %.
%mode concat-->r* %in %in %out %.
%term concat-->r*_ref concat-->r* -->r*_ref D D %.
%term concat-->r*_step %pi (concat-->r* (-->r*_step R S) D (-->r*_step D' S)) %<- (concat-->r* R D D') %.
%worlds () (concat-->r* _ _ _) %.
%freeze concat-->r* %.
%total D (concat-->r* D _ _) %.
%scope concat-->r*_step %sort ->r*_impossible {_ --> nil V Fs M} {_ value V} {_ -->r* Fs' M' Fs'' M''} %.
%mode {%in V term} {%in Fs framestack} {%in M term} {%in Fs' framestack} {%in M' term} {%in Fs'' framestack} {%in M'' term} {%in S --> nil V Fs M} {%in V1 value V} {%out R -->r* Fs' M' Fs'' M''} -->r*_impossible S V1 R %.
%worlds () (-->r*_impossible _ _ _) %.
%freeze -->r*_impossible %.
%total {} (-->r*_impossible _ _ _) %.
%sort concat-->r*_exists {R -->r* F1 M1 Fs M} {S -->r* (%the framestack Fs) (%the term M) (%the framestack Fs2) (%the term M2)} {_ concat-->r* R S RS} %.
%mode concat-->r*_exists %in %in %out %.
%term concat-->r*_exists_ref concat-->r*_exists -->r*_ref _ concat-->r*_ref %.
%term concat-->r*_exists_step
  %pi (concat-->r*_exists (-->r*_step R S) B (concat-->r*_step E))
  %<- (concat-->r*_exists R B E) %.
%worlds () (concat-->r*_exists _ _ _) %.
%freeze concat-->r*_exists %.
%total D (concat-->r*_exists D _ _) %.
%scope concat-->r*_exists_step %sort ->*_to_-->r*_lem {_ -->* Fs M Fs' M'} {_ -->r* Fs M Fs' M'} %.
%mode -->*_to_-->r*_lem %in %out %.
%scope concat-->r*_exists_step %term ->*_to_-->r*_lem_ref -->*_to_-->r*_lem -->*_ref -->r*_ref %.
%term ->*_to_-->r*_lem_step
  %pi (-->*_to_-->r*_lem (-->*_step R S) R'')
  %<- (-->*_to_-->r*_lem R R')
  %<- (concat-->r* R' (-->r*_step -->r*_ref S) R'') %.
%worlds () (-->*_to_-->r*_lem _ _) %.
%freeze -->*_to_-->r*_lem %.
%total D (-->*_to_-->r*_lem D _) %.
%scope concat-->r*_exists_step %sort ->r*_to_-->*_lem {_ -->r* Fs M Fs' M'} {_ -->* Fs M Fs' M'} %.
%mode -->r*_to_-->*_lem %in %out %.
%scope concat-->r*_exists_step %term ->r*_to_-->*_lem_ref -->r*_to_-->*_lem -->r*_ref -->*_ref %.
%term ->r*_to_-->*_lem_step
  %pi (-->r*_to_-->*_lem (-->r*_step R S) R'')
  %<- (-->r*_to_-->*_lem R R')
  %<- (concat-->* (-->*_step -->*_ref S) R' R'') %.
%worlds () (-->r*_to_-->*_lem _ _) %.
%freeze -->r*_to_-->*_lem %.
%total D (-->r*_to_-->*_lem D _) %.
%scope concat-->r*_exists_step %sort ->r*_add_step {_ --> Fs M Fs' M'} {_ -->r* Fs M nil V} {_ value V} {_ -->r* Fs' M' nil V} %.
%mode -->r*_add_step %in %in %in %out %.
%scope concat-->r*_exists_step %term ->r*_add_step_ref %pi (-->r*_add_step S -->r*_ref V R) %<- (-->r*_impossible S V R) %.
%term ->r*_add_step_step -->r*_add_step S (-->r*_step Rr S) V Rr %.
%worlds () (-->r*_add_step _ _ _ _) %.
%freeze -->r*_add_step %.
%total {} (-->r*_add_step _ _ _ _) %.
%scope concat-->r*_exists_step %sort ->*_add_step {_ --> Fs M Fs' M'} {_ -->* Fs M nil V} {_ value V} {_ -->* Fs' M' nil V} %.
%mode -->*_add_step %in %in %in %out %.
%scope concat-->r*_exists_step %term ->*_add_step_rule
  %pi (-->*_add_step S R V R')
  %<- (-->*_to_-->r*_lem R Rr)
  %<- (-->r*_add_step S Rr V R'r)
  %<- (-->r*_to_-->*_lem R'r R') %.
%worlds () (-->*_add_step _ _ _ _) %.
%freeze -->*_add_step %.
%total {} (-->*_add_step _ _ _ _) %.
%scope concat-->r*_exists_step %sort ->*_to_-->r*_lem_exists {S -->* _ _ _ _} {_ -->*_to_-->r*_lem S R} %.
%mode -->*_to_-->r*_lem_exists %in %out %.
%scope concat-->r*_exists_step %term ->*_to_-->r*_lem_exists_ref -->*_to_-->r*_lem_exists -->*_ref -->*_to_-->r*_lem_ref %.
%term ->*_to_-->r*_lem_exists_step
  %pi (-->*_to_-->r*_lem_exists (-->*_step R S) (-->*_to_-->r*_lem_step R'' R'))
  %<- (-->*_to_-->r*_lem_exists R (%the (-->*_to_-->r*_lem R Rr) R'))
  %<- (concat-->r*_exists Rr (-->r*_step -->r*_ref S) R'') %.
%worlds () (-->*_to_-->r*_lem_exists _ _) %.
%freeze -->*_to_-->r*_lem_exists %.
%total D (-->*_to_-->r*_lem_exists D _) %.
%sort eq_frame_eval_lemma {_ -->r* Fs M nil V} {_ value V} {_ frameapply Fs M FsM} {_ FsM \n/ V} %.
%mode eq_frame_eval_lemma %in %in %out %out %.
%term eq_frame_eval_lemma_z %pi (eq_frame_eval_lemma -->r*_ref V frameapply_nil EV) %<- (selfeval V EV) %.
%term eq_frame_eval_lemma_s
  %pi (eq_frame_eval_lemma (-->r*_step R S) V FA EV)
  %<- (eq_frame_eval_lemma R V FA' EV')
  %<- (lemma47 S FA' FA EV' EV) %.
%worlds () (eq_frame_eval_lemma _ _ _ _) %.
%freeze eq_frame_eval_lemma %.
%total D (eq_frame_eval_lemma D _ _ _) %.
%sort eq_frame_eval {_ -->* Fs M nil V} {_ value V} {_ frameapply Fs M FsM} {_ FsM \n/ V} %.
%mode eq_frame_eval %in %in %out %out %.
%term eq_frame_eval_rule
  %pi (eq_frame_eval FE V FA E)
  %<- (-->*_to_-->r*_lem FE R)
  %<- (eq_frame_eval_lemma R V FA E) %.
%worlds () (eq_frame_eval _ _ _ _) %.
%freeze eq_frame_eval %.
%total D (eq_frame_eval D _ _ _) %.
%scope eq_frame_eval_rule %sort ->*_skew {_ -->* Fs M nil V} {_ value V} {_ -->* Fs M Fs' M'} {_ -->* Fs' M' nil V} %.
%mode -->*_skew %in %in %in %out %.
%scope eq_frame_eval_rule %term ->*_skew_ref -->*_skew R V -->*_ref R %.
%term ->*_skew_step
  %pi (-->*_skew R V (-->*_step Rest S) RI)
  %<- (-->*_skew R V Rest RI')
  %<- (-->*_add_step S RI' V RI) %.
%worlds () (-->*_skew _ _ _ _) %.
%freeze -->*_skew %.
%total D (-->*_skew _ _ D _) %.
%sort eq_eval_frame {_ frameapply Fs M FsM} {_ FsM \n/ V} {_ -->* Fs M nil V} %.
%mode eq_eval_frame %in %in %out %.
%term eq_eval_frame_rule
  %pi (eq_eval_frame (%the (frameapply Fs M FsM) FA) EV R)
  %<- (lemma44 Fs M FA R'')
  %<- (lemma48 nil FsM EV R')
  %<- (value_soundness EV V)
  %<- (-->*_skew R' V R'' R) %.
%worlds () (eq_eval_frame _ _ _) %.
%freeze eq_eval_frame %.
%total {} (eq_eval_frame _ _ _) %.

Termination relation on the abstract machine

%sort frameterm {_ framestack} {_ term} %.
%term frameterm_val %pi (frameterm nil V) %<- (value V) %.
%term frameterm_app %pi (frameterm Fs (app M1 M2)) %<- (frameterm (cons (fapp M2) Fs) M1) %.
%term frameterm_tapp %pi (frameterm Fs (tapp M T)) %<- (frameterm (cons (ftapp T) Fs) M) %.
%term frameterm_letu %pi (frameterm Fs (letu M1 M2)) %<- (frameterm (cons (fletu M2) Fs) M1) %.
%term frameterm_letb %pi (frameterm Fs (letb M1 M2)) %<- (frameterm (cons (fletb M2) Fs) M1) %.
%term frameterm_lett %pi (frameterm Fs (lett M1 M2)) %<- (frameterm (cons (flett M2) Fs) M1) %.
%term frameterm_lam %pi (frameterm (cons (fapp M2) Fs) (lam T M1)) %<- (frameterm Fs (M1 M2)) %.
%term frameterm_tlam %pi (frameterm (cons (ftapp T) Fs) (tlam M1)) %<- (frameterm Fs (M1 T)) %.
%term frameterm_tens %pi (frameterm (cons (flett M3) Fs) (tens M1 M2)) %<- (frameterm Fs (M3 M1 M2)) %.
%term frameterm_thunk
  %pi (frameterm (cons (fletb M2) Fs) (thunk T M1))
  %<- (frameterm Fs (M2 (letb (thunk T M1) M1))) %.
%term frameterm_unit %pi (frameterm (cons (fletu M3) Fs) unit) %<- (frameterm Fs M3) %.
%freeze frameterm %.
%sort frameterm_eq_frames {_ eqf Fs Fs'} {_ eq M M'} {_ frameterm Fs M} {_ frameterm Fs' M'} %.
%mode frameterm_eq_frames %in %in %in %out %.
%term frameterm_eq_frames_rule frameterm_eq_frames eqf_ref eq_ref Ft Ft %.
%worlds () (frameterm_eq_frames _ _ _ _) %.
%freeze frameterm_eq_frames %.
%total {} (frameterm_eq_frames _ _ _ _) %.
%sort eq_frameterms {_ frameterm Fs M} {_ frameterm Fs M} %.
%mode eq_frameterms %in %out %.
%term eq_frameterms_ref eq_frameterms F F %.
%worlds () (eq_frameterms _ _) %.
%freeze eq_frameterms %.
%total {} (eq_frameterms _ _) %.
%sort inverse_ft_app {_ frameterm Fs (app M1 M2)} {_ frameterm (cons (fapp M2) Fs) M1} %.
%mode inverse_ft_app %in %out %.
%term inverse_ft_app_rule inverse_ft_app (frameterm_app Ft) Ft %.
%worlds () (inverse_ft_app _ _) %.
%reduces < D E (inverse_ft_app E D) %.
%total {} (inverse_ft_app _ _) %.
%sort inverse_ft_tapp {_ frameterm Fs (tapp M1 M2)} {_ frameterm (cons (ftapp M2) Fs) M1} %.
%mode inverse_ft_tapp %in %out %.
%term inverse_ft_tapp_rule inverse_ft_tapp (frameterm_tapp Ft) Ft %.
%worlds () (inverse_ft_tapp _ _) %.
%reduces < D E (inverse_ft_tapp E D) %.
%total {} (inverse_ft_tapp _ _) %.
%sort inverse_ft_letu {_ frameterm Fs (letu M1 M2)} {_ frameterm (cons (fletu M2) Fs) M1} %.
%mode inverse_ft_letu %in %out %.
%term inverse_ft_letu_rule inverse_ft_letu (frameterm_letu Ft) Ft %.
%worlds () (inverse_ft_letu _ _) %.
%reduces < D E (inverse_ft_letu E D) %.
%total {} (inverse_ft_letu _ _) %.
%sort inverse_ft_lett {_ frameterm Fs (lett M1 M2)} {_ frameterm (cons (flett M2) Fs) M1} %.
%mode inverse_ft_lett %in %out %.
%term inverse_ft_lett_rule inverse_ft_lett (frameterm_lett Ft) Ft %.
%worlds () (inverse_ft_lett _ _) %.
%reduces < D E (inverse_ft_lett E D) %.
%total {} (inverse_ft_lett _ _) %.
%sort inverse_ft_letb {_ frameterm Fs (letb M1 M2)} {_ frameterm (cons (fletb M2) Fs) M1} %.
%mode inverse_ft_letb %in %out %.
%term inverse_ft_letb_rule inverse_ft_letb (frameterm_letb Ft) Ft %.
%worlds () (inverse_ft_letb _ _) %.
%reduces < D E (inverse_ft_letb E D) %.
%total {} (inverse_ft_letb _ _) %.

The termination relation is really about the machine.

%sort frameterm_eq_f {_ frameterm Fs M} {_ -->r* Fs M nil V} {_ value V} %.
%mode frameterm_eq_f %in %out %out %.
%term frameterm_eq_f_val frameterm_eq_f (frameterm_val V) -->r*_ref V %.
%term frameterm_eq_f_app
  %pi (frameterm_eq_f (frameterm_app FT) (-->r*_step R evfs_app) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_tapp
  %pi (frameterm_eq_f (frameterm_tapp FT) (-->r*_step R evfs_tapp) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_letu
  %pi (frameterm_eq_f (frameterm_letu FT) (-->r*_step R evfs_letu) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_letb
  %pi (frameterm_eq_f (frameterm_letb FT) (-->r*_step R evfs_letb) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_lett
  %pi (frameterm_eq_f (frameterm_lett FT) (-->r*_step R evfs_lett) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_lam
  %pi (frameterm_eq_f (frameterm_lam FT) (-->r*_step R evfs_lam) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_tlam
  %pi (frameterm_eq_f (frameterm_tlam FT) (-->r*_step R evfs_tlam) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_tens
  %pi (frameterm_eq_f (frameterm_tens FT) (-->r*_step R evfs_tens) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_unit
  %pi (frameterm_eq_f (frameterm_unit FT) (-->r*_step R evfs_unit) V)
  %<- (frameterm_eq_f FT R V) %.
%term frameterm_eq_f_thunk
  %pi (frameterm_eq_f (frameterm_thunk FT) (-->r*_step R evfs_thunk) V)
  %<- (frameterm_eq_f FT R V) %.
%worlds () (frameterm_eq_f _ _ _) %.
%freeze frameterm_eq_f %.
%total D (frameterm_eq_f D _ _) %.
%sort frameterm_eq1 {_ frameterm Fs M} {_ -->* Fs M nil V} {_ value V} %.
%mode frameterm_eq1 %in %out %out %.
%term frameterm_eq1_rule
  %pi (frameterm_eq1 FT R V)
  %<- (frameterm_eq_f FT R' V)
  %<- (-->r*_to_-->*_lem R' R) %.
%worlds () (frameterm_eq1 _ _ _) %.
%freeze frameterm_eq1 %.
%total {} (frameterm_eq1 _ _ _) %.
%sort frameterm_eq2_r {_ -->r* Fs M nil V} {_ value V} {_ frameterm Fs M} %.
%mode frameterm_eq2_r %in %in %out %.
%term frameterm_eq2_r_ref frameterm_eq2_r -->r*_ref V (frameterm_val V) %.
%term frameterm_eq2_r_app
  %pi (frameterm_eq2_r (-->r*_step R evfs_app) V (frameterm_app F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_tapp
  %pi (frameterm_eq2_r (-->r*_step R evfs_tapp) V (frameterm_tapp F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_letu
  %pi (frameterm_eq2_r (-->r*_step R evfs_letu) V (frameterm_letu F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_letb
  %pi (frameterm_eq2_r (-->r*_step R evfs_letb) V (frameterm_letb F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_lett
  %pi (frameterm_eq2_r (-->r*_step R evfs_lett) V (frameterm_lett F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_lam
  %pi (frameterm_eq2_r (-->r*_step R evfs_lam) V (frameterm_lam F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_tlam
  %pi (frameterm_eq2_r (-->r*_step R evfs_tlam) V (frameterm_tlam F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_tens
  %pi (frameterm_eq2_r (-->r*_step R evfs_tens) V (frameterm_tens F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_unit
  %pi (frameterm_eq2_r (-->r*_step R evfs_unit) V (frameterm_unit F))
  %<- (frameterm_eq2_r R V F) %.
%term frameterm_eq2_r_thunk
  %pi (frameterm_eq2_r (-->r*_step R evfs_thunk) V (frameterm_thunk F))
  %<- (frameterm_eq2_r R V F) %.
%worlds () (frameterm_eq2_r _ _ _) %.
%freeze frameterm_eq2_r %.
%total D (frameterm_eq2_r D _ _) %.
%sort frameterm_eq2 {_ -->* Fs M nil V} {_ value V} {_ frameterm Fs M} %.
%mode frameterm_eq2 %in %in %out %.
%term frameterm_eq2_rule
  %pi (frameterm_eq2 R V F)
  %<- (-->*_to_-->r*_lem R R')
  %<- (frameterm_eq2_r R' V F) %.
%worlds () (frameterm_eq2 _ _ _) %.
%freeze frameterm_eq2 %.
%total {} (frameterm_eq2 _ _ _) %.
%sort eval_frameterm {_ M \n/ V} {_ frameterm nil M} %.
%mode eval_frameterm %in %out %.
%term eval_frameterm_rule
  %pi (eval_frameterm EV FT)
  %<- (value_soundness EV Vv)
  %<- (eq_eval_frame frameapply_nil EV R)
  %<- (frameterm_eq2 R Vv FT) %.
%worlds () (eval_frameterm _ _) %.
%freeze eval_frameterm %.
%total {} (eval_frameterm _ _) %.
%sort frameterm_eval {_ frameterm nil M} {_ M \n/ V} %.
%mode frameterm_eval %in %out %.
%term frameterm_eval_rule
  %pi (frameterm_eval FT EV)
  %<- (frameterm_eq1 FT R V)
  %<- (eq_frame_eval R V FA EV')
  %<- (frameapply_nil_eq FA Q)
  %<- (eq_sym Q Q')
  %<- (eq_eval Q' EV' EV) %.
%worlds () (frameterm_eval _ _) %.
%freeze frameterm_eval %.
%total {} (frameterm_eval _ _) %.

Excellent. We now know that termination in the frame stack semantics is the same as evaluation in the big step semantics. The nice thing about the termination relation is that it supplies us with an inductive description of termination.

Termination is invariant under evaluation

%sort lemma413a {_ -->* Fs M Fs' M'} {_ frameterm Fs M} {_ frameterm Fs' M'} %.
%mode lemma413a %in %in %out %.
%term lemma413a_ref lemma413a -->*_ref FT FT %.
%term lemma413a_thunk
  %pi (lemma413a (-->*_step R evfs_thunk) FT FT')
  %<- (lemma413a R FT (frameterm_thunk FT')) %.
%term lemma413a_app
  %pi (lemma413a (-->*_step R evfs_app) FT FT')
  %<- (lemma413a R FT (frameterm_app FT')) %.
%term lemma413a_tapp
  %pi (lemma413a (-->*_step R evfs_tapp) FT FT')
  %<- (lemma413a R FT (frameterm_tapp FT')) %.
%term lemma413a_letu
  %pi (lemma413a (-->*_step R evfs_letu) FT FT')
  %<- (lemma413a R FT (frameterm_letu FT')) %.
%term lemma413a_letb
  %pi (lemma413a (-->*_step R evfs_letb) FT FT')
  %<- (lemma413a R FT (frameterm_letb FT')) %.
%term lemma413a_lett
  %pi (lemma413a (-->*_step R evfs_lett) FT FT')
  %<- (lemma413a R FT (frameterm_lett FT')) %.
%term lemma413a_lam
  %pi (lemma413a (-->*_step R evfs_lam) FT FT')
  %<- (lemma413a R FT (frameterm_lam FT')) %.
%term lemma413a_tlam
  %pi (lemma413a (-->*_step R evfs_tlam) FT FT')
  %<- (lemma413a R FT (frameterm_tlam FT')) %.
%term lemma413a_tens
  %pi (lemma413a (-->*_step R evfs_tens) FT FT')
  %<- (lemma413a R FT (frameterm_tens FT')) %.
%term lemma413a_unit
  %pi (lemma413a (-->*_step R evfs_unit) FT FT')
  %<- (lemma413a R FT (frameterm_unit FT')) %.
%worlds () (lemma413a _ _ _) %.
%freeze lemma413a %.
%total D (lemma413a D _ _) %.
%sort lemma413b {_ -->r* Fs M Fs' M'} {_ frameterm Fs' M'} {_ frameterm Fs M} %.
%mode lemma413b %in %in %out %.
%term lemma413b_ref lemma413b -->r*_ref FT FT %.
%term lemma413b_thunk
  %pi (lemma413b (-->r*_step R evfs_thunk) FT (frameterm_thunk FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_app
  %pi (lemma413b (-->r*_step R evfs_app) FT (frameterm_app FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_tapp
  %pi (lemma413b (-->r*_step R evfs_tapp) FT (frameterm_tapp FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_letu
  %pi (lemma413b (-->r*_step R evfs_letu) FT (frameterm_letu FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_letb
  %pi (lemma413b (-->r*_step R evfs_letb) FT (frameterm_letb FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_lett
  %pi (lemma413b (-->r*_step R evfs_lett) FT (frameterm_lett FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_lam
  %pi (lemma413b (-->r*_step R evfs_lam) FT (frameterm_lam FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_tlam
  %pi (lemma413b (-->r*_step R evfs_tlam) FT (frameterm_tlam FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_tens
  %pi (lemma413b (-->r*_step R evfs_tens) FT (frameterm_tens FT'))
  %<- (lemma413b R FT FT') %.
%term lemma413b_unit
  %pi (lemma413b (-->r*_step R evfs_unit) FT (frameterm_unit FT'))
  %<- (lemma413b R FT FT') %.
%worlds () (lemma413b _ _ _) %.
%freeze lemma413b %.
%total D (lemma413b D _ _) %.
%sort lemma413c {_ -->* Fs M Fs' M'} {_ frameterm Fs' M'} {_ frameterm Fs M} %.
%mode lemma413c %in %in %out %.
%term lemma413b_rule %pi (lemma413c R FT FT') %<- (-->*_to_-->r*_lem R R') %<- (lemma413b R' FT FT') %.
%worlds () (lemma413c _ _ _) %.
%freeze lemma413c %.
%total {} (lemma413c _ _ _) %.

The Lily type system

Linearity

I encode linearity as a predicate on LF functions. Thus if linear([x].F) then we know that F is linear in x.

%sort linear {_ %pi term %-> term} %.
%name linear %.
% mode linear +E.
%term linear_id linear ([x] x) %.
%term linear_app1 %pi (linear ([x] app (E1 x) E2)) %<- (linear E1) %.
%term linear_app2 %pi (linear ([x] app E1 (E2 x))) %<- (linear E2) %.
%term linear_lam %pi (linear ([x] lam T ([y] E x y))) %<- ({y} linear ([x] E x y)) %.
%term linear_tlam %pi (linear ([x] tlam ([y] F x y))) %<- ({t tp} linear ([z] F z t)) %.
%term linear_tapp %pi (linear ([x] tapp (E x) T)) %<- (linear ([y] E y)) %.
% linear_thunk : No Rule as thunks have no free linear variables.
%term linear_letb1 %pi (linear ([x] letb (E1 x) E2)) %<- (linear E1) %.
%term linear_letb2 %pi (linear ([x] letb E1 ([y] E2 x y))) %<- ({y} linear ([x] E2 x y)) %.
% linear_unit : No Rule as units has no free linear variables.
%term linear_letu1 %pi (linear ([x] letu (E1 x) E2)) %<- (linear ([x] E1 x)) %.
%term linear_letu2 %pi (linear ([x] letu E1 (E2 x))) %<- (linear ([x] E2 x)) %.
%term linear_tens1 %pi (linear ([x] tens (E1 x) E2)) %<- (linear ([x] E1 x)) %.
%term linear_tens2 %pi (linear ([x] tens E1 (E2 x))) %<- (linear ([x] E2 x)) %.
%term linear_lett1 %pi (linear ([x] lett (E x) F)) %<- (linear ([x] E x)) %.
%term linear_lett2 %pi (linear ([x] lett E ([y] [z] F x y z))) %<- ({y} {z} linear ([x] F x y z)) %.
%block btlam {t tp}%.
%worlds (blam btlam) (linear _) %.
%freeze linear %.
%sort sub_linear {_ linear M1} {_ linear M2} {_ linear ([x] M1 (M2 x))} %.
%mode sub_linear %in %in %out %.
%term sub_linear_id sub_linear linear_id L2 L2 %.
%term sub_linear_app1 %pi (sub_linear (linear_app1 L1) L2 (linear_app1 L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_app2 %pi (sub_linear (linear_app2 L1) L2 (linear_app2 L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_lam
  %pi (sub_linear (linear_lam L1) L2 (linear_lam ([y] L3 y)))
  %<- ({y} sub_linear (L1 y) L2 (L3 y)) %.
%term sub_linear_tlam
  %pi (sub_linear (linear_tlam L1) L2 (linear_tlam ([t] L3 t)))
  %<- ({t} sub_linear (L1 t) L2 (L3 t)) %.
%term sub_linear_tapp %pi (sub_linear (linear_tapp L1) L2 (linear_tapp L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_letb1 %pi (sub_linear (linear_letb1 L1) L2 (linear_letb1 L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_letb2
  %pi (sub_linear (linear_letb2 L1) L2 (linear_letb2 L3))
  %<- ({y} sub_linear (L1 y) L2 (L3 y)) %.
%term sub_linear_letu1 %pi (sub_linear (linear_letu1 L1) L2 (linear_letu1 L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_letu2 %pi (sub_linear (linear_letu2 L1) L2 (linear_letu2 L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_lett1 %pi (sub_linear (linear_lett1 L1) L2 (linear_lett1 L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_lett2
  %pi (sub_linear (linear_lett2 L1) L2 (linear_lett2 L3))
  %<- ({y} {z} sub_linear (L1 y z) L2 (L3 y z)) %.
%term sub_linear_tens1 %pi (sub_linear (linear_tens1 L1) L2 (linear_tens1 L3)) %<- (sub_linear L1 L2 L3) %.
%term sub_linear_tens2 %pi (sub_linear (linear_tens2 L1) L2 (linear_tens2 L3)) %<- (sub_linear L1 L2 L3) %.
%block bsub_linear_lam1 {y term}%.
%block bsub_linear_lam2 {y tp}%.
%worlds (bsub_linear_lam1 bsub_linear_lam2) (sub_linear _ _ _) %.
%freeze sub_linear %.
%total D (sub_linear D _ _) %.

Some proofs are easier with relevance than with linearity.

%sort relavant {_ %pi term %-> term} %.
%name relavant %.
%mode relavant %in %.
%term relavant_id relavant ([x] x) %.
%term relavant_app1 %pi (relavant ([x] app (E1 x) (E2 x))) %<- (relavant E1) %.
%term relavant_app2 %pi (relavant ([x] app (E1 x) (E2 x))) %<- (relavant E2) %.
%term relavant_lam %pi (relavant ([x] lam T ([y] F x y))) %<- ({y} relavant ([x] F x y)) %.
%term relavant_tlam %pi (relavant ([x] tlam ([y] F x y))) %<- ({t tp} relavant ([z] F z t)) %.
%term relavant_tapp %pi (relavant ([x] tapp (E x) T)) %<- (relavant E) %.
%term relavant_letb1 %pi (relavant ([x] letb (E1 x) ([y] E2 x y))) %<- (relavant E1) %.
%term relavant_letb2 %pi (relavant ([x] letb (E1 x) ([y] E2 x y))) %<- ({y} relavant ([x] E2 x y)) %.
% linear_unit : No Rule as units has no free variables.
%term relavant_thunk %pi (relavant ([x] thunk T ([y] E x y))) %<- ({y} relavant ([x] E x y)) %.
%term relavant_letu1 %pi (relavant ([x] letu (E1 x) (E2 x))) %<- (relavant E1) %.
%term relavant_letu2 %pi (relavant ([x] letu (E1 x) (E2 x))) %<- (relavant ([x] E2 x)) %.
%term relavant_tens1 %pi (relavant ([x] tens (E1 x) (E2 x))) %<- (relavant E1) %.
%term relavant_tens2 %pi (relavant ([x] tens (E1 x) (E2 x))) %<- (relavant E2) %.
%term relavant_lett1 %pi (relavant ([x] lett (E1 x) ([y] [z] E2 x y z))) %<- (relavant E1) %.
%term relavant_lett2
  %pi (relavant ([x] lett (E1 x) ([y] [z] E2 x y z)))
  %<- ({y} {z} relavant ([x] E2 x y z)) %.
%worlds (blam btlam) (relavant _) %.
%freeze relavant %.
%sort linear_relavant {_ linear L} {_ relavant L} %.
%mode linear_relavant %in %out %.
%term linear_relavant_id linear_relavant linear_id relavant_id %.
%term linear_relavant_app1 %pi (linear_relavant (linear_app1 L) (relavant_app1 R)) %<- (linear_relavant L R) %.
%term linear_relavant_app2 %pi (linear_relavant (linear_app2 L) (relavant_app2 R)) %<- (linear_relavant L R) %.
%term linear_relavant_lam
  %pi (linear_relavant (linear_lam L) (relavant_lam R))
  %<- ({y} linear_relavant (L y) (R y)) %.
%term linear_relavant_tlam
  %pi (linear_relavant (linear_tlam L) (relavant_tlam R))
  %<- ({y} linear_relavant (L y) (R y)) %.
%term linear_relavant_tapp %pi (linear_relavant (linear_tapp L) (relavant_tapp R)) %<- (linear_relavant L R) %.
%term linear_relavant_letu1
  %pi (linear_relavant (linear_letu1 L) (relavant_letu1 R))
  %<- (linear_relavant L R) %.
%term linear_relavant_letu2
  %pi (linear_relavant (linear_letu2 L) (relavant_letu2 R))
  %<- (linear_relavant L R) %.
%term linear_relavant_letb1
  %pi (linear_relavant (linear_letb1 L) (relavant_letb1 R))
  %<- (linear_relavant L R) %.
%term linear_relavant_letb2
  %pi (linear_relavant (linear_letb2 L) (relavant_letb2 R))
  %<- ({y} linear_relavant (L y) (R y)) %.
%term linear_relavant_tens1
  %pi (linear_relavant (linear_tens1 L) (relavant_tens1 R))
  %<- (linear_relavant L R) %.
%term linear_relavant_tens2
  %pi (linear_relavant (linear_tens2 L) (relavant_tens2 R))
  %<- (linear_relavant L R) %.
%term linear_relavant_lett1
  %pi (linear_relavant (linear_lett1 L) (relavant_lett1 R))
  %<- (linear_relavant L R) %.
%term linear_relavant_lett2
  %pi (linear_relavant (linear_lett2 L) (relavant_lett2 R))
  %<- ({y} {z} linear_relavant (L y z) (R y z)) %.
%worlds (blam btlam) (linear_relavant _ _) %.
%freeze linear_relavant %.
%total D (linear_relavant D _) %.
%sort eq_relavant {_ {m} eq (R m) (R' m)} {_ relavant R} {_ relavant R'} %.
%mode eq_relavant %in %in %out %.
%term eq_relavant_rule eq_relavant ([m] eq_ref) R R %.
%worlds (blam) (eq_relavant _ _ _) %.
%freeze eq_relavant %.
%total {} (eq_relavant _ _ _) %.
%sort eq_linear {_ {m} eq (R m) (R' m)} {_ linear R} {_ linear R'} %.
%mode eq_linear %in %in %out %.
%term eq_linear_rule eq_linear ([m] eq_ref) R R %.
%worlds (blam) (eq_linear _ _ _) %.
%freeze eq_linear %.
%total {} (eq_linear _ _ _) %.

Typing rules

%sort ? {_ term} {_ tp} %.
% mode ? +M -T.
%name ? %.
%prec %none 500 ? %.
%term of_lam
  %pi (lam T ([x] M x) ? func T T')
  %<- ({x term} %pi (x ? T) %-> (M x ? T'))
  %<- (linear M) %.
%term of_app %pi (app M1 M2 ? T) %<- (M1 ? func T' T) %<- (M2 ? T') %.
%term of_tlam %pi (tlam M ? all T) %<- ({t tp} M t ? T t) %.
%term of_tapp {t tp} %pi (tapp M t ? T t) %<- (M ? all T) %.
%term of_thunk %pi (thunk T M ? bang T) %<- ({x} %pi (x ? T) %-> (M x ? T)) %.
%term of_letb %pi (letb M N ? T') %<- (M ? bang T) %<- ({x} %pi (x ? T) %-> (N x ? T')) %.
%term of_unit unit ? i %.
%term of_letu %pi (letu M N ? T) %<- (M ? i) %<- (N ? T) %.
%term of_tens %pi (tens M N ? tensor T T') %<- (M ? T) %<- (N ? T') %.
%term of_lett
  %pi (lett M N ? T'')
  %<- (M ? tensor T T')
  %<- ({x} %pi (x ? T) %-> ({y} %pi (y ? T') %-> (N x y ? T'')))
  %<- ({y} linear ([x] N x y))
  %<- ({x} linear ([y] N x y)) %.
%block blam_t [T tp] {x term} {u x ? T}%.
%block btlam_t {t tp}%.
%worlds (blam_t btlam_t) (? _ _) %.
%covers ? %in %out %.
%freeze ? %.

Take note of how I require functions and products to be linear.

Type preservation

As we have a type system we should prove soundness of it.

%sort tpres {_ M ? T} {_ M \n/ V} {_ V ? T} %.
%mode tpres %in %in %out %.
%term tpres_lam tpres (of_lam L D) ev_lam (of_lam L D) %.
%term tpres_tlam tpres (of_tlam D) ev_tlam (of_tlam D) %.
%term tpres_thunk tpres (of_thunk D) ev_thunk (of_thunk D) %.
%term tpres_unit tpres of_unit ev_unit of_unit %.
%term tpres_tens tpres (of_tens D' D) ev_tens (of_tens D' D) %.
%sort tpres_app_aux {_ lam T1 M ? func T3 T2} {_ {M'} %pi (M' ? T3) %-> (M M' ? T2)} %.
%mode tpres_app_aux %in %out %.
%term tpres_app_aux_rule tpres_app_aux (of_lam _ F) F %.
%worlds () (tpres_app_aux _ _) %.
%freeze tpres_app_aux %.
%total D (tpres_app_aux D _) %.
%term tpres_app
  %pi (tpres (of_app D2 D1) (ev_app E' E) D)
  %<- (tpres D1 E D')
  %<- (tpres_app_aux D' F)
  %<- (tpres (F _ D2) E' D) %.
%term tpres_tapp {D'' {t tp} M t ? T t}
  %pi (tpres (of_tapp _ D') (ev_tapp E' E) D)
  %<- (tpres D' E (of_tlam D''))
  %<- (tpres (D'' _) E' D) %.
%sort tpres_letb_aux {_ thunk T3 M ? bang T1} {_ {M'} %pi (M' ? T1) %-> (M M' ? T1)} %.
%mode tpres_letb_aux %in %out %.
%term tpres_letb_aux_rule tpres_letb_aux (of_thunk F) F %.
%worlds () (tpres_letb_aux _ _) %.
%freeze tpres_letb_aux %.
%total D (tpres_letb_aux D _) %.
%term tpres_letb
  %pi (tpres (of_letb D' D) (ev_letb E' E) D'')
  %<- (tpres D E DT)
  %<- (tpres_letb_aux DT Dt)
  %<- (tpres (D' _ (of_letb Dt DT)) E' D'') %.
%term tpres_letu %pi (tpres (of_letu D' _) (ev_letu E' _) D'') %<- (tpres D' E' D'') %.
%term tpres_lett
  %pi (tpres (of_lett _ _ D' D) (ev_lett E' E) D'')
  %<- (tpres D E (of_tens Dn Dm))
  %<- (tpres (D' _ Dm _ Dn) E' D'') %.
%worlds () (tpres _ _ _) %.
%freeze tpres %.
%total D (tpres _ D _) %.
%sort tpres_s {_ M ? T} {_ M \s/ V} {_ V ? T} %.
%mode tpres_s %in %in %out %.
%term tpres_s_lam tpres_s (of_lam L D) evs_lam (of_lam L D) %.
%term tpres_s_tlam tpres_s (of_tlam D) evs_tlam (of_tlam D) %.
%term tpres_s_thunk tpres_s (of_thunk D) evs_thunk (of_thunk D) %.
%term tpres_s_unit tpres_s of_unit evs_unit of_unit %.
%term tpres_s_tens tpres_s (of_tens D' D) evs_tens (of_tens D' D) %.
%sort tpres_s_app_aux {_ lam T1 M ? func T3 T2} {_ {M'} %pi (M' ? T3) %-> (M M' ? T2)} %.
%mode tpres_s_app_aux %in %out %.
%term tpres_s_app_aux_rule tpres_s_app_aux (of_lam _ F) F %.
%worlds () (tpres_s_app_aux _ _) %.
%freeze tpres_s_app_aux %.
%total D (tpres_s_app_aux D _) %.
%term tpres_s_app
  %pi (tpres_s (of_app D2 D1) (evs_app E3 E2 E1) D)
  %<- (tpres_s D1 E1 D')
  %<- (tpres_s_app_aux D' F)
  %<- (tpres_s D2 E2 D4)
  %<- (tpres_s (F _ D4) E3 D) %.
%term tpres_s_tapp {D'' {t tp} M t ? T t}
  %pi (tpres_s (of_tapp _ D') (evs_tapp E' E) D)
  %<- (tpres_s D' E (of_tlam D''))
  %<- (tpres_s (D'' _) E' D) %.
%sort tpres_s_letb_aux {_ thunk T3 M ? bang T1} {_ {M'} %pi (M' ? T1) %-> (M M' ? T1)} %.
%mode tpres_s_letb_aux %in %out %.
%term tpres_s_letb_aux_rule tpres_s_letb_aux (of_thunk F) F %.
%worlds () (tpres_s_letb_aux _ _) %.
%freeze tpres_s_letb_aux %.
%total D (tpres_s_letb_aux D _) %.
%term tpres_s_letb
  %pi (tpres_s (of_letb D' D) (evs_letb E' E) D'')
  %<- (tpres_s D E DT)
  %<- (tpres_s_letb_aux DT Dt)
  %<- (tpres_s (D' _ (of_letb Dt DT)) E' D'') %.
%term tpres_s_letu %pi (tpres_s (of_letu D' _) (evs_letu E' _) D'') %<- (tpres_s D' E' D'') %.
%term tpres_s_lett
  %pi (tpres_s (of_lett _ _ D' D) (evs_lett E' E) D'')
  %<- (tpres_s D E (of_tens Dn Dm))
  %<- (tpres_s (D' _ Dm _ Dn) E' D'') %.
%worlds () (tpres_s _ _ _) %.
%freeze tpres_s %.
%total D (tpres_s _ D _) %.

Equalities and inversions

%block bts_tlam {t tp}%.
%sort eq_typings {_ M ? T} {_ M ? T} %.
%mode eq_typings %in %out %.
%term eq_typings_ref eq_typings D D %.
%worlds (blam bts_tlam) (eq_typings _ _) %.
%freeze eq_typings %.
%total D (eq_typings D _) %.
%sort eq_type {_ eq M M'} {_ M ? T} {_ M' ? T} %.
%mode eq_type %in %in %out %.
%term eq_typing_rule eq_type eq_ref D D %.
%worlds () (eq_type _ _ _) %.
%freeze eq_type %.
%total {} (eq_type _ _ _) %.
%sort eq_type1 {_ eqt T1 T2} {_ M ? T1} {_ M ? T2} %.
%mode eq_type1 %in %in %out %.
%term eq_type1_rule eq_type1 eqt_ref D D %.
%worlds () (eq_type1 _ _ _) %.
%freeze eq_type1 %.
%total {} (eq_type1 _ _ _) %.
%sort inverse_lam {_ lam T M ? func T1 T2} {_ {a} %pi (a ? T1) %-> (M a ? T2)} {_ linear M} %.
%mode inverse_lam %in %out %out %.
%term inverse_lam_rule inverse_lam (of_lam L D) D L %.
%worlds () (inverse_lam _ _ _) %.
%total {} (inverse_lam _ _ _) %.
%sort inverse_tapp {_ tapp M T ? T'} {_ M ? all T1} %.
%mode inverse_tapp %in %out %.
%term inverse_tapp_rule inverse_tapp (of_tapp T D) D %.
%worlds () (inverse_tapp _ _) %.
%total {} (inverse_tapp _ _) %.
%sort eq_thunk_type {_ thunk T M ? bang T'} {_ eqt T T'} %.
%mode eq_thunk_type %in %out %.
%term eq_thunk_type_rule eq_thunk_type (of_thunk _) eqt_ref %.
%worlds () (eq_thunk_type _ _) %.
%freeze eq_thunk_type %.
%total {} (eq_thunk_type _ _) %.
%sort eq_val_funs {_ value M} {_ M ? func T1 T2} {_ eq M (lam T1 M')} %.
%mode eq_val_funs %in %in %out %.
%term eq_val_funs_rule eq_val_funs val_lam (of_lam _ _) eq_ref %.
%worlds () (eq_val_funs _ _ _) %.
%freeze eq_val_funs %.
%total {} (eq_val_funs _ _ _) %.
%sort eq_val_all {_ value M} {_ M ? all T1} {_ eq M (tlam M')} %.
%mode eq_val_all %in %in %out %.
%term eq_val_all_rule eq_val_all val_tlam (of_tlam _) eq_ref %.
%worlds () (eq_val_all _ _ _) %.
%freeze eq_val_all %.
%total {} (eq_val_all _ _ _) %.
%sort eq_val_unit {_ value M} {_ M ? i} {_ eq M unit} %.
%mode eq_val_unit %in %in %out %.
%term eq_val_unit_rule eq_val_unit val_unit of_unit eq_ref %.
%worlds () (eq_val_unit _ _ _) %.
%freeze eq_val_unit %.
%total {} (eq_val_unit _ _ _) %.
%sort eq_val_tensor {_ value M} {_ M ? tensor _ _} {_ eq M (tens M1 M2)} %.
%mode eq_val_tensor %in %in %out %.
%term eq_val_tensor_rule eq_val_tensor val_tens (of_tens _ _) eq_ref %.
%worlds () (eq_val_tensor _ _ _) %.
%freeze eq_val_tensor %.
%total {} (eq_val_tensor _ _ _) %.
%sort eq_val_bang {_ value M} {_ M ? bang _} {_ eq M (thunk T M')} %.
%mode eq_val_bang %in %in %out %.
%term eq_val_bang_rule eq_val_bang val_thunk (of_thunk _) eq_ref %.
%worlds () (eq_val_bang _ _ _) %.
%freeze eq_val_bang %.
%total {} (eq_val_bang _ _ _) %.

Abstract machine types

%sort fstp {_ framestack} {_ tp} {_ tp} %.
% mode fstp +FST +T -T'.
%name fstp %.
%term ftp_nil fstp nil T T %.
%term ftp_cons
  %pi (fstp (cons (%the (frame F') F) Fs) T T')
  %<- ({a} %pi (a ? T) %-> (F' a ? T''))
  %<- (fstp Fs T'' T') %.
%worlds () (fstp _ _ _) %.
%covers fstp %in %in %out %.
%freeze fstp %.
%sort eqf_fstp {_ eqf Fs Fs'} {_ fstp Fs T T'} {_ fstp Fs' T T'} %.
%mode eqf_fstp %in %in %out %.
%term eqf_fstp_rule eqf_fstp eqf_ref F F %.
%worlds (blam) (eqf_fstp _ _ _) %.
%freeze eqf_fstp %.
%total {} (eqf_fstp _ _ _) %.
%sort applysound {Fs framestack} {_ fstp Fs T T'} {_ M ? T} {_ frameapply Fs M M'} {_ M' ? T'} %.
%mode applysound %in %in %in %in %out %.
%term as_ftp_nil applysound nil ftp_nil D frameapply_nil D %.
%term as_ftp_cons_letb
  %pi (applysound (cons (fletb N) Fs) (ftp_cons FsT (%the ({m term} %pi (m ? T) %-> (letb m N ? T'')) Ft)) D1 (frameapply_cons Fap frameapp_app) D2)
  %<- (applysound Fs FsT (Ft M D1) Fap D2) %.
%term as_ftp_cons_app
  %pi (applysound (cons (fapp N) Fs) (ftp_cons FsT (%the ({m term} %pi (m ? T) %-> (app m N ? T'')) Ft)) D1 (frameapply_cons Fap frameapp_app) D2)
  %<- (applysound Fs FsT (Ft M D1) Fap D2) %.
%term as_ftp_cons_fletu
  %pi (applysound (cons (fletu N) Fs) (ftp_cons FsT (%the ({m term} %pi (m ? T) %-> (letu m N ? T'')) Ft)) D1 (frameapply_cons Fap frameapp_app) D2)
  %<- (applysound Fs FsT (Ft M D1) Fap D2) %.
%term as_ftp_cons_flett
  %pi (applysound (cons (flett N) Fs) (ftp_cons FsT (%the ({m term} %pi (m ? T) %-> (lett m N ? T'')) Ft)) D1 (frameapply_cons Fap frameapp_app) D2)
  %<- (applysound Fs FsT (Ft M D1) Fap D2) %.
%term as_ftp_cons_ftapp
  %pi (applysound (cons (ftapp T3) Fs) (ftp_cons FsT (%the ({m term} %pi (m ? T1) %-> (tapp m T3 ? T4)) Ft)) D1 (frameapply_cons Fap frameapp_app) D2)
  %<- (applysound Fs FsT (Ft M D1) Fap D2) %.
%worlds () (applysound _ _ _ _ _) %.
%freeze applysound %.
%total D (applysound D _ _ _ _) %.
%sort eqt_tapp {_ tapp M T ? T'} {_ M ? all T1} {_ eqt (T1 T) T'} %.
%mode eqt_tapp %in %out %out %.
%term eqt_tapp_rule eqt_tapp (of_tapp T D) D eqt_ref %.
%worlds () (eqt_tapp _ _ _) %.
%freeze eqt_tapp %.
%total {} (eqt_tapp _ _ _) %.

Preservation

Now I can prove soundness of the type system for the frame stack semantics:

%sort typed_step {_ fstp Fs T T'} {_ M ? T} {_ --> Fs M Fs' M'} {_ fstp Fs' T'' T'} {_ M' ? T''} %.
%mode typed_step %in %in %in %out %out %.
%term typed_step_letu %type d_step FsT (of_letu DN Di) evfs_letu (ftp_cons FsT ([a] [da] of_letu DN da)) Di %.
%term typed_step_letb %type d_step FsT (of_letb DN DM) evfs_letb (ftp_cons FsT ([a] [da] of_letb DN da)) DM %.
%term typed_step_lett %type d_step FsT (of_lett L1 L2 DN DM) evfs_lett (ftp_cons FsT ([a] [da] of_lett L1 L2 DN da)) DM %.
%term typed_step_fapp %type d_step FsT (of_app DN DM) evfs_app (ftp_cons FsT ([a] [da] of_app DN da)) DM %.
%term typed_step_ftapp %type d_step FsT (of_tapp T DM) evfs_tapp (ftp_cons FsT ([a] [da] of_tapp T da)) DM %.
%term typed_step_unit
  %pi (%type d_step (ftp_cons FsT Ft) of_unit evfs_unit FsT D)
  %<- (eq_typings (Ft unit of_unit) (of_letu D _)) %.
%term typed_step_lam
  %pi (%type d_step (ftp_cons FsT Ft) D1 evfs_lam FsT (D2 _ D))
  %<- (eq_typings (Ft _ D1) (of_app D (of_lam _ D2))) %.
%term typed_step_thunk
  %pi (%type d_step (ftp_cons FsT Ft) (of_thunk D1) evfs_thunk FsT (DN _ (of_letb DT (of_thunk DT))))
  %<- (eq_typings (Ft _ (of_thunk D1)) (of_letb DN (of_thunk DT))) %.
%term typed_step_tlam
  %pi (%type d_step (ftp_cons FsT Ft) D1 (%the (--> (cons (ftapp T1) Fs) _ _ _) evfs_tlam) FsT D5)
  %<- (eqt_tapp (Ft (tlam M1) D1) (of_tlam F) Q)
  %<- (eq_type1 Q (F T1) D5) %.
%term typed_step_tens
  %pi (%type d_step (ftp_cons FsT Ft) (of_tens D2 D1) evfs_tens FsT (D' M1 D1ss M2 D2ss))
  %<- (eq_typings (Ft (tens M1 M2) (of_tens D2 D1)) (of_lett L1 L2 D' (of_tens D2ss D1ss))) %.
%worlds () (typed_step _ _ _ _ _) %.
%freeze typed_step %.
%total {} (typed_step _ _ _ _ _) %.
%sort frame_pres_lem {_ -->r* Fs M Fs' M'} {_ fstp Fs T Te} {_ M ? T} {_ fstp Fs' T' Te} {_ M' ? T'} %.
%mode frame_pres_lem %in %in %in %out %out %.
%term frame_pres_lem_ref frame_pres_lem -->r*_ref FsTp D FsTp D %.
%term frame_pres_lem_step
  %pi (frame_pres_lem (-->r*_step Ss S) FsTp D FsTp' D')
  %<- (%type d_step FsTp D S FsTp'' D'')
  %<- (frame_pres_lem Ss FsTp'' D'' FsTp' D') %.
%worlds () (frame_pres_lem _ _ _ _ _) %.
%total Ss (frame_pres_lem Ss _ _ _ _) %.
%sort frame_pres {_ -->* Fs M Fs' M'} {_ fstp Fs T Te} {_ M ? T} {_ fstp Fs' T' Te} {_ M' ? T'} %.
%mode frame_pres %in %in %in %out %out %.
%term frame_pres_rule
  %pi (frame_pres Ss FsTp D FsTp' D')
  %<- (-->*_to_-->r*_lem Ss Ss')
  %<- (frame_pres_lem Ss' FsTp D FsTp' D') %.
%worlds () (frame_pres _ _ _ _ _) %.
%total Ss (frame_pres Ss _ _ _ _) %.

Progress

Progress and preservation seem to be in fashion. I will not rely on progress elsewhere.

%sort progress_good {_ framestack} {_ term} %.
%mode progress_good %in %in %.
%term progress_good_v %pi (progress_good nil V) %<- (value V) %.
%term progress_good_s %pi (progress_good Fs M) %<- (--> Fs M Fs' M') %.
%freeze progress_good %.
%sort frame_progress {F' frame F} {Fs} {_ F V ? T} {_ value V} {_ --> (cons F' Fs) V Fs M} %.
%mode frame_progress %in %in %in %in %out %.
%term frame_progress_app
  %pi (frame_progress (fapp M2) Fs (of_app D2 D1) V S)
  %<- (eq_val_funs V D1 Q)
  %<- (eq_sym Q Q')
  %<- (eq_step Q' evfs_lam S) %.
%term frame_progress_tapp
  %pi (frame_progress (ftapp T) Fs (of_tapp T D1) V S)
  %<- (eq_val_all V D1 Q)
  %<- (eq_sym Q Q')
  %<- (eq_step Q' evfs_tlam S) %.
%term frame_progress_lett
  %pi (frame_progress (flett M2) Fs (of_lett _ _ _ D1) V S)
  %<- (eq_val_tensor V D1 Q)
  %<- (eq_sym Q Q')
  %<- (eq_step Q' evfs_tens S) %.
%term frame_progress_letb
  %pi (frame_progress (fletb M2) Fs (of_letb _ D1) V S)
  %<- (eq_val_bang V D1 Q)
  %<- (eq_sym Q Q')
  %<- (eq_step Q' evfs_thunk S) %.
%term frame_progress_letu
  %pi (frame_progress (fletu M2) Fs (of_letu _ D1) V S)
  %<- (eq_val_unit V D1 Q)
  %<- (eq_sym Q Q')
  %<- (eq_step Q' evfs_unit S) %.
%worlds () (frame_progress _ _ _ _ _) %.
%total {} (frame_progress _ _ _ _ _) %.
%sort progress_val {_ fstp Fs T T'} {_ M ? T} {_ value M} {_ progress_good Fs M} %.
%mode progress_val %in %in %in %out %.
%term progress_nil_val progress_val ftp_nil D V (progress_good_v V) %.
%term progress_cons_rule
  %pi (progress_val (%the (fstp (cons F Fs) _ _) (ftp_cons FsTp Ftp)) D V (progress_good_s S))
  %<- (frame_progress F Fs (Ftp _ D) V S) %.
%worlds () (progress_val _ _ _ _) %.
%total {} (progress_val _ _ _ _) %.
%sort progress {_ fstp Fs T T'} {_ M ? T} {_ progress_good Fs M} %.
%mode progress %in %in %out %.
%term progress_lam %pi (progress FsTp D G) %<- (progress_val FsTp D val_lam G) %.
%term progress_tlam %pi (progress FsTp D G) %<- (progress_val FsTp D val_tlam G) %.
%term progress_thunk %pi (progress FsTp D G) %<- (progress_val FsTp D val_thunk G) %.
%term progress_tens %pi (progress FsTp D G) %<- (progress_val FsTp D val_tens G) %.
%term progress_unit %pi (progress FsTp D G) %<- (progress_val FsTp D val_unit G) %.
%term progress_app progress _ _ (progress_good_s evfs_app) %.
%term progress_tapp progress _ _ (progress_good_s evfs_tapp) %.
%term progress_letu progress _ _ (progress_good_s evfs_letu) %.
%term progress_letb progress _ _ (progress_good_s evfs_letb) %.
%term progress_lett progress _ _ (progress_good_s evfs_lett) %.
%worlds () (progress _ _ _) %.
%total {} (progress _ _ _) %.

Strictness lemma

Stack manipulations

There are two natural ways to define application of a frame stack to a term. I need them both and I need to show how they relate. As stacks are represented as lists this code is a nice example of how to prove classic theorems about lists.

%sort frameapply' {_ framestack} {_ term} {_ term} %.
%mode frameapply' %in %in %out %.
%term frameapply'_nil frameapply' nil M M %.
%term frameapply'_cons
  %pi (frameapply' (cons F Fs') M M')
  %<- (frameapply' Fs' M M'')
  %<- (frameapp F M'' M') %.
%worlds () (frameapply' _ _ _) %.
%freeze frameapply' %.
%total D (frameapply' D _ _) %.
%sort frameapply'_exists {Fs} {M} {_ frameapply' Fs M M'} %.
%mode frameapply'_exists %in %in %out %.
%term frameapply'_exists_nil frameapply'_exists nil M frameapply'_nil %.
%term frameapply'_exists_cons_letu
  %pi (frameapply'_exists (cons (fletu N) Fs) M (frameapply'_cons frameapp_app FsA))
  %<- (frameapply'_exists Fs M FsA) %.
%term frameapply'_exists_cons_letb
  %pi (frameapply'_exists (cons (fletb N) Fs) M (frameapply'_cons frameapp_app FsA))
  %<- (frameapply'_exists Fs M FsA) %.
%term frameapply'_exists_cons_lett
  %pi (frameapply'_exists (cons (flett N) Fs) M (frameapply'_cons frameapp_app FsA))
  %<- (frameapply'_exists Fs M FsA) %.
%term frameapply'_exists_cons_app
  %pi (frameapply'_exists (cons (fapp N) Fs) M (frameapply'_cons frameapp_app FsA))
  %<- (frameapply'_exists Fs M FsA) %.
%term frameapply'_exists_cons_tapp
  %pi (frameapply'_exists (cons (ftapp N) Fs) M (frameapply'_cons frameapp_app FsA))
  %<- (frameapply'_exists Fs M FsA) %.
%worlds (blam) (frameapply'_exists _ _ _) %.
%freeze frameapply'_exists %.
%total D (frameapply'_exists D _ _) %.
%sort frameapply'_eq {_ eqf Fs Fs'} {_ frameapply' Fs M FsM} {_ frameapply' Fs' M FsM} %.
%mode frameapply'_eq %in %in %out %.
%term frameapply'_eq_rule frameapply'_eq eqf_ref FA FA %.
%worlds (blam) (frameapply'_eq _ _ _) %.
%freeze frameapply'_eq %.
%total {} (frameapply'_eq _ _ _) %.
%sort frameapply'_nil_eq {_ frameapply' nil M M'} {_ eq M M'} %.
%mode frameapply'_nil_eq %in %out %.
%term frameapply'_nil_eq_rule frameapply'_nil_eq frameapply'_nil eq_ref %.
%worlds (blam) (frameapply'_nil_eq _ _) %.
%freeze frameapply'_nil_eq %.
%total {} (frameapply'_nil_eq _ _) %.
%sort revFs {_ framestack} {_ framestack} {_ framestack} %.
%mode revFs %in %in %out %.
%term revFs_nil revFs nil Fs' Fs' %.
%term revFs_cons %pi (revFs (cons F Fs) Fs'' Fs') %<- (revFs Fs (cons F Fs'') Fs') %.
%worlds () (revFs _ _ _) %.
%freeze revFs %.
%total D (revFs D _ _) %.
%sort revFs_exists {Fs} {Fs'} {_ revFs Fs Fs' Fs''} %.
%mode revFs_exists %in %in %out %.
%term revFs_exists_nil revFs_exists nil _ revFs_nil %.
%term revFs_exists_cons
  %pi (revFs_exists (cons F Fs) Fs' (revFs_cons Fs''))
  %<- (revFs_exists Fs (cons F Fs') Fs'') %.
%worlds (blam) (revFs_exists _ _ _) %.
%freeze revFs_exists %.
%total D (revFs_exists D _ _) %.
%sort revDet {_ revFs Fs Fs' Fs3} {_ revFs Fs Fs' Fs4} {_ eqf Fs3 Fs4} %.
%mode revDet %in %in %out %.
%term revDet_nil revDet revFs_nil _ eqf_ref %.
%term revDet_cons %pi (revDet (revFs_cons R) (revFs_cons R') Q) %<- (revDet R R' Q) %.
%worlds (blam) (revDet _ _ _) %.
%freeze revDet %.
%total D (revDet D _ _) %.
%sort revrev_id_lem {_ revFs Fs Fs' Fs''} {_ revFs Fs'' nil Fs4} {_ revFs Fs' Fs Fs6} {_ eqf Fs6 Fs4} %.
%mode revrev_id_lem %in %in %in %out %.
%term revrev_id_lem_nil %pi (revrev_id_lem revFs_nil F F' Q) %<- (revDet F' F Q) %.
%term revrev_id_lem_cons
  %pi (revrev_id_lem (revFs_cons R) R' R'' Q)
  %<- (revrev_id_lem R R' (revFs_cons R'') Q) %.
%worlds (blam) (revrev_id_lem _ _ _ _) %.
%freeze revrev_id_lem %.
%total D (revrev_id_lem D _ _ _) %.
%sort revrev_id {_ revFs Fs nil Fs'} {_ revFs Fs' nil Fs''} {_ eqf Fs Fs''} %.
%mode revrev_id %in %in %out %.
%term revrev_id_rule %pi (revrev_id R R' Q) %<- (revrev_id_lem R R' revFs_nil Q) %.
%worlds (blam) (revrev_id _ _ _) %.
%freeze revrev_id %.
%total {} (revrev_id _ _ _) %.
%sort rev_injective {_ revFs Fs nil Fs'} {_ revFs Fs'' nil Fs'} {_ eqf Fs Fs''} %.
%mode rev_injective %in %in %out %.
%term rev_injective_rule
  %pi (rev_injective (%the (revFs Fs nil Fs') R) R' Q)
  %<- (revFs_exists Fs' nil Rev)
  %<- (revrev_id R Rev Q')
  %<- (eqf_symm Q' Q''')
  %<- (revrev_id R' Rev Q'')
  %<- (eqf_trans Q'' Q''' Q1)
  %<- (eqf_symm Q1 Q) %.
%worlds (blam) (rev_injective _ _ _) %.
%freeze rev_injective %.
%total D (rev_injective D _ _) %.
%sort rev_eq1 {_ eqf Fs Fs'} {_ revFs Fs F1 F2} {_ revFs Fs' F1 F2} %.
%mode rev_eq1 %in %in %out %.
%term rev_eq1_rule rev_eq1 eqf_ref R R %.
%worlds (blam) (rev_eq1 _ _ _) %.
%freeze rev_eq1 %.
%total {} (rev_eq1 _ _ _) %.
%sort rev_eq2 {_ eqf Fs Fs'} {_ revFs F1 F2 Fs} {_ revFs F1 F2 Fs'} %.
%mode rev_eq2 %in %in %out %.
%term rev_eq2_rule rev_eq2 eqf_ref R R %.
%worlds (blam) (rev_eq2 _ _ _) %.
%freeze rev_eq2 %.
%total {} (rev_eq2 _ _ _) %.
%sort frameapply_e {_ revFs Fs Fs' Fs''} {_ frameapply' Fs' M M''} {_ frameapply Fs M'' M'} {_ frameapply' Fs'' M M'} %.
%mode frameapply_e %in %in %in %out %.
%term frameapply_e_nil frameapply_e revFs_nil FA frameapply_nil FA %.
%term frameapply_e_cons
  %pi (frameapply_e (revFs_cons R) FA' (frameapply_cons FA frameapp_app) FA'')
  %<- (frameapply_e R (frameapply'_cons frameapp_app FA') FA FA'') %.
%worlds (blam) (frameapply_e _ _ _ _) %.
%freeze frameapply_e %.
%total D (frameapply_e _ _ D _) %.
%sort frameapply_e2 {_ revFs Fs nil Fs'} {_ frameapply Fs M M'} {_ frameapply' Fs' M M'} %.
%mode frameapply_e2 %in %in %out %.
%term frameapply_e2_rule %pi (frameapply_e2 R FA' FA) %<- (frameapply_e R frameapply'_nil FA' FA) %.
%worlds (blam) (frameapply_e2 _ _ _) %.
%freeze frameapply_e2 %.
%total {} (frameapply_e2 _ _ _) %.
%sort frameapply'_e {_ revFs Fs Fs' Fs'''} {_ revFs Fs''' nil Fs''} {_ frameapply' Fs' M M''} {_ frameapply Fs M'' M'} {_ frameapply Fs'' M M'} %.
%mode frameapply'_e %in %in %in %in %out %.
%term frameapply'_e_nil
  %pi (frameapply'_e R R' frameapply'_nil FA FA')
  %<- (revrev_id R R' Q)
  %<- (frameapply_eq Q FA FA') %.
%term frameapply'_e_cons
  %pi (frameapply'_e R R' (frameapply'_cons frameapp_app FA') FA FA'')
  %<- (frameapply'_e (revFs_cons R) R' FA' (frameapply_cons FA frameapp_app) FA'') %.
%worlds (blam) (frameapply'_e _ _ _ _ _) %.
%freeze frameapply'_e %.
%total D (frameapply'_e _ _ D _ _) %.
%sort frameapply_e1 {_ revFs Fs nil Fs'} {_ frameapply' Fs M M'} {_ frameapply Fs' M M'} %.
%mode frameapply_e1 %in %in %out %.
%term frameapply_e1_rule
  %pi (frameapply_e1 R FA' FA)
  %<- (frameapply'_e revFs_nil R FA' frameapply_nil FA) %.
%worlds (blam) (frameapply_e1 _ _ _) %.
%freeze frameapply_e1 %.
%total {} (frameapply_e1 _ _ _) %.

Some degenerate lemmas

The next lemma is degenerate and needed to take care of other degenerate cases.

%sort lem45 {M %pi term %-> term} {_ {m term} frameapply' (Fs m) (N m) R} {_ {m term} frameapply' (Fs m) (M (N m)) R'} %.
%mode lem45 %in %in %out %.
%term lem45_nil lem45 _ ([m] frameapply'_nil) ([m] frameapply'_nil) %.
%term lem45_app
  %pi (lem45 M ([m] frameapply'_cons (%the (frameapp (fapp _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem45 M FA FA') %.
%term lem45_tapp
  %pi (lem45 M ([m] frameapply'_cons (%the (frameapp (ftapp _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem45 M FA FA') %.
%term lem45_letb
  %pi (lem45 M ([m] frameapply'_cons (%the (frameapp (fletb _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem45 M FA FA') %.
%term lem45_lett
  %pi (lem45 M ([m] frameapply'_cons (%the (frameapp (flett _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem45 M FA FA') %.
%term lem45_letu
  %pi (lem45 M ([m] frameapply'_cons (%the (frameapp (fletu _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem45 M FA FA') %.
%worlds (blam) (lem45 _ _ _) %.
%freeze lem45 %.
%total D (lem45 _ D _) %.

Frames are linear

%sort redex {_ term} {_ term} %.
%name redex %.
% mode redex +M +M'.
%term redex_app redex (app (lam T M1) M2) (M1 M2) %.
%term redex_tapp redex (tapp (tlam M) T) (M T) %.
%term redex_lett redex (lett (tens M1 M2) M3) (M3 M1 M2) %.
%term redex_letu redex (letu unit M) M %.
%term redex_letb redex (letb (thunk T M1) M2) (M2 (letb (thunk T M1) M1)) %.
%freeze redex %.
%sort ctp %.
%term ctp_0 ctp %.
%term ctp_1 %pi (linear M) %-> ctp %.
%term ctp_2
  %pi ({m term} linear ([n term] M n m))
  %-> ({m term} linear ([n term] M m n))
  %-> ctp %.
%freeze ctp %.
%sort redex_tp {_ {m term} redex (M m) (M' m)} {_ ctp} %.
%term redex_tp_app {L linear (M N)} redex_tp ([m term] %the (redex (app (lam T (M m)) (M2 m)) _) redex_app) (ctp_1 L) %.
%term redex_tp_tapp redex_tp ([m] %the (redex (tapp (tlam (M m)) T) (M m T)) redex_tapp) ctp_0 %.
%term redex_tp_lett {L1 {m term} linear ([n term] M3 N n m)} {L2 {m term} linear ([n term] M3 N m n)} redex_tp ([m term] %the (redex (lett (tens (M1 m) (M2 m)) (M3 m)) _) redex_lett) (ctp_2 L1 L2) %.
%term redex_tp_letu redex_tp ([m] redex_letu) ctp_0 %.
%term redex_tp_letb redex_tp ([m] %the (redex (letb (thunk T (M1 m)) (M2 m)) (M2 m (letb (thunk T (M1 m)) (M1 m)))) redex_letb) ctp_0 %.
%freeze redex_tp %.
%sort lem33 {_ {m term} redex (M m) (M' m)} {_ {m term} frameapply' (Fs m) (M m) R} {_ {m term} frameapply' (Fs m) (M' m) R'} %.
%mode lem33 %in %in %out %.
%term lem33_nil lem33 C ([m] frameapply'_nil) ([m] frameapply'_nil) %.
%term lem33_app
  %pi (lem33 C ([m] frameapply'_cons (%the (frameapp (fapp _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem33 C FA FA') %.
%term lem33_tapp
  %pi (lem33 C ([m] frameapply'_cons (%the (frameapp (ftapp _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem33 C FA FA') %.
%term lem33_letb
  %pi (lem33 C ([m] frameapply'_cons (%the (frameapp (fletb _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem33 C FA FA') %.
%term lem33_lett
  %pi (lem33 C ([m] frameapply'_cons (%the (frameapp (flett _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem33 C FA FA') %.
%term lem33_letu
  %pi (lem33 C ([m] frameapply'_cons (%the (frameapp (fletu _) _ _) frameapp_app) (FA m)) ([m] frameapply'_cons frameapp_app (FA' m)))
  %<- (lem33 C FA FA') %.
%worlds (blam) (lem33 _ _ _) %.
%total D (lem33 _ D _) %.
%sort lem31 {_ {m term} value (M m)} {_ {a term} frameapply' (Fs a) (N a) (M a)} {_ {a} eq (N a) (M a)} %.
%mode lem31 %in %in %out %.
%term lem31_rule lem31 _ ([m] frameapply'_nil) ([m] eq_ref) %.
%worlds (blam) (lem31 _ _ _) %.
%total {} (lem31 _ _ _) %.
%sort lem32 {Fs} {M} {_ {m} value (B m)} {_ {m term} redex (N1 m) (N2 m)} {_ {m term} eq (N1 m) (B m)} {_ {m term} frameapply' (Fs m) (N2 m) (M m)} %.
%mode lem32 %in %in %in %in %in %out %.
%worlds (blam) (lem32 _ _ _ _ _ _) %.
%total {} (lem32 _ _ _ _ _ _) %.
%sort lem34 {_ {a term} frameapply' (Fs a) (N a) a} {_ {a} eqf (Fs a) nil} %.
%mode lem34 %in %out %.
%term lem34_rule lem34 ([m] frameapply'_nil) ([m] eqf_ref) %.
%worlds (blam) (lem34 _ _) %.
%total {} (lem34 _ _) %.
%sort lem35 {Fs} {M} {_ {m term} redex (N1 m) (N2 m)} {_ {m term} eq (N1 m) m} {_ {m term} frameapply' (Fs m) (N2 m) (M m)} %.
%mode lem35 %in %in %in %in %out %.
%worlds (blam) (lem35 _ _ _ _ _) %.
%total {} (lem35 _ _ _ _ _) %.

Here I am building up rather technical lemmas that are needed in the strictness lemma. Take note of how easy it is to deal with linearity.

%sort frame_linear_lem2 {_ redex_tp (%the ({m term} redex (M m) (M' m)) C) Ct} {_ {m term} frameapply' (Fs m) (M m) (R m)} {_ linear R} {_ {m} frameapply' (Fs m) (M' m) (R' m)} {_ linear R'} %.
%mode frame_linear_lem2 %in %in %in %out %out %.
%term frame_linear_lem2_nil1 frame_linear_lem2 _ ([m] %the (frameapply' _ (app _ M2) _) frameapply'_nil) (linear_app1 (linear_lam L)) ([m] frameapply'_nil) (L M2) %.
%term frame_linear_lem2_nil2
  %pi (frame_linear_lem2 (redex_tp_app L2) ([m] %the (frameapply' _ (app _ (M' m)) _) frameapply'_nil) (linear_app2 L) ([m] frameapply'_nil) L')
  %<- (sub_linear L2 L L') %.
%term frame_linear_tens_lem2_nil1
  %pi (frame_linear_lem2 (redex_tp_lett L1 L2) ([m] %the (frameapply' _ (lett (tens _ M2) M3) _) frameapply'_nil) (linear_lett1 (linear_tens1 L)) ([m] frameapply'_nil) L')
  %<- (sub_linear (L1 M2) L L') %.
%term frame_linear_tens_lem2_nil2
  %pi (frame_linear_lem2 (redex_tp_lett L1 L2) ([m] %the (frameapply' _ (lett (tens M1 _) M3) _) frameapply'_nil) (linear_lett1 (linear_tens2 L)) ([m] frameapply'_nil) L')
  %<- (sub_linear (L2 M1) L L') %.
%term frame_linear_tens_lem2_nil3 frame_linear_lem2 C ([m] %the (frameapply' _ (lett (tens M1 M2) (M3 m)) _) frameapply'_nil) (linear_lett2 L) ([m] frameapply'_nil) (L M1 M2) %.
%term frame_linear_unit_lem_nil2 frame_linear_lem2 C ([m] %the (frameapply' _ (letu unit (M3 m)) _) frameapply'_nil) (linear_letu2 L) ([m] frameapply'_nil) L %.
%term frame_linear_thunk_lem_nil2 frame_linear_lem2 C ([m] %the (frameapply' _ (letb (thunk T M1) (M2 m)) _) frameapply'_nil) (linear_letb2 L) ([m] frameapply'_nil) (L (letb (thunk T M1) M1)) %.
%term frame_linear_tlam_lem_nil1 frame_linear_lem2 C ([m] %the (frameapply' _ (tapp _ T) _) frameapply'_nil) (linear_tapp (linear_tlam L)) ([m] frameapply'_nil) (L T) %.
%term frame_linear_cons_app1
  %pi (frame_linear_lem2 C ([m] frameapply'_cons (%the (frameapp (fapp M2) (M1 m) _) frameapp_app) (FA m)) (linear_app1 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_app1 L'))
  %<- (frame_linear_lem2 C FA L FA' L') %.
%term frame_linear_cons_tapp1
  %pi (frame_linear_lem2 C ([m] frameapply'_cons (%the (frameapp (ftapp T) (M1 m) _) frameapp_app) (FA m)) (linear_tapp L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_tapp L'))
  %<- (frame_linear_lem2 C FA L FA' L') %.
%term frame_linear_cons_letu1
  %pi (frame_linear_lem2 C ([m] frameapply'_cons (%the (frameapp (fletu T) (M1 m) _) frameapp_app) (FA m)) (linear_letu1 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_letu1 L'))
  %<- (frame_linear_lem2 C FA L FA' L') %.
%term frame_linear_cons_letb1
  %pi (frame_linear_lem2 C ([m] frameapply'_cons (%the (frameapp (fletb T) (M1 m) _) frameapp_app) (FA m)) (linear_letb1 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_letb1 L'))
  %<- (frame_linear_lem2 C FA L FA' L') %.
%term frame_linear_cons_lett1
  %pi (frame_linear_lem2 C ([m] frameapply'_cons (%the (frameapp (flett T) (M1 m) _) frameapp_app) (FA m)) (linear_lett1 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_lett1 L'))
  %<- (frame_linear_lem2 C FA L FA' L') %.
%term frame_linear_cons_letu2
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) ([m] frameapply'_cons (%the (frameapp (fletu (M2 m)) M1 _) frameapp_app) (FA m)) (linear_letu2 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_letu2 L))
  %<- (lem33 C' FA FA') %.
%term frame_linear_cons_letb2
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) ([m] frameapply'_cons (%the (frameapp (fletb (M2 m)) M1 _) frameapp_app) (FA m)) (linear_letb2 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_letb2 L))
  %<- (lem33 C' FA FA') %.
%term frame_linear_cons_lett2
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) ([m] frameapply'_cons (%the (frameapp (flett (M2 m)) M1 _) frameapp_app) (FA m)) (linear_lett2 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_lett2 L))
  %<- (lem33 C' FA FA') %.
%term frame_linear_cons_app2
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) ([m] frameapply'_cons (%the (frameapp (fapp (M2 m)) M1 _) frameapp_app) (FA m)) (linear_app2 L) ([m] frameapply'_cons frameapp_app (FA' m)) (linear_app2 L))
  %<- (lem33 C' FA FA') %.
%term frame_linear_cons_tens1
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) (%the ({m} frameapply' (Fs m) (M1 m) (tens (M3 m) M4)) FA) (linear_tens1 L) FA' (linear_tens1 L))
  %<- (lem31 ([m] val_tens) FA Q)
  %<- (lem32 Fs ([m] tens (M3 m) M4) ([m] val_tens) C' Q FA') %.
%term frame_linear_cons_tens2
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) (%the ({m} frameapply' (Fs m) (M1 m) (tens M3 (M4 m))) FA) (linear_tens2 L) FA' (linear_tens2 L))
  %<- (lem31 ([m] val_tens) FA Q)
  %<- (lem32 Fs ([m] tens M3 (M4 m)) ([m] val_tens) C' Q FA') %.
%term frame_linear_cons_tlam
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) (%the ({m} frameapply' (Fs m) (M1 m) (tlam (M4 m))) FA) (linear_tlam L) FA' (linear_tlam L))
  %<- (lem31 ([m] val_tlam) FA Q)
  %<- (lem32 Fs ([m] tlam (M4 m)) ([m] val_tlam) C' Q FA') %.
%term frame_linear_cons_lam_lem2
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) (%the ({m term} frameapply' (Fs m) (M1 m) (lam T1 (M4 m))) FA) (linear_lam L) FA' (linear_lam L))
  %<- (lem31 ([m] val_lam) FA Q)
  %<- (lem32 Fs ([m] lam T1 (M4 m)) ([m] val_lam) C' Q FA') %.
%term frame_linear_lam_lem2_id
  %pi (frame_linear_lem2 (%the (redex_tp C' _) C) (%the ({m} frameapply' (Fs m) (M1 m) m) FA) linear_id FA' linear_id)
  %<- (lem34 FA Q)
  %<- ({m} frameapply'_eq (Q m) (FA m) (FA'' m))
  %<- ({m} frameapply'_nil_eq (FA'' m) (Q' m))
  %<- (lem35 Fs ([m] m) C' Q' FA') %.
%worlds (blam) (frame_linear_lem2 _ _ _ _ _) %.
%total FA (frame_linear_lem2 _ FA _ _ _) %.
%sort frame_linear_lem1 {_ redex_tp (%the ({m term} redex (M m) (M' m)) C) Ct} {_ {m term} frameapply (Fs m) (M m) (R m)} {_ linear R} {_ {m} frameapply (Fs m) (M' m) (R' m)} {_ linear R'} %.
%mode frame_linear_lem1 %in %in %in %out %out %.
%term frame_linear_lem1_rule
  %pi (frame_linear_lem1 C (%the ({m} frameapply (Fs m) _ _) FA) LR FA' LR')
  %<- ({m} revFs_exists (Fs m) nil (%the (revFs (Fs m) nil (Fs' m)) (Rev m)))
  %<- ({m} frameapply_e2 (Rev m) (FA m) (FA'' m))
  %<- (frame_linear_lem2 C FA'' LR FA3 LR')
  %<- ({m} revFs_exists (Fs' m) nil (Rev' m))
  %<- ({m} revrev_id (Rev m) (Rev' m) (Q m))
  %<- ({m} frameapply_e1 (Rev' m) (FA3 m) (FA4 m))
  %<- ({m} eqf_symm (Q m) (Q' m))
  %<- ({m} frameapply_eq (Q' m) (FA4 m) (FA' m)) %.
%worlds (blam) (frame_linear_lem1 _ _ _ _ _) %.
%total {} (frame_linear_lem1 _ _ _ _ _) %.
%sort frame_linear {_ {m} redex (M m) (M' m)} {_ M A ? T} {_ {m term} frameapply (Fs m) (M m) (R m)} {_ linear R} {_ {m} frameapply (Fs m) (M' m) (R' m)} {_ linear R'} %.
%mode frame_linear %in %in %in %in %out %out %.
%term frame_linear_app
  %pi (frame_linear ([m] redex_app) (of_app D2 (of_lam LM _)) FA LR FA' LR')
  %<- (frame_linear_lem1 (%the (redex_tp ([m term] %the (redex (app (lam T (M1 m)) _) _) redex_app) _) (redex_tp_app LM)) FA LR FA' LR') %.
%term frame_linear_lett
  %pi (frame_linear ([m] redex_lett) (of_lett L1 L2 _ _) FA LR FA' LR')
  %<- (frame_linear_lem1 (%the (redex_tp ([m term] %the (redex (lett (tens (M1 m) (M2 m)) (M3 m)) _) redex_lett) _) (redex_tp_lett L2 L1)) FA LR FA' LR') %.
%term frame_linear_letu
  %pi (frame_linear ([m] redex_letu) _ FA LR FA' LR')
  %<- (frame_linear_lem1 redex_tp_letu FA LR FA' LR') %.
%term frame_linear_letb
  %pi (frame_linear ([m] redex_letb) _ FA LR FA' LR')
  %<- (frame_linear_lem1 redex_tp_letb FA LR FA' LR') %.
%term frame_linear_tapp
  %pi (frame_linear ([m] redex_tapp) _ FA LR FA' LR')
  %<- (frame_linear_lem1 redex_tp_tapp FA LR FA' LR') %.
%worlds () (frame_linear _ _ _ _ _ _) %.
%total {} (frame_linear _ _ _ _ _ _) %.

Termination is invariant to redexes

%sort add_redex_steps {_ redex M M'} {_ frameterm Fs M'} {_ frameterm Fs M} %.
%mode add_redex_steps %in %in %out %.
%term add_redex_steps_app add_redex_steps redex_app Ft (frameterm_app (frameterm_lam Ft)) %.
%term add_redex_steps_tapp add_redex_steps redex_tapp Ft (frameterm_tapp (frameterm_tlam Ft)) %.
%term add_redex_steps_lett add_redex_steps redex_lett Ft (frameterm_lett (frameterm_tens Ft)) %.
%term add_redex_steps_letu add_redex_steps redex_letu Ft (frameterm_letu (frameterm_unit Ft)) %.
%term add_redex_steps_letb add_redex_steps redex_letb Ft (frameterm_letb (frameterm_thunk Ft)) %.
%worlds () (add_redex_steps _ _ _) %.
%total {} (add_redex_steps _ _ _) %.
%sort lem42 {Fs} {N} {_ redex M M'} {_ frameterm (Fs M') (N M')} {_ frameterm (Fs M) (N M)} %.
%mode lem42 %in %in %in %in %out %.
%term lem42_val
  %pi (lem42 ([a] nil) ([a] a) R (frameterm_val V) Ft)
  %<- (add_redex_steps R (frameterm_val V) Ft) %.
%term lem42_base1 lem42 ([a term] nil) ([a] lam T _) _ (frameterm_val _) (frameterm_val val_lam) %.
%term lem42_base2 lem42 ([a term] nil) ([a] tlam _) _ (frameterm_val _) (frameterm_val val_tlam) %.
%term lem42_base3 lem42 ([a term] nil) ([a] tens _ _) _ (frameterm_val _) (frameterm_val val_tens) %.
%term lem42_base4 lem42 ([a term] nil) ([a] thunk T _) _ (frameterm_val _) (frameterm_val val_thunk) %.
%term lem42_base5 lem42 ([a term] nil) ([a] unit) _ (frameterm_val _) (frameterm_val val_unit) %.
%term lem42_app
  %pi (lem42 Fs ([a] a) R (frameterm_app Ft) Ft')
  %<- (lem42 ([a] cons (fapp M2) (Fs a)) ([a] M1) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_app Ft'') Ft') %.
%term lem42_tapp
  %pi (lem42 Fs ([a] a) R (frameterm_tapp Ft) Ft')
  %<- (lem42 ([a] cons (ftapp T) (Fs a)) ([a] M1) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_tapp Ft'') Ft') %.
%term lem42_lett
  %pi (lem42 Fs ([a] a) R (frameterm_lett Ft) Ft')
  %<- (lem42 ([a] cons (flett T) (Fs a)) ([a] M1) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_lett Ft'') Ft') %.
%term lem42_letu
  %pi (lem42 Fs ([a] a) R (frameterm_letu Ft) Ft')
  %<- (lem42 ([a] cons (fletu T) (Fs a)) ([a] M1) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_letu Ft'') Ft') %.
%term lem42_letb
  %pi (lem42 Fs ([a] a) R (frameterm_letb Ft) Ft')
  %<- (lem42 ([a] cons (fletb T) (Fs a)) ([a] M1) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_letb Ft'') Ft') %.
%term lem42_unit
  %pi (lem42 ([a] cons (fletu (M2 a)) (Fs a)) ([a] a) R (frameterm_unit Ft) Ft')
  %<- (lem42 Fs ([a] M2 a) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_unit Ft'') Ft') %.
%term lem42_tlam
  %pi (lem42 ([a] cons (ftapp T) (Fs a)) ([a] a) R (%the (frameterm _ (tlam M)) (frameterm_tlam Ft)) Ft')
  %<- (lem42 Fs ([a] M T) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_tlam Ft'') Ft') %.
%term lem42_lam
  %pi (lem42 ([a] cons (fapp (M2 a)) (Fs a)) ([a] a) R (%the (frameterm _ (lam T M1')) (frameterm_lam Ft)) Ft')
  %<- (lem42 Fs ([a] M1' (M2 a)) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_lam Ft'') Ft') %.
%term lem42_tens
  %pi (lem42 ([a] cons (flett (M3 a)) (Fs a)) ([a] a) R (%the (frameterm _ (tens M1 M2)) (frameterm_tens Ft)) Ft')
  %<- (lem42 Fs ([a] M3 a M1 M2) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_tens Ft'') Ft') %.
%term lem42_thunk
  %pi (lem42 ([a] cons (fletb (M2 a)) (Fs a)) ([a] a) R (%the (frameterm _ (thunk T M1)) (frameterm_thunk Ft)) Ft')
  %<- (lem42 Fs ([a] M2 a (letb (thunk T M1) M1)) R Ft Ft'')
  %<- (add_redex_steps R (frameterm_thunk Ft'') Ft') %.
%term lem42_lam2
  %pi (lem42 ([a] cons (fapp (M2 a)) (Fs a)) ([a] lam T (M1' a)) R (frameterm_lam Ft) (frameterm_lam Ft'))
  %<- (lem42 Fs ([a] M1' a (M2 a)) R Ft Ft') %.
%term lem42_tens2
  %pi (lem42 ([a] cons (flett (M3 a)) (Fs a)) ([a] tens (M1 a) (M2 a)) R (frameterm_tens Ft) (frameterm_tens Ft'))
  %<- (lem42 Fs ([a] M3 a (M1 a) (M2 a)) R Ft Ft') %.
%term lem42_tlam2
  %pi (lem42 ([a] cons (ftapp T) (Fs a)) ([a] tlam (M1' a)) R (frameterm_tlam Ft) (frameterm_tlam Ft'))
  %<- (lem42 Fs ([a] M1' a T) R Ft Ft') %.
%term lem42_unit2
  %pi (lem42 ([a] cons (fletu (M2 a)) (Fs a)) ([a] unit) R (frameterm_unit Ft) (frameterm_unit Ft'))
  %<- (lem42 Fs ([a] M2 a) R Ft Ft') %.
%term lem42_thunk2
  %pi (lem42 ([a] cons (fletb (M2 a)) (Fs a)) ([a] thunk T (M1 a)) R (frameterm_thunk Ft) (frameterm_thunk Ft'))
  %<- (lem42 Fs ([a] M2 a (letb (thunk T (M1 a)) (M1 a))) R Ft Ft') %.
%term lem42_app2
  %pi (lem42 Fs ([a] app (M1 a) (M2 a)) R Ft (frameterm_app Ft'))
  %<- (inverse_ft_app Ft Ft2)
  %<- (lem42 ([a] cons (fapp (M2 a)) (Fs a)) M1 R Ft2 Ft') %.
%term lem42_tapp2
  %pi (lem42 Fs ([a] tapp (M1 a) T) R Ft (frameterm_tapp Ft'))
  %<- (inverse_ft_tapp Ft Ft2)
  %<- (lem42 ([a] cons (ftapp T) (Fs a)) M1 R Ft2 Ft') %.
%term lem42_letu2
  %pi (lem42 Fs ([a] letu (M1 a) (M2 a)) R Ft (frameterm_letu Ft'))
  %<- (inverse_ft_letu Ft Ft2)
  %<- (lem42 ([a] cons (fletu (M2 a)) (Fs a)) M1 R Ft2 Ft') %.
%term lem42_letb2
  %pi (lem42 Fs ([a] letb (M1 a) (M2 a)) R Ft (frameterm_letb Ft'))
  %<- (inverse_ft_letb Ft Ft2)
  %<- (lem42 ([a] cons (fletb (M2 a)) (Fs a)) M1 R Ft2 Ft') %.
%term lem42_lett2
  %pi (lem42 Fs ([a] lett (M1 a) (M2 a)) R Ft (frameterm_lett Ft'))
  %<- (inverse_ft_lett Ft Ft2)
  %<- (lem42 ([a] cons (flett (M2 a)) (Fs a)) M1 R Ft2 Ft') %.
%worlds () (lem42 _ _ _ _ _) %.
%total D (lem42 _ _ _ D _) %.
%sort lem20 {M term} {M' term} {_ {a term} value (B a)} {_ {a} frameapply' (Fs a) (N a) (B a)} {_ eqf (Fs M) (Fs M')} %.
%mode lem20 %in %in %in %in %out %.
%term lem20_rule lem20 M M' _ ([a] frameapply'_nil) eqf_ref %.
%worlds (blam) (lem20 _ _ _ _ _) %.
%freeze lem20 %.
%total {} (lem20 _ _ _ _ _) %.
%sort lem26 {F1} {F2} {_ {m} frameapp (F m) m M1} {_ eqf F1 F2} %.
%mode lem26 %in %in %in %out %.
%worlds (blam) (lem26 _ _ _ _) %.
%freeze lem26 %.
%total {} (lem26 _ _ _ _) %.

More on linear frames

%sort lem27 {_ relavant ([m] N)} {Fs} {Fs'} {_ eqf Fs Fs'} %.
%mode lem27 %in %in %in %out %.
%term lem27_app1 %pi (lem27 (relavant_app1 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_app2 %pi (lem27 (relavant_app2 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_lam %pi (lem27 (relavant_lam R) M M' Q) %<- (lem27 (R unit) M M' Q) %.
%term lem27_tlam %pi (lem27 (relavant_tlam R) M M' Q) %<- (lem27 (R i) M M' Q) %.
%term lem27_tapp %pi (lem27 (relavant_tapp R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_letb1 %pi (lem27 (relavant_letb1 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_leb2 %pi (lem27 (relavant_letb2 R) M M' Q) %<- (lem27 (R unit) M M' Q) %.
%term lem27_thunk %pi (lem27 (relavant_thunk R) M M' Q) %<- (lem27 (R unit) M M' Q) %.
%term lem27_letu1 %pi (lem27 (relavant_letu1 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_letu2 %pi (lem27 (relavant_letu2 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_tens1 %pi (lem27 (relavant_tens1 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_tens2 %pi (lem27 (relavant_tens2 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_lett1 %pi (lem27 (relavant_lett1 R) M M' Q) %<- (lem27 R M M' Q) %.
%term lem27_lett2 %pi (lem27 (relavant_lett2 R) M M' Q) %<- (lem27 (R unit unit) M M' Q) %.
%worlds (blam) (lem27 _ _ _ _) %.
%freeze lem27 %.
%total D (lem27 D _ _ _) %.
%sort lem28 {Fs'} {Fs''} {_ {m term} frameapply (Fs m) (N m) M1} {_ relavant N} {_ eqf Fs' Fs''} %.
%mode lem28 %in %in %in %in %out %.
%term lem28_id %pi (lem28 Fs' Fs'' ([m] frameapply_cons _ (F m)) _ Q) %<- (lem26 _ _ F Q) %.
%term lem28_app1
  %pi (lem28 Fs' Fs'' ([m] frameapply_cons (FA m) (%the (frameapp (fapp (N m)) (M3 m) (app (M3 m) (N m))) frameapp_app)) R Q)
  %<- (lem28 Fs' Fs'' FA (relavant_app1 R) Q) %.
%term lem28_tapp
  %pi (lem28 Fs' Fs'' ([m] frameapply_cons (FA m) (%the (frameapp (ftapp T) (M3 m) (tapp (M3 m) T)) frameapp_app)) R Q)
  %<- (lem28 Fs' Fs'' FA (relavant_tapp R) Q) %.
%term lem28_letb
  %pi (lem28 Fs' Fs'' ([m] frameapply_cons (FA m) (%the (frameapp (fletb (N m)) (M3 m) (letb (M3 m) (N m))) frameapp_app)) R Q)
  %<- (lem28 Fs' Fs'' FA (relavant_letb1 R) Q) %.
%term lem28_lett
  %pi (lem28 Fs' Fs'' ([m] frameapply_cons (FA m) (%the (frameapp (flett (N m)) (M3 m) (lett (M3 m) (N m))) frameapp_app)) R Q)
  %<- (lem28 Fs' Fs'' FA (relavant_lett1 R) Q) %.
%term lem28_letu
  %pi (lem28 Fs' Fs'' ([m] frameapply_cons (FA m) (%the (frameapp (fletu (N m)) (M3 m) (letu (M3 m) (N m))) frameapp_app)) R Q)
  %<- (lem28 Fs' Fs'' FA (relavant_letu1 R) Q) %.
%term lem28_nil
  %pi (lem28 Fs' Fs'' ([m term] %the (frameapply nil (N2 m) N1) (FA m)) R Q)
  %<- ({m} frameapply_nil_eq (FA m) (Q' m))
  %<- (eq_relavant Q' R R')
  %<- (lem27 R' Fs' Fs'' Q) %.
%worlds (blam) (lem28 _ _ _ _ _) %.
%freeze lem28 %.
%total D (lem28 _ _ D _ _) %.
%sort lem19 {M' term} {M term} {_ {a} frameapply' (Fs a) a (R a)} {_ linear R} {_ eqf (Fs M') (Fs M)} %.
%mode lem19 %in %in %in %in %out %.
%term lem19_nil lem19 M M' ([a] frameapply'_nil) L eqf_ref %.
%term lem19_app1
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (fapp N2) _ _) frameapp_app) (FA a)) (linear_app1 L) Q)
  %<- (lem19 M M' FA L Q')
  %<- (eqf_extend (fapp N2) Q' Q) %.
%term lem19_letu1
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (fletu N2) _ _) frameapp_app) (FA a)) (linear_letu1 L) Q)
  %<- (lem19 M M' FA L Q')
  %<- (eqf_extend (fletu N2) Q' Q) %.
%term lem19_lett1
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (flett N2) _ _) frameapp_app) (FA a)) (linear_lett1 L) Q)
  %<- (lem19 M M' FA L Q')
  %<- (eqf_extend (flett N2) Q' Q) %.
%term lem19_letb1
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (fletb N2) _ _) frameapp_app) (FA a)) (linear_letb1 L) Q)
  %<- (lem19 M M' FA L Q')
  %<- (eqf_extend (fletb N2) Q' Q) %.
%term lem19_tapp
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (ftapp N2) _ _) frameapp_app) (FA a)) (linear_tapp L) Q)
  %<- (lem19 M M' FA L Q')
  %<- (eqf_extend (ftapp N2) Q' Q) %.
%term lem19_tens1 %pi (lem19 M M' FA (linear_tens1 L) Q) %<- (lem20 M M' ([a] val_tens) FA Q) %.
%term lem19_tens2 %pi (lem19 M M' FA (linear_tens2 L) Q) %<- (lem20 M M' ([a] val_tens) FA Q) %.
%term lem19_lam %pi (lem19 M M' FA (linear_lam L) Q) %<- (lem20 M M' ([a] val_lam) FA Q) %.
%term lem19_tlam %pi (lem19 M M' FA (linear_tlam L) Q) %<- (lem20 M M' ([a] val_tlam) FA Q) %.
%term lem19_app2
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (fapp (N2 a)) _ _) frameapp_app) (%the (frameapply' (Fs a) a M1) (FA a))) (linear_app2 L) Q)
  %<- ({y term} revFs_exists (Fs y) nil (Rev y))
  %<- ({y term} frameapply_e1 (Rev y) (FA y) (FA' y))
  %<- (lem28 _ _ FA' relavant_id Q) %.
%term lem19_letb2
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (fletb (N2 a)) _ _) frameapp_app) (%the (frameapply' (Fs a) a M1) (FA a))) (linear_letb2 L) Q)
  %<- ({y term} revFs_exists (Fs y) nil (Rev y))
  %<- ({y term} frameapply_e1 (Rev y) (FA y) (FA' y))
  %<- (lem28 _ _ FA' relavant_id Q) %.
%term lem19_letu2
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (fletu (N2 a)) _ _) frameapp_app) (%the (frameapply' (Fs a) a M1) (FA a))) (linear_letu2 L) Q)
  %<- ({y term} revFs_exists (Fs y) nil (Rev y))
  %<- ({y term} frameapply_e1 (Rev y) (FA y) (FA' y))
  %<- (lem28 _ _ FA' relavant_id Q) %.
%term lem19_lett2
  %pi (lem19 M M' ([a] frameapply'_cons (%the (frameapp (flett (N2 a)) _ _) frameapp_app) (%the (frameapply' (Fs a) a M1) (FA a))) (linear_lett2 L) Q)
  %<- ({y term} revFs_exists (Fs y) nil (Rev y))
  %<- ({y term} frameapply_e1 (Rev y) (FA y) (FA' y))
  %<- (lem28 _ _ FA' relavant_id Q) %.
%worlds (blam) (lem19 _ _ _ _ _) %.
%total D (lem19 _ _ _ D _) %.
%sort lem18 {M' term} {M term} {_ {a} frameapply (Fs a) a (R a)} {_ linear R} {_ eqf (Fs M') (Fs M)} %.
%mode lem18 %in %in %in %in %out %.
%term lem18_rule
  %pi (lem18 M M' (%the ({a} frameapply (Fs a) _ _) FA) L Q)
  %<- ({a} revFs_exists (Fs a) nil (Rev a))
  %<- ({a} frameapply_e2 (Rev a) (FA a) (FA' a))
  %<- (lem19 M M' FA' L Q')
  %<- (rev_eq2 Q' (Rev M) R)
  %<- (rev_injective R (Rev M') Q) %.
%worlds (blam) (lem18 _ _ _ _ _) %.
%total {} (lem18 _ _ _ _ _) %.
%sort apply_linear {_ linear M} {_ linear N} {_ linear R} {_ {a} frameapply' (Fs a) (N a) (R a)} {_ {a} frameapply' (Fs a) (M (N a)) (R' a)} {_ linear R'} %.
%mode apply_linear %in %in %in %in %out %out %.
%term apply_linear_nil
  %pi (apply_linear LM LN LR ([a term] frameapply'_nil) ([a term] frameapply'_nil) LR')
  %<- (sub_linear LM LN LR') %.
%term apply_linear_app1
  %pi (apply_linear LM LN (linear_app1 L) ([a term] frameapply'_cons (%the (frameapp (fapp M2) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_app1 LR'))
  %<- (apply_linear LM LN L FA FA' LR') %.
%term apply_linear_tapp1
  %pi (apply_linear LM LN (linear_tapp L) ([a term] frameapply'_cons (%the (frameapp (ftapp M2) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_tapp LR'))
  %<- (apply_linear LM LN L FA FA' LR') %.
%term apply_linear_letu1
  %pi (apply_linear LM LN (linear_letu1 L) ([a term] frameapply'_cons (%the (frameapp (fletu M2) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_letu1 LR'))
  %<- (apply_linear LM LN L FA FA' LR') %.
%term apply_linear_letb1
  %pi (apply_linear LM LN (linear_letb1 L) ([a term] frameapply'_cons (%the (frameapp (fletb M2) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_letb1 LR'))
  %<- (apply_linear LM LN L FA FA' LR') %.
%term apply_linear_lett1
  %pi (apply_linear LM LN (linear_lett1 L) ([a term] frameapply'_cons (%the (frameapp (flett M2) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_lett1 LR'))
  %<- (apply_linear LM LN L FA FA' LR') %.
%term apply_linear_app2
  %pi (apply_linear (%the (linear M) LM) LN (linear_app2 L) ([a term] frameapply'_cons (%the (frameapp (fapp _) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_app2 L))
  %<- (lem45 M FA FA') %.
%term apply_linear_letu2
  %pi (apply_linear (%the (linear M) LM) LN (linear_letu2 L) ([a term] frameapply'_cons (%the (frameapp (fletu _) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_letu2 L))
  %<- (lem45 M FA FA') %.
%term apply_linear_letb2
  %pi (apply_linear (%the (linear M) LM) LN (linear_letb2 L) ([a term] frameapply'_cons (%the (frameapp (fletb _) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_letb2 L))
  %<- (lem45 M FA FA') %.
%term apply_linear_lett2
  %pi (apply_linear (%the (linear M) LM) LN (linear_lett2 L) ([a term] frameapply'_cons (%the (frameapp (flett _) _ _) frameapp_app) (FA a)) ([a term] frameapply'_cons frameapp_app (FA' a)) (linear_lett2 L))
  %<- (lem45 M FA FA') %.
%worlds () (apply_linear _ _ _ _ _ _) %.
%freeze apply_linear %.
%total D (apply_linear _ _ _ D _ _) %.
%sort apply_lin {_ linear M} {_ linear N} {_ linear R} {_ {a} frameapply (Fs a) (N a) (R a)} {_ {a} frameapply (Fs a) (M (N a)) (R' a)} {_ linear R'} %.
%mode apply_lin %in %in %in %in %out %out %.
%term apply_lin_rule
  %pi (apply_lin LM LN LR (%the ({m} frameapply (Fs m) (N m) _) FA) FA4 L2)
  %<- ({m} revFs_exists (Fs m) nil (%the (revFs (Fs m) nil (Fs' m)) (Rev m)))
  %<- ({m} frameapply_e2 (Rev m) (FA m) (FA' m))
  %<- (apply_linear LM LN LR FA' FA2 L2)
  %<- ({m} revFs_exists (Fs' m) nil (Rev' m))
  %<- ({m} frameapply_e1 (Rev' m) (FA2 m) (FA3 m))
  %<- ({m} revrev_id (Rev m) (Rev' m) (Q m))
  %<- ({m} eqf_symm (Q m) (Q' m))
  %<- ({m} frameapply_eq (Q' m) (FA3 m) (FA4 m)) %.
%worlds () (apply_lin _ _ _ _ _ _) %.
%freeze apply_lin %.
%total D (apply_lin _ _ _ D _ _) %.
%sort add_frame {F} {_ {m term} frameapply (Fs m) m (R m)} {_ linear R} {_ {m term} frameapply (cons F (Fs m)) m (R' m)} {_ linear R'} %.
%mode add_frame %in %in %in %out %out %.
%term add_frame_app
  %pi (add_frame (fapp M) FA LR ([m] frameapply_cons (FA' m) frameapp_app) L')
  %<- (apply_lin (%the (linear ([a] app a M)) (linear_app1 linear_id)) linear_id LR FA FA' L') %.
%term add_frame_tapp
  %pi (add_frame (ftapp T) FA LR ([m] frameapply_cons (FA' m) frameapp_app) L')
  %<- (apply_lin (%the (linear ([a] tapp a T)) (linear_tapp linear_id)) linear_id LR FA FA' L') %.
%term add_frame_lett
  %pi (add_frame (flett M) FA LR ([m] frameapply_cons (FA' m) frameapp_app) L')
  %<- (apply_lin (%the (linear ([a] lett a M)) (linear_lett1 linear_id)) linear_id LR FA FA' L') %.
%term add_frame_letb
  %pi (add_frame (fletb M) FA LR ([m] frameapply_cons (FA' m) frameapp_app) L')
  %<- (apply_lin (%the (linear ([a] letb a M)) (linear_letb1 linear_id)) linear_id LR FA FA' L') %.
%term add_frame_letu
  %pi (add_frame (fletu M) FA LR ([m] frameapply_cons (FA' m) frameapp_app) L')
  %<- (apply_lin (%the (linear ([a] letu a M)) (linear_letu1 linear_id)) linear_id LR FA FA' L') %.
%worlds () (add_frame _ _ _ _ _) %.
%freeze add_frame %.
%total {} (add_frame _ _ _ _ _) %.

Strictness lemma preparations

Now we are ready for the strictness lemma.

Height preservation

The proof relies on complete induction on the height of a derivation which is a little troublesome in STELF.

%sort nat %.
%term zero nat %.
%term succ %pi nat %-> nat %.
%sort height_ok {_ frameterm _ _} {_ nat} %.
%term height_ok_bot height_ok (frameterm_val _) N %.
%term height_ok_app %pi (height_ok (frameterm_app F) (succ N)) %<- (height_ok F N) %.
%term height_ok_tapp %pi (height_ok (frameterm_tapp F) (succ N)) %<- (height_ok F N) %.
%term height_ok_letu %pi (height_ok (frameterm_letu F) (succ N)) %<- (height_ok F N) %.
%term height_ok_lett %pi (height_ok (frameterm_lett F) (succ N)) %<- (height_ok F N) %.
%term height_ok_letb %pi (height_ok (frameterm_letb F) (succ N)) %<- (height_ok F N) %.
%term height_ok_lam %pi (height_ok (frameterm_lam F) (succ N)) %<- (height_ok F N) %.
%term height_ok_tlam %pi (height_ok (frameterm_tlam F) (succ N)) %<- (height_ok F N) %.
%term height_ok_unit %pi (height_ok (frameterm_unit F) (succ N)) %<- (height_ok F N) %.
%term height_ok_tens %pi (height_ok (frameterm_tens F) (succ N)) %<- (height_ok F N) %.
%term height_ok_thunk %pi (height_ok (frameterm_thunk F) (succ N)) %<- (height_ok F N) %.
%sort height_ok_exists {ft frameterm Fs M} {_ height_ok ft N} %.
%mode height_ok_exists %in %out %.
%term height_ok_exists_bot height_ok_exists (frameterm_val _) (%the (height_ok _ zero) height_ok_bot) %.
%term height_ok_exists_app
  %pi (height_ok_exists (frameterm_app Ft) (height_ok_app H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_tapp
  %pi (height_ok_exists (frameterm_tapp Ft) (height_ok_tapp H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_letu
  %pi (height_ok_exists (frameterm_letu Ft) (height_ok_letu H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_lett
  %pi (height_ok_exists (frameterm_lett Ft) (height_ok_lett H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_letb
  %pi (height_ok_exists (frameterm_letb Ft) (height_ok_letb H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_lam
  %pi (height_ok_exists (frameterm_lam Ft) (height_ok_lam H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_tlam
  %pi (height_ok_exists (frameterm_tlam Ft) (height_ok_tlam H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_unit
  %pi (height_ok_exists (frameterm_unit Ft) (height_ok_unit H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_tens
  %pi (height_ok_exists (frameterm_tens Ft) (height_ok_tens H))
  %<- (height_ok_exists Ft H) %.
%term height_ok_exists_thunk
  %pi (height_ok_exists (frameterm_thunk Ft) (height_ok_thunk H))
  %<- (height_ok_exists Ft H) %.
%worlds () (height_ok_exists _ _) %.
%total D (height_ok_exists D _) %.
%sort succ_height_ok {_ height_ok Ft N} {_ height_ok Ft (succ N)} %.
%mode succ_height_ok %in %out %.
%term succ_height_ok_bot succ_height_ok height_ok_bot height_ok_bot %.
%term succ_height_ok_app
  %pi (succ_height_ok (height_ok_app H) (height_ok_app H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_tapp
  %pi (succ_height_ok (height_ok_tapp H) (height_ok_tapp H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_letu
  %pi (succ_height_ok (height_ok_letu H) (height_ok_letu H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_lett
  %pi (succ_height_ok (height_ok_lett H) (height_ok_lett H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_letb
  %pi (succ_height_ok (height_ok_letb H) (height_ok_letb H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_lam
  %pi (succ_height_ok (height_ok_lam H) (height_ok_lam H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_tlam
  %pi (succ_height_ok (height_ok_tlam H) (height_ok_tlam H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_unit
  %pi (succ_height_ok (height_ok_unit H) (height_ok_unit H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_tens
  %pi (succ_height_ok (height_ok_tens H) (height_ok_tens H'))
  %<- (succ_height_ok H H') %.
%term succ_height_ok_thunk
  %pi (succ_height_ok (height_ok_thunk H) (height_ok_thunk H'))
  %<- (succ_height_ok H H') %.
%worlds () (succ_height_ok _ _) %.
%total D (succ_height_ok D _) %.
%sort frameterm_eq_framesNum {_ eqf Fs Fs'} {_ eq M M'} {Ft frameterm Fs M} {_ height_ok Ft Num} {Ft' frameterm Fs' M'} {_ height_ok Ft' Num} %.
%mode frameterm_eq_framesNum %in %in %in %in %out %out %.
%term frameterm_eq_framesNum_rule frameterm_eq_framesNum eqf_ref eq_ref Ft H Ft H %.
%worlds () (frameterm_eq_framesNum _ _ _ _ _ _) %.
%total {} (frameterm_eq_framesNum _ _ _ _ _ _) %.

Height reducing inversions

%sort up_app {ft frameterm Fs (app M1 M2)} {_ height_ok ft (succ N)} {ft' frameterm (cons (fapp M2) Fs) M1} {_ height_ok ft' N} %.
%mode up_app %in %in %out %out %.
%term up_app_rule up_app (frameterm_app F) (height_ok_app H) F H %.
%worlds () (up_app _ _ _ _) %.
%total D (up_app D _ _ _) %.
%sort up_tapp {ft frameterm Fs (tapp M T)} {_ height_ok ft (succ N)} {ft' frameterm (cons (ftapp T) Fs) M} {_ height_ok ft' N} %.
%mode up_tapp %in %in %out %out %.
%term up_tapp_rule up_tapp (frameterm_tapp F) (height_ok_tapp H) F H %.
%worlds () (up_tapp _ _ _ _) %.
%total D (up_tapp D _ _ _) %.
%sort up_lett {ft frameterm Fs (lett M1 M2)} {_ height_ok ft (succ N)} {ft' frameterm (cons (flett M2) Fs) M1} {_ height_ok ft' N} %.
%mode up_lett %in %in %out %out %.
%term up_lett_rule up_lett (frameterm_lett F) (height_ok_lett H) F H %.
%worlds () (up_lett _ _ _ _) %.
%total D (up_lett D _ _ _) %.
%sort up_letu {ft frameterm Fs (letu M1 M2)} {_ height_ok ft (succ N)} {ft' frameterm (cons (fletu M2) Fs) M1} {_ height_ok ft' N} %.
%mode up_letu %in %in %out %out %.
%term up_letu_rule up_letu (frameterm_letu F) (height_ok_letu H) F H %.
%worlds () (up_letu _ _ _ _) %.
%total D (up_letu D _ _ _) %.
%sort up_letb {ft frameterm Fs (letb M1 M2)} {_ height_ok ft (succ N)} {ft' frameterm (cons (fletb M2) Fs) M1} {_ height_ok ft' N} %.
%mode up_letb %in %in %out %out %.
%term up_letb_rule up_letb (frameterm_letb F) (height_ok_letb H) F H %.
%worlds () (up_letb _ _ _ _) %.
%total D (up_letb D _ _ _) %.
%sort up_lam {ft frameterm (cons (fapp M2) Fs) (lam T M1')} {_ height_ok ft (succ N)} {ft' frameterm Fs (M1' M2)} {_ height_ok ft' N} %.
%mode up_lam %in %in %out %out %.
%term up_lam_rule up_lam (frameterm_lam F) (height_ok_lam H) F H %.
%worlds () (up_lam _ _ _ _) %.
%total D (up_lam D _ _ _) %.
%sort up_tlam {ft frameterm (cons (ftapp T) Fs) (tlam M)} {_ height_ok ft (succ N)} {ft' frameterm Fs (M T)} {_ height_ok ft' N} %.
%mode up_tlam %in %in %out %out %.
%term up_tlam_rule up_tlam (frameterm_tlam F) (height_ok_tlam H) F H %.
%worlds () (up_tlam _ _ _ _) %.
%total D (up_tlam D _ _ _) %.
%sort up_tens {ft frameterm (cons (flett M3) Fs) (tens M1 M2)} {_ height_ok ft (succ N)} {ft' frameterm Fs (M3 M1 M2)} {_ height_ok ft' N} %.
%mode up_tens %in %in %out %out %.
%term up_tens_rule up_tens (frameterm_tens F) (height_ok_tens H) F H %.
%worlds () (up_tens _ _ _ _) %.
%total D (up_tens D _ _ _) %.
%sort up_unit {ft frameterm (cons (fletu M) Fs) unit} {_ height_ok ft (succ N)} {ft' frameterm Fs M} {_ height_ok ft' N} %.
%mode up_unit %in %in %out %out %.
%term up_unit_rule up_unit (frameterm_unit F) (height_ok_unit H) F H %.
%worlds () (up_unit _ _ _ _) %.
%total D (up_unit D _ _ _) %.
%sort up_thunk {ft frameterm (cons (fletb M2) Fs) (thunk T M1)} {_ height_ok ft (succ N)} {ft' frameterm Fs (M2 (letb (thunk T M1) M1))} {_ height_ok ft' N} %.
%mode up_thunk %in %in %out %out %.
%term up_thunk_rule up_thunk (frameterm_thunk F) (height_ok_thunk H) F H %.
%worlds () (up_thunk _ _ _ _) %.
%total D (up_thunk D _ _ _) %.

Special cases of type preservation

%sort types_pres_app1_s {_ M \s/ V} {_ app M N ? T} {_ app V N ? T} %.
%mode types_pres_app1_s %in %in %out %.
%term types_pres_app1_s_rule %pi (%type s_pres_app1_s E (of_app D2 D1) (of_app D2 D1')) %<- (tpres_s D1 E D1') %.
%worlds () (types_pres_app1_s _ _ _) %.
%total {} (types_pres_app1_s _ _ _) %.
%sort types_pres_app2_s {_ M \s/ V} {_ app N M ? T} {_ app N V ? T} %.
%mode types_pres_app2_s %in %in %out %.
%term types_pres_app2_s_rule %pi (%type s_pres_app2_s E (of_app D2 D1) (of_app D2' D1)) %<- (tpres_s D2 E D2') %.
%worlds () (types_pres_app2_s _ _ _) %.
%total {} (types_pres_app2_s _ _ _) %.
%sort types_pres_tapp_s {_ M \s/ V} {_ tapp M T ? T'} {_ tapp V T ? T'} %.
%mode types_pres_tapp_s %in %in %out %.
%term types_pres_tapp_s_rule %pi (%type s_pres_tapp_s E (of_tapp T D1) (of_tapp T D1')) %<- (tpres_s D1 E D1') %.
%worlds () (types_pres_tapp_s _ _ _) %.
%total {} (types_pres_tapp_s _ _ _) %.
%sort types_pres_letu_s {_ M \s/ V} {_ letu M N ? T} {_ letu V N ? T} %.
%mode types_pres_letu_s %in %in %out %.
%term types_pres_letu_s_rule
  %pi (%type s_pres_letu_s E (of_letu D2 D1) (of_letu D2 D1'))
  %<- (tpres_s D1 E D1') %.
%worlds () (types_pres_letu_s _ _ _) %.
%total {} (types_pres_letu_s _ _ _) %.
%sort types_pres_lett_s {_ M \s/ V} {_ lett M N ? T} {_ lett V N ? T} %.
%mode types_pres_lett_s %in %in %out %.
%term types_pres_lett_s_rule
  %pi (%type s_pres_lett_s E (of_lett L1 L2 D2 D1) (of_lett L1 L2 D2 D1'))
  %<- (tpres_s D1 E D1') %.
%worlds () (types_pres_lett_s _ _ _) %.
%total {} (types_pres_lett_s _ _ _) %.
%sort types_pres_letb_s {_ M \s/ V} {_ letb M N ? T} {_ letb V N ? T} %.
%mode types_pres_letb_s %in %in %out %.
%term types_pres_letb_s_rule
  %pi (%type s_pres_letb_s E (of_letb D2 D1) (of_letb D2 D1'))
  %<- (tpres_s D1 E D1') %.
%worlds () (types_pres_letb_s _ _ _) %.
%freeze types_pres_letb_s %.
%total {} (types_pres_letb_s _ _ _) %.
%sort redex_rev_type {_ redex M M'} {_ M ? T} {_ M' ? T} %.
%mode redex_rev_type %in %in %out %.
%term redex_rev_type_app
  %pi (redex_rev_type redex_app (of_app D2 D1) (D1' _ D2))
  %<- (inverse_lam D1 D1' _) %.
%term redex_rev_type_tapp redex_rev_type redex_tapp (of_tapp T (of_tlam D1)) (D1 T) %.
%term redex_rev_type_letu redex_rev_type redex_letu (of_letu D2 D1) D2 %.
%term redex_rev_type_lett redex_rev_type redex_lett (of_lett _ _ D3 (of_tens D2 D1)) (D3 _ D1 _ D2) %.
%term redex_rev_type_letb redex_rev_type redex_letb (of_letb D2 (of_thunk D1)) (D2 _ (of_letb D1 (of_thunk D1))) %.
%worlds () (redex_rev_type _ _ _) %.
%total {} (redex_rev_type _ _ _) %.

The actual lemma

%sort strictness_base {N} {M} {_ N M ? bang T} {_ linear N} {_ value (N M)} {_ value M} %.
%mode strictness_base %in %in %in %in %in %out %.
%term strictness_base_rule strictness_base _ _ _ linear_id V V %.
%worlds () (strictness_base _ _ _ _ _ _) %.
%total {} (strictness_base _ _ _ _ _ _) %.
%sort strictness_lem1 {N} {Fs} {Num nat} {Ft frameterm (Fs M) (N M)} {_ height_ok Ft Num} {_ {a} frameapply (Fs a) (N a) (FsN a)} {_ linear FsN} {_ fstp (Fs M) T1 (bang T2)} {_ N M ? T1} {Ft2 frameterm (Fs V) (N V)} {_ M \s/ V} {_ height_ok Ft2 Num} %.
%mode strictness_lem1 %in %in %in %in %in %in %in %in %in %out %out %out %.
%term strictness_lem1_base
  %pi (strictness_lem1 N ([a] nil) Num (frameterm_val V) H FA L FsTp DNM (frameterm_val V) Evs H)
  %<- (frameapply_nil_eq (FA M) Q)
  %<- (eq_val Q V V')
  %<- (applysound nil FsTp DNM (FA M) DNMB)
  %<- (strictness_base _ M DNMB L V' VM)
  %<- (selfevals VM Evs) %.
%term strictness_lem1_app2
  %pi (strictness_lem1 ([a] a) Fs _ (frameterm_app Ft) (height_ok_app H) FA L FsTp D3 Ft6 (evs_app EvM12 EvM2 EvM1') H7)
  %<- (lem18 (app M1 M2) M1 FA L Q)
  %<- (frameterm_eq_framesNum Q eq_ref (frameterm_app Ft) (height_ok_app H) Ft1 H1)
  %<- (up_app Ft1 H1 Ft2 H2)
  %<- (eqf_fstp Q FsTp FsTp1)
  %<- (%type d_step FsTp1 D3 evfs_app FsTp' D3')
  %<- (add_frame (fapp M2) FA L FA' L')
  %<- (eq_typings D3 (of_app _ D1))
  %<- (strictness_lem1 ([a] a) ([a] cons (fapp M2) (Fs a)) _ Ft2 H2 FA' L' FsTp' D3' Ft2' (%the (M1 \s/ V1) EvM1) H2')
  %<- (tpres_s D1 EvM1 D1')
  %<- (value_soundness_s EvM1 Val1)
  %<- (eq_val_funs Val1 D1' Q1)
  %<- (eq_type Q1 D1' D1'')
  %<- (eq_typings D1'' (of_lam (%the (linear M1') L1) D1'''))
  %<- (succ_height_ok H2' H2'')
  %<- (frameterm_eq_framesNum eqf_ref Q1 Ft2' H2'' Ft3 H3)
  %<- (up_lam Ft3 H3 Ft3' H3')
  %<- (lem18 V1 M2 FA L Q2)
  %<- (frameterm_eq_framesNum Q2 eq_ref Ft3' H3' Ft4 H4)
  %<- (apply_lin L1 linear_id L FA FA2 L2)
  %<- (%type s_pres_app1_s EvM1 D3 D3'')
  %<- (eq_ctx Q1 ([a] app a M2) Q1')
  %<- (eq_type Q1' D3'' D4)
  %<- (redex_rev_type redex_app D4 D4')
  %<- (lem18 (app M1 M2) M2 FA L Q3)
  %<- (eqf_fstp Q3 FsTp FsTp2)
  %<- (strictness_lem1 M1' Fs _ Ft4 H4 FA2 L2 FsTp2 D4' Ft4' (%the (M2 \s/ V2) EvM2) H4')
  %<- (lem18 V2 (M1' V2) FA L Q5)
  %<- (frameterm_eq_framesNum Q5 eq_ref Ft4' H4' Ft5 H5)
  %<- (%type s_pres_app2_s EvM2 D4 D5)
  %<- (redex_rev_type redex_app D5 D5')
  %<- (lem18 M2 (M1' V2) FA L Q6)
  %<- (eqf_fstp Q6 FsTp2 FsTp3)
  %<- (strictness_lem1 ([a] a) Fs _ Ft5 H5 FA L FsTp3 D5' Ft6 EvM12 H6)
  %<- (eq_res_s Q1 EvM1 EvM1')
  %<- (succ_height_ok H6 H7) %.
%term strictness_lem1_tapp2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D2 Ft4' (evs_tapp EvM1'T EvM1') H5)
  %<- (lem18 (tapp M1 T1) M1 FA L Q)
  %<- (frameterm_eq_framesNum Q eq_ref Ft H Ft1 H1)
  %<- (up_tapp Ft1 H1 Ft2 H2)
  %<- (eqf_fstp Q FsTp FsTp1)
  %<- (inverse_tapp D2 D1)
  %<- (%type d_step FsTp1 D2 evfs_tapp FsTp' D2')
  %<- (add_frame (ftapp T1) FA L FA' L')
  %<- (strictness_lem1 ([a] a) ([a] cons (ftapp T1) (Fs a)) _ Ft2 H2 FA' L' FsTp' D2' Ft2' (%the (M1 \s/ V1) EvM1) H2')
  %<- (tpres_s D1 EvM1 D1')
  %<- (value_soundness_s EvM1 Val1)
  %<- (eq_val_all Val1 D1' Q1)
  %<- (eq_type Q1 D1' D1'')
  %<- (eq_typings D1'' (of_tlam (%the ({t tp} M1' t ? _) D1''')))
  %<- (succ_height_ok H2' H2'')
  %<- (frameterm_eq_framesNum eqf_ref Q1 Ft2' H2'' Ft2'' H2''')
  %<- (up_tlam Ft2'' H2''' Ft3 H3)
  %<- (%type s_pres_tapp_s EvM1 D2 D3)
  %<- (eq_ctx Q1 ([a] tapp a T1) Q1')
  %<- (eq_type Q1' D3 D4)
  %<- (redex_rev_type redex_tapp D4 D4')
  %<- (lem18 M1 (M1' T1) FA L Q2)
  %<- (eqf_fstp Q2 FsTp1 FsTp1')
  %<- (lem18 V1 (M1' T1) FA L Q3)
  %<- (frameterm_eq_framesNum Q3 eq_ref Ft3 H3 Ft4 H4)
  %<- (strictness_lem1 ([a] a) Fs _ Ft4 H4 FA L FsTp1' D4' Ft4' EvM1'T H4')
  %<- (eq_res_s Q1 EvM1 EvM1')
  %<- (succ_height_ok H4' H5) %.
%term strictness_lem1_lett2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D3 Ft4' (evs_lett EvM2 EvM1') H5)
  %<- (lem18 (lett M1 M2) M1 FA L Q)
  %<- (frameterm_eq_framesNum Q eq_ref Ft H Ft1 H1)
  %<- (up_lett Ft1 H1 Ft2 H2)
  %<- (eqf_fstp Q FsTp FsTp1)
  %<- (%type d_step FsTp1 D3 evfs_lett FsTp' D3')
  %<- (add_frame (flett M2) FA L FA' L')
  %<- (strictness_lem1 ([a] a) ([a] cons (flett M2) (Fs a)) _ Ft2 H2 FA' L' FsTp' D3' Ft2' (%the (M1 \s/ V1) EvM1) H2')
  %<- (eq_typings D3 (of_lett _ _ _ D1))
  %<- (tpres_s D1 EvM1 D1')
  %<- (value_soundness_s EvM1 Val1)
  %<- (eq_val_tensor Val1 D1' Q1)
  %<- (eq_type Q1 D1' D1'')
  %<- (eq_typings D1'' (of_tens (%the (Mt2 ? _) Dt2) (%the (Mt1 ? _) Dt1)))
  %<- (succ_height_ok H2' H2'')
  %<- (frameterm_eq_framesNum eqf_ref Q1 Ft2' H2'' Ft3 H3)
  %<- (up_tens Ft3 H3 Ft3' H3')
  %<- (%type s_pres_lett_s EvM1 D3 D4)
  %<- (eq_ctx Q1 ([a] lett a M2) Q1')
  %<- (eq_type Q1' D4 D4'')
  %<- (redex_rev_type redex_lett D4'' D4')
  %<- (lem18 M1 (M2 Mt1 Mt2) FA L Q2)
  %<- (eqf_fstp Q2 FsTp1 FsTp1')
  %<- (lem18 V1 (M2 Mt1 Mt2) FA L Q3)
  %<- (frameterm_eq_framesNum Q3 eq_ref Ft3' H3' Ft4 H4)
  %<- (strictness_lem1 ([a] a) Fs _ Ft4 H4 FA L FsTp1' D4' Ft4' EvM2 H4')
  %<- (eq_res_s Q1 EvM1 EvM1')
  %<- (succ_height_ok H4' H5) %.
%term strictness_lem1_letu2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D3 Ft4' (evs_letu EvM2 EvM1') H5)
  %<- (lem18 (letu M1 M2) M1 FA L Q)
  %<- (frameterm_eq_framesNum Q eq_ref Ft H Ft1 H1)
  %<- (up_letu Ft1 H1 Ft2 H2)
  %<- (eqf_fstp Q FsTp FsTp1)
  %<- (%type d_step FsTp1 D3 evfs_letu FsTp' D3')
  %<- (add_frame (fletu M2) FA L FA' L')
  %<- (strictness_lem1 ([a] a) ([a] cons (fletu M2) (Fs a)) _ Ft2 H2 FA' L' FsTp' D3' Ft2' (%the (M1 \s/ V1) EvM1) H2')
  %<- (eq_typings D3 (of_letu _ D1))
  %<- (tpres_s D1 EvM1 D1')
  %<- (value_soundness_s EvM1 Val1)
  %<- (eq_val_unit Val1 D1' Q1)
  %<- (succ_height_ok H2' H2'')
  %<- (frameterm_eq_framesNum eqf_ref Q1 Ft2' H2'' Ft3 H3)
  %<- (up_unit Ft3 H3 Ft3' H3')
  %<- (lem18 V1 M2 FA L Q2)
  %<- (lem18 M1 M2 FA L Q2')
  %<- (frameterm_eq_framesNum Q2 eq_ref Ft3' H3' Ft4 H4)
  %<- (eqf_fstp Q2' FsTp1 FsTp1')
  %<- (%type s_pres_letu_s EvM1 D3 D3'')
  %<- (eq_ctx Q1 ([a] letu a M2) Q3)
  %<- (eq_type Q3 D3'' D4)
  %<- (redex_rev_type redex_letu D4 D4')
  %<- (strictness_lem1 ([a] a) Fs _ Ft4 H4 FA L FsTp1' D4' Ft4' EvM2 H4')
  %<- (succ_height_ok H4' H5)
  %<- (eq_res_s Q1 EvM1 EvM1') %.
%term strictness_lem1_letb2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D3 Ft4' (evs_letb EvM2 EvM1') H5)
  %<- (lem18 (letb M1 M2) M1 FA L Q)
  %<- (frameterm_eq_framesNum Q eq_ref Ft H Ft1 H1)
  %<- (up_letb Ft1 H1 Ft2 H2)
  %<- (eqf_fstp Q FsTp FsTp1)
  %<- (%type d_step FsTp1 D3 evfs_letb FsTp' D3')
  %<- (add_frame (fletb M2) FA L FA' L')
  %<- (strictness_lem1 ([a] a) ([a] cons (fletb M2) (Fs a)) _ Ft2 H2 FA' L' FsTp' D3' Ft2' (%the (M1 \s/ V1) EvM1) H2')
  %<- (eq_typings D3 (of_letb _ D1))
  %<- (tpres_s D1 EvM1 D1')
  %<- (value_soundness_s EvM1 Val1)
  %<- (eq_val_bang Val1 D1' Q1)
  %<- (eq_type Q1 D1' D1'')
  %<- (eq_thunk_type D1'' Q')
  %<- (eqt_symm Q' Q'')
  %<- (eqt_ctx Q'' ([t] bang t) Q''')
  %<- (eq_type1 Q''' D1'' D1''')
  %<- (eq_typings D1''' (%the (thunk Ty _ ? _) (of_thunk (%the ({m term} {d m ? _} Mt1 m ? _) Dt1))))
  %<- (succ_height_ok H2' H2'')
  %<- (frameterm_eq_framesNum eqf_ref Q1 Ft2' H2'' Ft3 H3)
  %<- (up_thunk Ft3 H3 Ft3' H3')
  %<- (%type s_pres_letb_s EvM1 D3 D4)
  %<- (eq_ctx Q1 ([a] letb a M2) Q1')
  %<- (eq_type Q1' D4 D4'')
  %<- (redex_rev_type redex_letb D4'' D4')
  %<- (lem18 M1 (M2 (letb (thunk Ty Mt1) Mt1)) FA L Q2)
  %<- (eqf_fstp Q2 FsTp1 FsTp1')
  %<- (lem18 V1 (M2 (letb (thunk Ty Mt1) Mt1)) FA L Q3)
  %<- (frameterm_eq_framesNum Q3 eq_ref Ft3' H3' Ft4 H4)
  %<- (strictness_lem1 ([a] a) Fs _ Ft4 H4 FA L FsTp1' D4' Ft4' EvM2 H4')
  %<- (succ_height_ok H4' H5)
  %<- (eq_res_s Q1 EvM1 EvM1') %.
%term strictness_lem1_app1
  %pi (strictness_lem1 ([a] app (N1 a) (N2 a)) Fs _ (frameterm_app Ft) (height_ok_app H) FA L FsTp (of_app DN2 DN1) (frameterm_app Ft') Evs (height_ok_app H'))
  %<- (strictness_lem1 N1 ([a] cons (fapp (N2 a)) (Fs a)) _ Ft H ([a] frameapply_cons (FA a) (%the (frameapp _ _ _) frameapp_app)) L (ftp_cons FsTp ([a] [da] of_app DN2 da)) DN1 Ft' Evs H') %.
%term strictness_lem1_tapp1
  %pi (strictness_lem1 ([a] tapp (N1 a) T) Fs _ (frameterm_tapp Ft) (height_ok_tapp H) FA L FsTp (of_tapp _ DN1) (frameterm_tapp Ft') Evs (height_ok_tapp H'))
  %<- (strictness_lem1 N1 ([a] cons (ftapp T) (Fs a)) _ Ft H ([a] frameapply_cons (FA a) (%the (frameapp _ _ _) frameapp_app)) L (ftp_cons FsTp ([a] [da] of_tapp _ da)) DN1 Ft' Evs H') %.
%term strictness_lem1_letu1
  %pi (strictness_lem1 ([a] letu (N1 a) (N2 a)) Fs _ (frameterm_letu Ft) (height_ok_letu H) FA L FsTp (of_letu DN2 DN1) (frameterm_letu Ft') Evs (height_ok_letu H'))
  %<- (strictness_lem1 N1 ([a] cons (fletu (N2 a)) (Fs a)) _ Ft H ([a] frameapply_cons (FA a) (%the (frameapp _ _ _) frameapp_app)) L (ftp_cons FsTp ([a] [da] of_letu DN2 da)) DN1 Ft' Evs H') %.
%term strictness_lem1_letb1
  %pi (strictness_lem1 ([a] letb (N1 a) (N2 a)) Fs _ (frameterm_letb Ft) (height_ok_letb H) FA L FsTp (of_letb DN2 DN1) (frameterm_letb Ft') Evs (height_ok_letb H'))
  %<- (strictness_lem1 N1 ([a] cons (fletb (N2 a)) (Fs a)) _ Ft H ([a] frameapply_cons (FA a) (%the (frameapp _ _ _) frameapp_app)) L (ftp_cons FsTp ([a] [da] of_letb DN2 da)) DN1 Ft' Evs H') %.
%term strictness_lem1_lett1
  %pi (strictness_lem1 ([a] lett (N1 a) (N2 a)) Fs _ (frameterm_lett Ft) (height_ok_lett H) FA L FsTp (of_lett L1 L2 DN2 DN1) (frameterm_lett Ft') Evs (height_ok_lett H'))
  %<- (strictness_lem1 N1 ([a] cons (flett (N2 a)) (Fs a)) _ Ft H ([a] frameapply_cons (FA a) (%the (frameapp _ _ _) frameapp_app)) L (ftp_cons FsTp ([a] [da] of_lett L1 L2 DN2 da)) DN1 Ft' Evs H') %.
%term strictness_lem1_lam
  %pi (strictness_lem1 ([a] lam T (M4 a)) ([a] cons (fapp (M5 a)) (Fs a)) _ (frameterm_lam Ft) (height_ok_lam H) ([a] frameapply_cons (FA a) (%the (frameapp (fapp (M5 a)) _ _) frameapp_app)) L (ftp_cons FsTp FTp) D2 (frameterm_lam Ft') Evs (height_ok_lam H'))
  %<- (eq_typings ((%the ({m} %pi (m ? func _ _) %-> (app m _ ? T2)) FTp) _ D2) D1)
  %<- (redex_rev_type redex_app D1 D')
  %<- (frame_linear ([m] redex_app) D1 FA L FA1 L1)
  %<- (strictness_lem1 ([a] M4 a (M5 a)) Fs _ Ft H FA1 L1 FsTp D' Ft' Evs H') %.
%term strictness_lem1_tens
  %pi (strictness_lem1 ([a] tens (M3 a) (M4 a)) ([a] cons (flett (M5 a)) (Fs a)) _ (frameterm_tens Ft) (height_ok_tens H) ([a] frameapply_cons (FA a) (%the (frameapp (flett (M5 a)) _ _) frameapp_app)) L (ftp_cons FsTp FTp) D2 (frameterm_tens Ft') Evs (height_ok_tens H'))
  %<- (eq_typings ((%the ({m} %pi (m ? tensor _ _) %-> (lett m _ ? T2)) FTp) _ D2) Dt)
  %<- (redex_rev_type redex_lett Dt D')
  %<- (frame_linear ([m] redex_lett) Dt FA L FA1 L')
  %<- (strictness_lem1 ([a] M5 a (M3 a) (M4 a)) Fs _ Ft H FA1 L' FsTp D' Ft' Evs H') %.
%term strictness_lem1_unit
  %pi (strictness_lem1 ([a] unit) ([a] cons (fletu (M5 a)) (Fs a)) _ (frameterm_unit Ft) (height_ok_unit H) ([a] frameapply_cons (FA a) (%the (frameapp (fletu (M5 a)) _ _) frameapp_app)) L (ftp_cons FsTp FTp) D2 (frameterm_unit Ft') Evs (height_ok_unit H'))
  %<- (eq_typings ((%the ({m} %pi (m ? i) %-> (letu m _ ? T2)) FTp) _ D2) Dt)
  %<- (redex_rev_type redex_letu Dt D')
  %<- (frame_linear ([m] redex_letu) Dt FA L FA1 L')
  %<- (strictness_lem1 ([a] M5 a) Fs _ Ft H FA1 L' FsTp D' Ft' Evs H') %.
%term strictness_lem1_thunk
  %pi (strictness_lem1 ([a] thunk T (M4 a)) ([a] cons (fletb (M5 a)) (Fs a)) _ (frameterm_thunk Ft) (height_ok_thunk H) ([a] frameapply_cons (FA a) (%the (frameapp (fletb (M5 a)) _ _) frameapp_app)) L (ftp_cons FsTp FTp) D2 (frameterm_thunk Ft') Evs (height_ok_thunk H'))
  %<- (eq_typings ((%the ({m} %pi (m ? bang _) %-> (letb m _ ? T2)) FTp) _ D2) Dt)
  %<- (redex_rev_type redex_letb Dt D')
  %<- (frame_linear ([m] redex_letb) Dt FA L FA1 L')
  %<- (strictness_lem1 ([a] M5 a (letb (thunk T (M4 a)) (M4 a))) Fs _ Ft H FA1 L' FsTp D' Ft' Evs H') %.
%term strictness_lem1_tlam
  %pi (strictness_lem1 ([a] tlam (M4 a)) ([a] cons (ftapp T) (Fs a)) _ (frameterm_tlam Ft) (height_ok_tlam H) ([a] frameapply_cons (FA a) (%the (frameapp (ftapp T) _ _) frameapp_app)) L (ftp_cons FsTp FTp) D2 (frameterm_tlam Ft') Evs (height_ok_tlam H'))
  %<- (eq_typings ((%the ({m} %pi (m ? all _) %-> (tapp m _ ? T2)) FTp) _ D2) D1)
  %<- (redex_rev_type redex_tapp D1 D')
  %<- (frame_linear ([m] redex_tapp) D1 FA L FA1 L1)
  %<- (strictness_lem1 ([a] M4 a T) Fs _ Ft H FA1 L1 FsTp D' Ft' Evs H') %.
%term strictness_lem1_unit2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D2 Ft Evs H)
  %<- (selfevals val_unit Evs) %.
%term strictness_lem1_lam2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D2 Ft Evs H)
  %<- (selfevals val_lam Evs) %.
%term strictness_lem1_tlam2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D2 Ft Evs H)
  %<- (selfevals val_tlam Evs) %.
%term strictness_lem1_tens2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D2 Ft Evs H)
  %<- (selfevals val_tens Evs) %.
%term strictness_lem1_thunk2
  %pi (strictness_lem1 ([a] a) Fs _ Ft H FA L FsTp D2 Ft Evs H)
  %<- (selfevals val_thunk Evs) %.
%worlds () (strictness_lem1 _ _ _ _ _ _ _ _ _ _ _ _) %.
% covers strictness_lem1 +N +Fs +Num +FtM +H +FA +L +FD +FsT -FtV -EVs -H'.
% terminates D (strictness_lem1 _ _ D _ _ _ _ _ _ _ _ _).
%total D (strictness_lem1 _ _ D _ _ _ _ _ _ _ _ _) %.
%sort strictness1 {_ N M ? bang T'} {_ linear N} {_ N M \/} {_ M \s/ V'} {_ N V' \/} %.
%mode strictness1 %in %in %in %out %out %.
%term strictness1_rule
  %pi (strictness1 D1 L (terminate Ev) Evs (terminate Ev'))
  %<- (eval_frameterm Ev Ft)
  %<- (height_ok_exists Ft (%the (height_ok _ Num) H))
  %<- (strictness_lem1 N ([a term] nil) Num Ft H ([a] frameapply_nil) L ftp_nil D1 Ft' Evs H')
  %<- (frameterm_eval Ft' Ev') %.
%worlds () (strictness1 _ _ _ _ _) %.
% covers strictness1 +D +L +Ev -S -Term.
%total {} (strictness1 _ _ _ _ _) %.
%sort frameterm_eq_frames {_ eqf Fs Fs'} {_ eq M M'} {_ frameterm Fs M} {_ frameterm Fs' M'} %.
%mode frameterm_eq_frames %in %in %in %out %.
%term frameterm_eq_frames_rule frameterm_eq_frames eqf_ref eq_ref Ft Ft %.
%worlds () (frameterm_eq_frames _ _ _ _) %.
%total {} (frameterm_eq_frames _ _ _ _) %.
%sort strictness2_lem1 {N} {Fs} {_ frameterm (Fs V) (N V)} {_ M \s/ V} {_ frameterm (Fs M) (N M)} %.
%mode strictness2_lem1 %in %in %in %in %out %.
%term strictness2_lem1_tens_val strictness2_lem1 ([a] tens _ _) ([a] nil) (frameterm_val _) _ (frameterm_val val_tens) %.
%term strictness2_lem1_unit_val strictness2_lem1 ([a] unit) ([a] nil) (frameterm_val _) _ (frameterm_val val_unit) %.
%term strictness2_lem1_lam_val strictness2_lem1 ([a] lam T _) ([a] nil) (frameterm_val _) _ (frameterm_val val_lam) %.
%term strictness2_lem1_tlam_val strictness2_lem1 ([a] tlam _) ([a] nil) (frameterm_val _) _ (frameterm_val val_tlam) %.
%term strictness2_lem1_thunk_val strictness2_lem1 ([a] thunk T _) ([a] nil) (frameterm_val _) _ (frameterm_val val_thunk) %.
%term strictness2_lem1_unit2 strictness2_lem1 ([a] a) Fs Ft evs_unit Ft %.
%term strictness2_lem1_lam2 strictness2_lem1 ([a] a) Fs Ft evs_lam Ft %.
%term strictness2_lem1_tlam2 strictness2_lem1 ([a] a) Fs Ft evs_tlam Ft %.
%term strictness2_lem1_tens2 strictness2_lem1 ([a] a) Fs Ft evs_tens Ft %.
%term strictness2_lem1_thunk2 strictness2_lem1 ([a] a) Fs Ft evs_thunk Ft %.
%term strictness2_lem1_app1
  %pi (strictness2_lem1 ([a] app (N1 a) (N2 a)) Fs (frameterm_app Ft) Evs (frameterm_app Ft'))
  %<- (strictness2_lem1 N1 ([a] cons (fapp (N2 a)) (Fs a)) Ft Evs Ft') %.
%term strictness2_lem1_tapp1
  %pi (strictness2_lem1 ([a] tapp (N1 a) T) Fs (frameterm_tapp Ft) Evs (frameterm_tapp Ft'))
  %<- (strictness2_lem1 N1 ([a] cons (ftapp T) (Fs a)) Ft Evs Ft') %.
%term strictness2_lem1_letu1
  %pi (strictness2_lem1 ([a] letu (N1 a) (N2 a)) Fs (frameterm_letu Ft) Evs (frameterm_letu Ft'))
  %<- (strictness2_lem1 N1 ([a] cons (fletu (N2 a)) (Fs a)) Ft Evs Ft') %.
%term strictness2_lem1_letb1
  %pi (strictness2_lem1 ([a] letb (N1 a) (N2 a)) Fs (frameterm_letb Ft) Evs (frameterm_letb Ft'))
  %<- (strictness2_lem1 N1 ([a] cons (fletb (N2 a)) (Fs a)) Ft Evs Ft') %.
%term strictness2_lem1_lett1
  %pi (strictness2_lem1 ([a] lett (N1 a) (N2 a)) Fs (frameterm_lett Ft) Evs (frameterm_lett Ft'))
  %<- (strictness2_lem1 N1 ([a] cons (flett (N2 a)) (Fs a)) Ft Evs Ft') %.
%term strictness2_lem1_lam
  %pi (strictness2_lem1 ([a] lam T (M4 a)) ([a] cons (fapp (M5 a)) (Fs a)) (frameterm_lam Ft) Evs (frameterm_lam Ft'))
  %<- (strictness2_lem1 ([a] M4 a (M5 a)) Fs Ft Evs Ft') %.
%term strictness2_lem1_tens
  %pi (strictness2_lem1 ([a] tens (M3 a) (M4 a)) ([a] cons (flett (M5 a)) (Fs a)) (frameterm_tens Ft) Evs (frameterm_tens Ft'))
  %<- (strictness2_lem1 ([a] M5 a (M3 a) (M4 a)) Fs Ft Evs Ft') %.
%term strictness2_lem1_unit
  %pi (strictness2_lem1 ([a] unit) ([a] cons (fletu (M5 a)) (Fs a)) (frameterm_unit Ft) Evs (frameterm_unit Ft'))
  %<- (strictness2_lem1 ([a] M5 a) Fs Ft Evs Ft') %.
%term strictness2_lem1_thunk
  %pi (strictness2_lem1 ([a] thunk T (M4 a)) ([a] cons (fletb (M5 a)) (Fs a)) (frameterm_thunk Ft) Evs (frameterm_thunk Ft'))
  %<- (strictness2_lem1 ([a] M5 a (letb (thunk T (M4 a)) (M4 a))) Fs Ft Evs Ft') %.
%term strictness2_lem1_tlam
  %pi (strictness2_lem1 ([a] tlam (M4 a)) ([a] cons (ftapp T) (Fs a)) (frameterm_tlam Ft) Evs (frameterm_tlam Ft'))
  %<- (strictness2_lem1 ([a] M4 a T) Fs Ft Evs Ft') %.
%term strictness2_lem1_app2
  %pi (strictness2_lem1 ([a] a) Fs Ft1 (evs_app EvM12 EvM2 EvM1) (frameterm_app Ft7))
  %<- (strictness2_lem1 ([a] a) Fs Ft1 EvM12 Ft2)
  %<- (strictness2_lem1 ([a] M1' a) ([a] Fs (M1' a)) Ft2 EvM2 Ft4)
  %<- (lem42 ([a] Fs a) ([a] a) (%the (redex (app (lam T M1') M2) _) redex_app) Ft4 Ft5)
  %<- (inverse_ft_app Ft5 Ft6)
  %<- (strictness2_lem1 ([a] a) ([a] cons (fapp M2) (Fs (app a M2))) Ft6 EvM1 Ft7) %.
%term strictness2_lem1_tapp2
  %pi (strictness2_lem1 ([a] a) Fs Ft1 (evs_tapp EvM12 EvM1) (frameterm_tapp Ft5))
  %<- (strictness2_lem1 ([a] a) Fs Ft1 EvM12 Ft2)
  %<- (lem42 ([a] Fs a) ([a] a) (%the (redex (tapp (tlam M1') T) _) redex_tapp) Ft2 Ft3)
  %<- (inverse_ft_tapp Ft3 Ft4)
  %<- (strictness2_lem1 ([a] a) ([a] cons (ftapp T) (Fs (tapp a T))) Ft4 EvM1 Ft5) %.
%term strictness2_lem1_letu2
  %pi (strictness2_lem1 ([a] a) Fs Ft1 (evs_letu EvM2 EvM1) (frameterm_letu Ft5))
  %<- (strictness2_lem1 ([a] a) Fs Ft1 EvM2 Ft2)
  %<- (lem42 ([a] Fs a) ([a] a) (%the (redex (letu unit M2) _) redex_letu) Ft2 Ft3)
  %<- (inverse_ft_letu Ft3 Ft4)
  %<- (strictness2_lem1 ([a] a) ([a] cons (fletu M2) (Fs (letu a M2))) Ft4 EvM1 Ft5) %.
%term strictness2_lem1_lett2
  %pi (strictness2_lem1 ([a] a) Fs Ft1 (evs_lett EvM2 EvM1) (frameterm_lett Ft5))
  %<- (strictness2_lem1 ([a] a) Fs Ft1 EvM2 Ft2)
  %<- (lem42 ([a] Fs a) ([a] a) (%the (redex (lett (tens M1 M2) M3) _) redex_lett) Ft2 Ft3)
  %<- (inverse_ft_lett Ft3 Ft4)
  %<- (strictness2_lem1 ([a] a) ([a] cons (flett M3) (Fs (lett a M3))) Ft4 EvM1 Ft5) %.
%term strictness2_lem1_letb2
  %pi (strictness2_lem1 ([a] a) Fs Ft1 (evs_letb EvM2 EvM1) (frameterm_letb Ft5))
  %<- (strictness2_lem1 ([a] a) Fs Ft1 EvM2 Ft2)
  %<- (lem42 ([a] Fs a) ([a] a) (%the (redex (letb (thunk T M1) M2) _) redex_letb) Ft2 Ft3)
  %<- (inverse_ft_letb Ft3 Ft4)
  %<- (strictness2_lem1 ([a] a) ([a] cons (fletb M2) (Fs (letb a M2))) Ft4 EvM1 Ft5) %.
%worlds () (strictness2_lem1 _ _ _ _ _) %.
% covers strictness2_lem1 +N +Fs +FtV +EVs -FtM.
% terminates {E D} (strictness2_lem1 _ _ D E _).
%total {E D} (strictness2_lem1 _ _ D E _) %.
%sort strictness21 {N} {_ N V \/} {_ M \s/ V} {_ N M \/} %.
%mode strictness21 %in %in %in %out %.
%term strictness21_rule
  %pi (strictness21 N (terminate Ev) Evs (terminate Ev'))
  %<- (eval_frameterm Ev Ft)
  %<- (strictness2_lem1 N ([a term] nil) Ft Evs Ft')
  %<- (frameterm_eval Ft' Ev') %.
%worlds () (strictness21 _ _ _ _) %.
% covers strictness21 +N +Ev -S -Term.
%total {} (strictness21 _ _ _ _) %.

>See all code for this case study. check="true">See STELF's output.

Category:STELF code