value-mono : % If is-valuetm M -> elab E A M % then -> step* E E' -> elab E' A M -> is-value E' -> exp-not-app E -> type. %mode value-mono +IsValtm +Elab -Step -Elab' -IsVal -NotApp. - : value-mono _ (elab/topintro IsVal) (step*/zero) (elab/topintro IsVal) IsVal (exp-not-app/val IsVal). - : value-mono _ (elab/arrintro Elab) (step*/zero) (elab/arrintro Elab) (is-value/lam) (exp-not-app/val (is-value/lam)). - : value-mono IsVal1 (elab/merge1 Elab1) (step*/left (step/unmerge left) Step1) Elab1' IsVal exp-not-app/merge <- value-mono IsVal1 Elab1 Step1 Elab1' IsVal _. - : value-mono IsVal2 (elab/merge2 Elab2) (step*/left (step/unmerge right) Step2) Elab2' IsVal exp-not-app/merge <- value-mono IsVal2 Elab2 Step2 Elab2' IsVal _. value-mono/sect : value-mono (is-valuetm/pair IsValtm1 IsValtm2) (elab/sectintro Elab1 Elab2) (step*/left step/split Step*) (elab/sectintro (elab/merge1 Elab1') (elab/merge2 Elab2')) (is-value/merge IsVal1 IsVal2) NotApp % exp-not-app/merge <- value-mono IsValtm1 Elab1 Step*1 Elab1' IsVal1 NotApp <- value-mono IsValtm2 Elab2 Step*2 Elab2' IsVal2 _ <- step*merge1 _ Step*1 Step*1M <- step*merge2 _ Step*2 Step*2M <- step*append Step*1M Step*2M Step* . value-mono/inl : value-mono (is-valuetm/inl IsValtm1) (elab/unintro1 Elab1) Step* (elab/unintro1 Elab1') IsVal NotApp <- value-mono IsValtm1 Elab1 Step* Elab1' IsVal NotApp. value-mono/inr : value-mono (is-valuetm/inr IsValtm2) (elab/unintro2 Elab2) Step* (elab/unintro2 Elab2') IsVal NotApp <- value-mono IsValtm2 Elab2 Step* Elab2' IsVal NotApp. %worlds () (value-mono _ _ _ _ _ _). %total (Elab) (value-mono IsValtm Elab _ _ _ _). app-not-value : % If is-value (app E1 E2) % then -> absurd -> type. %mode app-not-value +IsVal -ABSURD. % No possible cases %worlds () (app-not-value _ _). %total {} (app-not-value _ _). % app-not-merge : eqexp (app E1 E2) (merge E1' E2') % -> absurd -> type. % %mode app-not-merge +Eq -ABSURD. % %worlds () (app-not-merge _ _). % %total {} (app-not-merge _ _). apps-don't-adstep: % If adstep (app E1 E2) _ % then -> absurd -> type. %mode apps-don't-adstep +Adstep -ABSURD. % No possible cases %worlds () (apps-don't-adstep _ _). %total {} (apps-don't-adstep _ _). apps-don't-adstep*: % If is-value V -> adstep* (app E1 E2) V % then -> absurd -> type. %mode apps-don't-adstep* +IsVal +Adstep* -ABSURD. - : apps-don't-adstep* IsVal (adstep*/left Adstep _) ABSURD <- apps-don't-adstep Adstep ABSURD. - : apps-don't-adstep* IsVal (adstep*/zero) ABSURD <- app-not-value IsVal ABSURD. %worlds () (apps-don't-adstep* _ _ _). %total {} (apps-don't-adstep* _ _ _).