%%%%%%%%%%%%%%%%% "library" definitions and lemmas

false: type.

nat-neq-false:
  nat-neq N N -> false -> type.
%mode nat-neq-false +P1 -P2.
%% CASES DELETED

lt-succ: lt N N' -> lt N (1+ N') -> type.
%mode lt-succ +P1 -P2.
%% CASES DELETED

lt-succ': {N} lt N (1+ N) -> type.
%mode lt-succ' +N -P2.
%% CASES DELETED

lt-trans: lt A B -> lt B C -> lt A C -> type.
%mode lt-trans +P1 +P2 -P3.
%% CASES DELETED

lt-neq: lt N N' -> nat-neq N N' -> type.
%mode lt-neq +P1 -P2.
%% CASES DELETED

not-eq-lt:
  lt N N -> false -> type.
%mode not-eq-lt +P1 -P2.
%% CASES DELETED


%%%%%%%%%%%%%%% ex-falsum lemmas for basic operators

false-var-lookup: false -> {R}{V}{A} var-lookup R V A -> type.
%mode false-var-lookup +P1 +R +V +A -P2.
%% [NO] CASES DELETED [!]

false-env-ok: false -> {G} env-ok G -> type.
%mode false-env-ok +P1 +G -P2.

false-env-sub: false -> {G}{G'} env-sub G G' -> type.
%mode false-env-sub +P1 +N +G -P2.

false-check-block: false -> {Pi0}{G}{I} check-block Pi0 G I -> type.
%mode false-check-block +P1 +Pi0 +G +I -P2.

%%%%%%%%%%%%%%% Term equalities and simple congruence lemmas

value-eq: value -> value -> type.
%mode value-eq +A1 +A2.
value-eq1: value-eq A A.

false-value-eq: false -> {A}{A'} value-eq A A' -> type.
%mode false-value-eq +P1 +A +A' -P2.

value-neq: value -> value -> type.
%mode value-neq +A1 +A2.
%deterministic value-neq.

value-neq1: value-neq value-nil (value-cons A0 A1).
value-neq2: value-neq (value-cons A0 A1) value-nil.
value-neq3: value-neq (value-cons A0 A1) (value-cons A0' A1') <-
                    value-neq A0 A0'.
value-neq4: value-neq (value-cons A0 A1) (value-cons A0' A1') <-
                    value-neq A1 A1'.

ty-eq: ty -> ty -> type.
%mode ty-eq +T1 +T2.
ty-eq1: ty-eq T T.

false-ty-eq: false -> {A}{A'} ty-eq A A' -> type.
%mode false-ty-eq +P1 +A +A' -P2.

ty-list-1to1: ty-eq (ty-list T) (ty-list T') -> ty-eq T T' -> type.
%mode ty-list-1to1 +P1 -P2.

ty-listcons-congr: ty-eq T T' -> 
             ty-eq (ty-listcons T) (ty-listcons T') -> type.
%mode ty-listcons-congr +P1 -P2.

ty-neq: ty -> ty -> type.
%mode ty-neq +T1 +T2.
%deterministic ty-neq.

ty-eq-neq-false:
  ty-eq N N' -> ty-neq N N' -> false -> type.
%mode ty-eq-neq-false +P1 +P2 -P3.

nat-eq: nat -> nat -> type.
%mode nat-eq +N1 +N2.

var-eq: var -> var -> type.
%mode var-eq +N1 +N2.

false-var-eq: false -> {V}{V'} var-eq V V' -> type.
%mode false-var-eq +P1 +V +V' -P2.

nat-eq-or-neq: nat -> nat -> type.

nat-eq-or-neq1: nat-eq-or-neq N N.
nat-eq-or-neq2: nat-eq-or-neq N N' <- nat-neq N N'.

lemma: nat-eq-or-neq N N' -> nat-eq-or-neq (1+ N) (1+ N') -> type.
%mode lemma +P1 -P2.
- : lemma nat-eq-or-neq1 nat-eq-or-neq1.
- : lemma (nat-eq-or-neq2 P1) (nat-eq-or-neq2 (nat-neq3 P1)).
%worlds () (lemma P1 _).
%total P1 (lemma P1 _).

always-nat-eq-or-neq: {N}{N'} nat-eq-or-neq N N' -> type.
%mode always-nat-eq-or-neq +N +N' -P.

a1: always-nat-eq-or-neq N N nat-eq-or-neq1.
a2: always-nat-eq-or-neq (1+ N) 0 (nat-eq-or-neq2 nat-neq1).
a3: always-nat-eq-or-neq 0 (1+ N) (nat-eq-or-neq2 nat-neq2).
a4: always-nat-eq-or-neq (1+ N) (1+ N') P2 <-
        always-nat-eq-or-neq N N' P1 <-
        lemma P1 P2.

%worlds () (always-nat-eq-or-neq N N' _).
%total N (always-nat-eq-or-neq N N' _).

var-neq-false: var-neq V V -> false -> type.
%mode var-neq-false +P1 -P2.
-: var-neq-false (var-neq1 P1: var-neq (var# N) (var# N)) P2 <-
     nat-neq-false P1 P2.
%worlds () (var-neq-false _ _).
%total {} (var-neq-false _ _).

nat-neq-comm: nat-neq V V' -> nat-neq V' V -> type.
%mode nat-neq-comm +P1 -P2.
-: nat-neq-comm nat-neq1 nat-neq2.
-: nat-neq-comm nat-neq2 nat-neq1.
-: nat-neq-comm (nat-neq3 P1) (nat-neq3 P2) <- nat-neq-comm P1 P2.
%worlds () (nat-neq-comm P1 _).
%total P1 (nat-neq-comm P1 _).

var-neq-comm: var-neq V V' -> var-neq V' V -> type.
%mode var-neq-comm +P1 -P2.
-: var-neq-comm (var-neq1 P1) (var-neq1 P2) <- nat-neq-comm P1 P2.
%worlds () (var-neq-comm _ _).
%total {} (var-neq-comm _ _).

var-eq-or-neq: var -> var -> type.
var-eq-or-neq1: var-eq-or-neq V V.
var-eq-or-neq2: var-neq V V' -> var-eq-or-neq V V'.

lemma: nat-eq-or-neq N N' -> var-eq-or-neq (var# N) (var# N') -> type.
%mode lemma +P1 -P2.

-: lemma nat-eq-or-neq1 var-eq-or-neq1.
-: lemma (nat-eq-or-neq2 P1) (var-eq-or-neq2 (var-neq1 P1)).

%worlds () (lemma _ _).
%total {} (lemma _ _).

always-var-eq-or-neq: 
  {V}{V'} var-eq-or-neq V V' -> type.
%mode always-var-eq-or-neq +V +V' -P1.

-: always-var-eq-or-neq (var# N) (var# N') P1 <- 
      always-nat-eq-or-neq N N' P2 <- lemma P2 P1.

%worlds () (always-var-eq-or-neq _ _ _).
%total {} (always-var-eq-or-neq _ _ _).

env-eq: env -> env -> type.
%mode env-eq +G1 +G2.
env-eq1: env-eq G G.

false-env-eq: false -> {A}{A'} env-eq A A' -> type.
%mode false-env-eq +P1 +A +A' -P2.

env-neq: env -> env -> type.
%mode env-neq +G1 +G2.
%deterministic env-neq.

var-has-type-congr: 
  var-eq V V' -> ty-eq T T' -> env-eq G G' ->
  env-eq (var-has-type V T G) (var-has-type V' T' G') -> type.
%mode var-has-type-congr +P1 +P2 +P3 -P4.

env-sub-congr: 
  env-eq G1 G1' ->
  env-eq G2 G2' ->
  env-sub G1 G2 ->
  env-sub G1' G2' ->
  type.
%mode env-sub-congr +P1 +P2 +P3 -P4.


check-block-congr:
  env-eq G G' ->
  check-block Pi G I ->
  check-block Pi G' I ->
  type.
%mode check-block-congr +P1 +P2 -P3.


%%%%%%%%%%%% value-has-ty

value-has-ty: value -> ty -> type.
%mode value-has-ty +R +G.
%deterministic value-has-ty.

false-value-has-ty: false -> {A}{T} value-has-ty A T -> type.
%mode false-value-has-ty +P1 +A +T -P2.

value-has-ty-congr: 
  value-eq A A' -> 
  ty-eq T T' ->
  value-has-ty A T -> value-has-ty A' T' -> type.
%mode value-has-ty-congr +P1 +P2 +P3 -P4.

%%%%%%%%%%%%%%% store-has-type

store-has-type: store -> env -> type.
%mode store-has-type +R +G.
%deterministic store-has-type.

store-has-type1: store-has-type R env-empty.

store-has-type2: store-has-type R (var-has-type V T G) <-
                  var-lookup R V A <-
                  value-has-ty A T <-
                  store-has-type R G.
                   
false-store-has-type: false -> {R}{G} store-has-type R G -> type.
%mode false-store-has-type +P1 +R +G -P2.

%%%%%%%%%%%%%%% env-good
env-no-binding: var -> env -> type.
env-no-binding1: env-no-binding V env-empty.
env-no-binding2:  
    env-no-binding  V' (var-has-type V T G) <-
    var-neq V V' <-
    env-no-binding  V' G.

false-env-no-binding: 
     false -> {V}{G} env-no-binding V G -> type.
%mode false-env-no-binding +P1 +V +G -P2.

env-good: env -> type.
env-good1: env-good env-empty.
env-good2: env-good (var-has-type V T G) <- env-no-binding V G <- env-good G.

%%%%%%%%%%%%%%%%%

env-lookup-no-binding2:
  env-good G ->
  env-lookup G V T G' ->
  env-no-binding V' G ->
  env-no-binding V' G' ->
  type.
%mode env-lookup-no-binding2 +P1 +P2 +P3 -P4.

env-lookup-no-binding2-aux:
   var-eq-or-neq V V'' ->
   env-good G ->
   env-no-binding V G ->
   env-lookup (var-has-type V T G) V'' T'' G' ->
   env-no-binding V' G ->
   var-neq V V' ->
   env-no-binding V' G' ->
   type.
%mode env-lookup-no-binding2-aux +P0 +P1 +P2 +P3 +P4 +P5 -P6.


%worlds () (env-lookup-no-binding2 _ _ _ _)
           (env-lookup-no-binding2-aux _ _ _ _ _ _ _).
%total (P1 P1') (env-lookup-no-binding2 P1 _ _ _)
                (env-lookup-no-binding2-aux _ P1' _ _ _ _ _).

env-lookup-no-binding:
  env-good G ->
  env-lookup G V T G' ->
  env-good G' ->
  env-no-binding V G' ->
  type.
%mode env-lookup-no-binding +P1 +P2 -P3 -P4.

%worlds () (env-ok-no-binding P1 P2 _).
%total P1 (env-ok-no-binding P1 P2 _).

env-ok-good:
  env-ok G -> env-good G -> type.
%mode env-ok-good +P1 -P2.

env-no-binding-set:
   env-no-binding V' G ->
   var-neq V V' ->
   env-set G V T G' ->
   env-no-binding V' G' ->
   type.
%mode env-no-binding-set +P1 +P2 +P3 -P4.

env-no-binding-set-aux:
     var-eq-or-neq V1 V ->
     env-no-binding V' G1 ->
     var-neq V1 V' ->
     var-neq V V' ->
     env-set (var-has-type V1 T1 G1) V T G' ->
     env-no-binding V' G' ->
     type.
%mode env-no-binding-set-aux  +P0 +P1a +P1b +P2 +P3 -P4.


%worlds () (env-no-binding-set P1 P2 P3 _)
           (env-no-binding-set-aux P0' P1' P1b' P2' P3' _).

%total (P1 P1') 
   (env-no-binding-set P1 P2 P3 _)
   (env-no-binding-set-aux P0' P1' P1b' P2' P3' _).

%%%%%%%%%%%%%%%%%% var-set-lookup
var-set-lookup: var-set R V A R' -> var-lookup R' V A -> type.
%mode var-set-lookup +P1 -P2.

%%%%%%%%%%%%%%%%%% var-lookup-uniq

var-lookup-uniq:
     var-lookup R V A -> var-lookup R V A' -> value-eq A A' -> type.
%mode var-lookup-uniq +P1 +P2 -P3.

%%%%%%%%%%%%%%%%%% env-lookup-uniq

env-lookup-uniq:
     env-lookup G V T1 G1 -> env-lookup G V T2 G2 -> 
     ty-eq T1 T2 -> env-eq G1 G2 -> type.
%mode env-lookup-uniq +P1 +P2 -P3 -P4.

%%%%%%%%%%%%%%%%%% env-set-good
env-set-good:
   env-good G ->
   env-set G V T G' ->
   env-good G' ->
   type.
%mode env-set-good +P1 +P2 -P3.

%%%%%%%%%%%%%%%%%% var-set-type

var-lookup-equiv: store -> store -> var -> type.

var-lookup-equiv0: var-lookup-equiv R R V.

var-lookup-equiv1: var-lookup-equiv (store-bind V A R) (store-bind V A R') V.

var-lookup-equiv2: var-lookup-equiv (store-bind V A R) R' V' 
                          <- var-neq V V' 
                          <- var-lookup-equiv R R' V'.

var-lookup-equiv3: var-lookup-equiv R (store-bind V A R') V' 
                          <- var-neq V V'
                          <- var-lookup-equiv R R' V'.
      
var-set-diff-lookup-equiv-aux:
    var-eq-or-neq V V' ->
    var-lookup-equiv R R' V' ->
    {A}
    var-lookup-equiv (store-bind V A R) (store-bind V A R') V' ->
    type.

%mode var-set-diff-lookup-equiv-aux +P1 +P2 +A -P3.

var-set-diff-lookup-equiv: 
    var-neq V V' -> var-set R V A R' -> var-lookup-equiv R R' V' -> type.
%mode var-set-diff-lookup-equiv +P1 +P2 -P3.

var-lookup-equiv-e1:
  var-lookup-equiv R R' V ->
  var-lookup R V A ->
  var-lookup R' V A ->
  type.

%mode var-lookup-equiv-e1 +P1 +P2 -P3.

var-lookup-equiv-bind:
  var-eq-or-neq V V' ->
  var-lookup-equiv R R' V' ->
  {A}
  var-lookup-equiv (store-bind V A R) (store-bind V A R') V' ->
  type.

%mode var-lookup-equiv-bind +P1 +P2 +A -P3.

store-has-type-set-diff:
  env-no-binding V G ->
  var-set R V A R' ->
  store-has-type R G ->
  store-has-type R' G ->
  type.

%mode store-has-type-set-diff +P1 +P2 +P3 -P4.

var-set-lookup-diff: 
       var-set R V A R' -> 
       var-neq V V' -> 
       var-lookup R V' A' ->
       var-lookup R' V' A' -> type.
%mode var-set-lookup-diff +P1 +P2 +P3 -P4.

var-set-type: 
    env-good G ->
    store-has-type R G -> 
     value-has-ty A T -> 
      var-set R V A R' -> 
       env-set G V T G' ->
        store-has-type R' G' -> type.
%mode var-set-type +P0 +P1 +P2 +P3 +P4 -P5.

var-set-type-aux:
   var-eq-or-neq V V' ->
   env-good G ->
   env-no-binding V' G ->
   store-has-type R G ->
   value-has-ty A' T' ->
   var-lookup R V' A' ->
   value-has-ty A T ->
   var-set R V A R' ->
   env-set (var-has-type V' T' G) V T G' ->
   store-has-type R' G' ->
   type.

%mode var-set-type-aux +P0 +P1a +P1b +P2 +P3 +P4 +P5 +P6 +P7 -P8.


%worlds () (var-set-type P0 P1 P2 P3 P4 _)
           (var-set-type-aux Q0 Q1a Q1b Q2 Q3 Q4 Q6 Q7 Q8 _).
%total (P1 Q2) (var-set-type P0 P1 P2 P3 P4 _)
           (var-set-type-aux Q0 Q1a Q1b Q2 Q3 Q4 Q6 Q7 Q8 _).

%%%%%%%%%%%%%%%%% progress-check-blocks %%%%%%%%%%%%%%%%%%%

progress-typing-dom-match:
  (typing-dom-match Pi P) ->
  (block-typing-lookup Pi L G) ->
  {I'} (program-lookup P L I') -> type.
%mode progress-typing-dom-match +P1 +P2 -I -P3.

%worlds () (progress-typing-dom-match C D _ _).
%total C (progress-typing-dom-match C D _ _).

%%%%%%%%%%%%%%%%%%%% progress-check-program
progress-check-program:
  (check-program P Pi) -> (block-typing-lookup Pi L G) ->
      {I}  (program-lookup P L I) -> type.
%mode progress-check-program +P1 +P2 -I -P4.

%worlds () (progress-check-program _ _ _ _).
%total {} (progress-check-program _ _ _ _).

%%%%%%%%%%%%%%%%%%%%%%%% progress-env
progress-env:
  env-lookup G V T _ -> store-has-type R G -> 
  {A} var-lookup R V A -> value-has-ty A T -> type.
%mode progress-env +P1 +P2 -A -P3 -P4.

%worlds () (progress-env _ _ _ _ _).
%total P (progress-env _ P _ _ _).

%%%%%%%%%%%%%%%%%%%%%%%% progress-var-set

progress-var-bind-set: 
   {R}{V}{V'}{A}{A'} var-eq-or-neq V V' -> var-set (store-bind V A R) V' A' R' -> type.
%mode progress-var-bind-set +R +V +V' +A +A' +P1 -P2.

progress-var-set: {R}{V}{A} var-set R V A R' -> type.
%mode progress-var-set +R +V +A -P.

%%%%%%%%%%%%%%%%%%%%%%%% progress-branch

progress-branch: 
        {I} program-lookup P L I' -> 
           var-lookup R V A -> 
            step-or-halt P R (instr-branch-if-nil V L ,instr I) ->
             type.

%mode progress-branch +I +P1 +P2 -P3.

%worlds () (progress-branch I P1 P2 _).
%total {} (progress-branch I P1 P2 _).
  
%%%%%%%%%%%%%%%%%%%%%%%% progress

progress-instr: 
           {I'}
           (check-program P Pi) -> (check-instr Pi G I G') -> 
           (store-has-type R G) -> 
           (step-or-halt P R (I ,instr I')) -> type.
%mode progress-instr +I' +P1 +P2 +P3 -P4.

%worlds () (progress-instr _ _ _ _ _).
%total {} (progress-instr _ _ _ _ _).

progress:  (check-program P Pi) -> (check-block Pi G I) -> 
           (store-has-type R G) -> 
           (step-or-halt P R I) -> type.
%mode progress +P1 +P2 +P3 -P4.


%worlds () (progress _ _ _ _).
%total {} (progress _ _ _ _).

%%%%%%%%%%%%%%%%%% subsumption
subsumption: subtype T1 T2 -> value-has-ty A T1 -> value-has-ty A T2 -> type.
%mode subsumption +P1 +P2 -P3.

%%%%%%%%%%%%%%%%%% subsumption-env
subsumption-env-aux:
   store-has-type R G ->
   env-lookup G V T1 G1 ->
   store-has-type R G1 ->
   type.
%mode subsumption-env-aux +P1 +P2 -P3.

subsumption-env-aux2:
     var-eq-or-neq V V' ->
     store-has-type R G ->
     value-has-ty A T ->
     var-lookup R V A ->
     env-lookup (var-has-type V T G) V' T' G' ->
     store-has-type R G' ->
     type.
%mode subsumption-env-aux2 +P0 +P1 +P2 +P3 +P4 -P5.


%worlds () (subsumption-env-aux _ _ _)
           (subsumption-env-aux2 _ _ _ _ _ _).

%total (P1 P1') (subsumption-env-aux P1 _ _)
           (subsumption-env-aux2 _ P1' _ _ _ _).

subsumption-env: env-sub T1 T2 -> store-has-type R T1 -> 
      store-has-type R T2 -> type.
%mode subsumption-env +P1 +P2 -P3.

%%%%%%%%%%%%%%%%%%%%%%%%%%%
subsumption-env2:
   env-lookup G V T G' ->
   store-has-type R G ->
   store-has-type R G' ->
   type.
%mode subsumption-env2 +P1 +P2 -P3.

subsumption-env2-aux: ...


%worlds () (subsumption-env2 _ _ _)
           (subsumption-env2-aux _ _ _ _ _ _).
%total (P1 P1') (subsumption-env2 _ P1 _)
           (subsumption-env2-aux _ _ P1' _ _ _).

%%%%%%%%%%%%%%%%%%%%%%%% preservation-env
preservation-env-lookup:
  env-lookup G V T _ -> store-has-type R G -> 
  var-lookup R V A -> value-has-ty A T -> type.
%mode preservation-env-lookup +P1 +P2 +P3 -P4.


%%%%%%%%%%%%%%%%%%%%%%%
block-typing-lookup-ok:
   block-typing-lookup Pi L G -> env-ok G -> type.
%mode block-typing-lookup-ok +P1 -P2.


block-typing-lookup-uniq:
      block-typing-lookup Pi L G ->
      block-typing-lookup Pi L G' ->
      env-eq G G' ->
      type.

%mode block-typing-lookup-uniq +P1 +P2 -P3.
preservation-block-typing:
   check-blocks Pi P ->
   program-lookup P L I ->
   block-typing-lookup Pi L G ->
   check-block Pi G I ->
   env-ok G ->
   type.
%mode preservation-block-typing +P1 +P2 +P3 -P4 -P5.

%%%%%%%%%%%%%%%%%%% preservation-program-typing
preservation-program-typing:
   check-program P Pi ->
   program-lookup P L I ->
   block-typing-lookup Pi L G ->
   check-block Pi G I ->
   env-ok G ->
   type.
%mode preservation-program-typing +P1 +P2 +P3 -P4 -P5.


%%%%%%%%%%%%%%%%%% preservation

preservation: check-program P Pi -> 
                 env-good G ->
                 store-has-type R G -> 
                 check-block Pi G I ->
                 step P R I R' I' -> 
                {G'} env-good G' -> store-has-type R' G' -> 
                check-block Pi G' I' -> type.

%mode preservation +P1 +P2 +P3 +P4 +P5 -G' -P6 -P7 -P8.

check-instr-seq-invert: 
       check-block Pi G (instr-jump L) ->
       {G'} block-typing-lookup Pi L G' -> env-sub G G' -> type.
%mode check-instr-seq-invert +P1 -G' -P2 -P3.
-: check-instr-seq-invert (check-block-jump P1 P2) _ P2 P1.
%worlds () (check-instr-seq-invert P1 _ _ _).
%total P1  (check-instr-seq-invert P1 _ _ _).

check-instr2-invert: 
       check-block Pi G (instr-branch-if-nil V L ,instr I) ->
       {T}{G'} env-lookup G V T G' -> type.
%mode check-instr2-invert +P1 -T -G' -P2.

check-instr-branch-list-invert: 
       check-block Pi G (instr-branch-if-nil V L ,instr I) ->
       env-lookup G V (ty-list T) G' ->
       {G1}
          block-typing-lookup Pi L G1 ->
          env-sub (var-has-type V ty-nil G') G1 ->
          check-block Pi (var-has-type V (ty-listcons T) G') I ->
          type.
%mode check-instr-branch-list-invert +P1 +P2 -G1 -P3 -P4 -P5.

check-instr-branch-listcons-invert: 
       check-block Pi G (instr-branch-if-nil V L ,instr I) ->
       env-lookup G V (ty-listcons T) G' ->
       {G1}
           block-typing-lookup Pi L G1 ->
           env-sub (var-has-type V ty-nil G') G1 ->
           check-block Pi G I ->
           type.
%mode check-instr-branch-listcons-invert +P1 +P2 -G1 -P3 -P4 -P5.

check-instr-branch-nil-invert: 
       check-block Pi G (instr-branch-if-nil V L ,instr I) ->
       env-lookup G V ty-nil G' ->
       {G1}
           block-typing-lookup Pi L G1 ->
           env-sub G G1 ->
           type.

%mode check-instr-branch-nil-invert +P1 +P2 -G1 -P3 -P4.

preservation-step-branch-not-taken:
        check-program P Pi -> 
        env-good G ->
        store-has-type R G -> 
        check-block Pi G (instr-branch-if-nil V L ,instr I) ->
        var-lookup R V (value-cons A0 A1) ->
        env-lookup G V T G' ->
        {G2}
        env-good G2 ->
        store-has-type R G2 -> 
        check-block Pi G2 I -> type.

%mode preservation-step-branch-not-taken +P1 +P2 +P3 +P4 +P5 +P6 -G2 -P7 -P8 -P9.

%%%%%%%%%%%%%%%%%%% preservation
preservation-step-branch-taken:
        check-program P Pi -> 
        store-has-type R G -> 
        check-block Pi G (instr-branch-if-nil V L ,instr I) ->
        var-lookup R V value-nil ->
        program-lookup P L I' ->
        env-lookup G V T G' ->
        {G2}
        env-good G2 ->
        store-has-type R G2 -> 
        check-block Pi G2 I' -> type.
%mode preservation-step-branch-taken +P1 +P2 +P3 +P4 +P5 +P6 -G2 -P7 -P8 -P9.

check-instr-fetch-field-0-invert: 
       check-block Pi G (instr-fetch-field V 0 V' ,instr I) ->
       {T}{G'}{G''} env-lookup G V (ty-listcons T) G'' ->
           env-set G V' T G' ->
           check-block Pi G' I ->
           type.
%mode check-instr-fetch-field-0-invert +P1 -T -G' -G'' -P2 -P3 -P4.
-: check-instr-fetch-field-0-invert (check-block-seq P1 (check-instr-fetch-field-0 P2 P3)) _ _ _ P3 P2 P1.
%worlds () (check-instr-fetch-field-0-invert P1 _ _ _ _ _ _).
%total P1  (check-instr-fetch-field-0-invert P1 _ _ _ _ _ _).

%worlds () (preservation P1 P2 P3 P4 P5 _ _ _ _).
%total P1 (preservation P1 P2 P3 P4 P5 _ _ _ _).

%%%%%%%%%%%%%%%%%%%% run-prog-finite-well-typed: 

run-prog-finite-well-typed: 
 check-program P Pi -> 
 run-prog-finite P R I -> 
 {G} env-good G -> check-block Pi G I -> store-has-type R G -> type.
%mode run-prog-finite-well-typed +P1 +P2 -G -P3 -P4 -P5.

%worlds () (run-prog-finite-well-typed P1 P2 _ _ _ _).
%total P2 (run-prog-finite-well-typed P1 P2 _ _ _ _).

%%%%%%%%%%%%%%%%%%%% soundness

-: soundness 
 (P1: check-program P Pi)
 (P2: run-prog-finite P R I)
 P9 <-
 run-prog-finite-well-typed P1 P2 G 
  (P3:env-good G)
  (P4:check-block Pi G I)
  (P5:store-has-type R G) <-
 progress P1 P4 P5 (P9:step-or-halt P R I).
%worlds () (soundness _ _ _).
%total {}  (soundness _ _ _).