proposition: Lemma soundness (M : fmodel) Ca : gen Ca -> funsat M Ca.
proof: Proof. elim => {Ca}. - move => C E [w] [/=]. by rewrite satC1 /=. - move => p C E [w] [/=]. rewrite !satC1 /=. by case: (flabel _). - move => s t C a _ U1 _ U2. apply: funsat2 U1 U2; by (move => w; rewrite ?satC1 /=; bcase). - move => s t C a _ U1. apply: funsat1 U1; by (move => w; rewrite ?satC1 /=; bcase). - move => s C a _ U1 [w] [/=]. case/satU1P. rewrite /= implybF negb_forall => /existsP [v]. rewrite negb_imply => /andP [A B] H _. apply U1. exists v. split => //=. rewrite satC1 /= implybF B /=. exact: satCR A. - move => s C H _ U1 [w] [/= wC] [v wv hst]. apply: U1. exists v => //. split => //=. exact: satCR wv. - move => s C a _ U1. apply: funsat1 U1. move => w. rewrite !satC1 [interp _]/= evalbAG. bcase. - move => s C a _ U1 _ U2. apply: funsat2 U1 U2 => w. rewrite !satC1 [interp _]/= [fAG _]lock [fAX _]lock /= -!lock evalbAG. bcase. - move => s C _ IH [w] [/= /satU1P [w1 w2] _]. apply IH; exists w. split => //=. case/forall_inPn : w1 => v wv H. exists v => //. exact: sat_hist0. - move => s C H _ IH1 _ IH2 [w [/= w1 w2]]. case: w2 => [_ ws|v wH wv Hv]. apply: (IH1). exists w. split => //=. by rewrite satC1 w1. apply: (IH2). exists w. split => //=. exists v => //. elim: {w w1 wH wv} Hv => {v} - v. * move => v1 v2. apply: hist0 (v2). rewrite dsatU1 v1 andbT. apply/negP => HC. apply IH1. exists v. split => //=. by rewrite satC1 HC. * move => u vH vu _ H2. apply: histS (vu) (H2). rewrite dsatU1 vH andbT. apply/negP => HC. apply IH2. exists v. split => //=. by exists u. - move => s C H [w] [/= D1 /hist_dsatH D2]. by rewrite dsatU1 D1 in D2. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)