Proof of the Progress Property |
Require Import Calculus.
Require Import List.
Module SetProgram(My_Program: Program).
Import My_Program.
Require Proofs_AdmissibilityOfTransitivity.
Module My_Proofs_AdmissibilityOfTransitivity := Proofs_AdmissibilityOfTransitivity.SetProgram(My_Program).
Import My_Proofs_AdmissibilityOfTransitivity.
Import My_Proofs_Subclassing.
Import My_Proofs_TypeOrdering.
Import My_Proofs_Miscellaneous.
Import My_WellFormedness.
Import My_Semantics.
Import My_Typing.
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.
Lemma lemmaA29_aux_1:
forall (f: FieldSym) (fvs: FieldValueList),
(In f (fields_of_fieldValueList fvs)) ->
exists v: Value,
(FieldValueList_contains fvs f v)
.
Definition params_evaluated (xts: ParamTermList): Prop :=
exists xvs: (list (ParamSym * Value)),
(paramValueList_to_ParamTermList xvs) = xts
.
Definition fields_evaluated (fts: FieldTermList): Prop :=
exists fvs: FieldValueList,
(fieldValueList_to_fieldTermList fvs) = fts
.
Definition lemmaA29_aux_2_prop1 (t: Term): Prop :=
(term_evaluated t) \/ ~(term_evaluated t)
.
Definition lemmaA29_aux_2_prop2 (fts: FieldTermList): Prop :=
(fields_evaluated fts) \/ ~(fields_evaluated fts)
.
Definition lemmaA29_aux_2_prop3 (xts: ParamTermList): Prop :=
(params_evaluated xts) \/ ~(params_evaluated xts)
.
Lemma lemmaA29_aux_2:
forall (t: Term),
(term_evaluated t) \/ ~(term_evaluated t)
.
Lemma lemmaA29_aux_3:
forall (xts: ParamTermList),
(params_evaluated xts) \/ ~(params_evaluated xts)
.
Definition lemmaA29_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
G = rootEnv ->
~(term_evaluated t) ->
exists u: Term, (Red_term t u)
.
Definition lemmaA29_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList) (H: (ParamTermListTyping G p m xts)): Prop :=
G = rootEnv ->
~(params_evaluated xts) ->
exists xts': ParamTermList, (Red_paramTermList xts xts')
.
Definition lemmaA29_prop3 (G: Env) (C: ClassSym) (fts: FieldTermList) (H: (FieldTermListTyping G C fts)): Prop :=
G = rootEnv ->
~(fields_evaluated fts) ->
exists fts': FieldTermList, (Red_fieldTermList fts fts')
.
| Progress |
Lemma lemmaA29:
forall (t: Term) (T: type),
(Typing rootEnv t T) ->
~(term_evaluated t) ->
exists u: Term, (Red_term t u)
.
End SetProgram.