Nuprl Definition : sqle def

This is Doug Howe's computational simulation relation on terms.
We call if "squiggle" less-or-equal or `sqle`.

The simulation ⌜s ≤ t⌝ is coinductive relation 
on terms that says (essentially) that for any canonical form X, 
if computes to ⌜X[a1; a2; ...]⌝ 
then there exist terms b1, b2,... such that 
computes to ⌜X[b1; b2; ...]⌝
and ⌜a1 ≤ b1⌝,⌜a2 ≤ b2⌝,...

See also the documentation for ⌜t⌝.⋅


Rules referencing :  exceptionNotBottom exceptionNotAxiom divergentSqle axiomSqleEquality sqequalSqle sqleDefinition sqleReflexivity sqleTransitivity sqleRule sqleExtensionalEquality sqleIntensionalEquality fixpointLeast callbyvalueReduce callbyvalueInt callbyvalueAtom1 callbyvalueAtom2 callbyvalueAtom callbyvalueType callbyvalueAdd callbyvalueMultiply callbyvalueDivide callbyvalueRemainder callbyvalueMinus callbyvalueLess callbyvalueIntEq callbyvalueAtomEq callbyvalueAtomnEq callbyvalueApply callbyvalueApplyCases exceptionApplyCases tryReduceValue sqleLambda applyPair applyInl applyInr applyInt callbyvalueCallbyvalue callbyvalueSpread callbyvalueDecide callbyvalueIspair callbyvalueIsaxiom callbyvalueIsinl callbyvalueIsinr callbyvalueIslambda callbyvalueIsint callbyvalueIsatom callbyvalueIsatom1 callbyvalueIsatom2 ispairCases isintCases isatomCases isaxiomCases islambdaCases isinlCases isinrCases isatom1Cases isatom2Cases

s  \mleq{}  t  ==    PRIMITIVE

Date html generated: 2016_07_08-PM-04_46_23
Last ObjectModification: 2015_10_30-AM-11_52_45

Theory : core_1

Home Index