Proof: Set Key Value Example

Let's prove the following theorem:

Proof:

Proof Table

#	Claim	Reason
1	result of storing 5 at key: a in map: [ ] = output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ]	result of storing 5 at key: a in map: [ ] = output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] (Set Key and Value Property 1)
2	output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] = reverse of [ entry a: 5, [ ] ]	output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] = reverse of [ entry a: 5, [ ] ] (Set Key and Value Add Property)
3	reverse of [ entry a: 5, [ ] ] = [ entry a: 5, [ ] ]	reverse of [ entry a: 5, [ ] ] = [ entry a: 5, [ ] ] (reverse_example_general)
4	output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] = [ entry a: 5, [ ] ]	if output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] = reverse of [ entry a: 5, [ ] ] and reverse of [ entry a: 5, [ ] ] = [ entry a: 5, [ ] ], then output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] = [ entry a: 5, [ ] ] (Transitive Property of Equality)
5	result of storing 5 at key: a in map: [ ] = [ entry a: 5, [ ] ]	if result of storing 5 at key: a in map: [ ] = output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] and output of function store_compute where input key is a, value is 5, map is [ ], and processed map is [ ] = [ entry a: 5, [ ] ], then result of storing 5 at key: a in map: [ ] = [ entry a: 5, [ ] ] (Transitive Property of Equality)

Comments

Please log in to add comments